feat(LinearMap): Added lemmas relating kernels of linear maps to Submodule.map

[Raph-DG]

Added the lemma ne_map_or_ne_kernel_inter_of_lt stating that if A < B as submodules, then for any linear map f, ker f ⊓ A ≠ ker f ⊓ B ∨ Submodule.map f A ≠ Submodule.map f B. We also prove the corollaries ker_inter_mono_of_map_eq and map_mono_of_ker_inter_eq.

Co-authored-by: Raphael Douglas Giles ([email protected])

---

[github-actions]

PR summary d7b7085dfa

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ ker_inf_lt_ker_inf
+ ker_inter_mono_of_map_eq
+ map_lt_map_of_ker_inf_eq
+ map_lt_map_or
+ map_mono_of_ker_inter_eq
+ ne_map_or_ne_kernel_inter_of_lt

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[j-loreaux]

Here are alternate names, statements and proofs. Note that the proof uses the IsModularLattice (Submodule R M) instance, so this would need to be placed in LinearAlgebra.Span.Basic.

Suggested change

	theorem ne_map_or_ne_kernel_inter_of_lt {M' : Type*} [AddCommGroup M'] [Module R M']
	{A B : Submodule R M} (f : M →ₗ[R] M') (hab : A < B) :
	Submodule.map f A ≠ Submodule.map f B ∨ ker f ⊓ A ≠ ker f ⊓ B := by
	by_cases q : ker f ⊓ A ≠ ker f ⊓ B
	· exact Or.inr q
	· simp only [ne_eq, not_not] at q
	apply Or.inl
	intro h
	apply hab.ne
	apply le_antisymm hab.le
	intro x hx
	obtain ⟨z, hz, hzy⟩ := (h ▸ ⟨x, hx, rfl⟩ : f x ∈ Submodule.map f A)
	suffices x - z ∈ LinearMap.ker f ⊓ A by simpa using add_mem this.2 hz
	exact q ▸ ⟨by simp[hzy], sub_mem hx (hab.le hz)⟩
	theorem ker_inter_mono_of_map_eq {M' : Type*} [AddCommGroup M'] [Module R M']
	{A B : Submodule R M} {f : M →ₗ[R] M'} (hab : A < B)
	(q : Submodule.map f A = Submodule.map f B) : LinearMap.ker f ⊓ A < LinearMap.ker f ⊓ B :=
	lt_iff_le_and_ne.mpr ⟨inf_le_inf le_rfl hab.le,
	Or.elim (LinearMap.ne_map_or_ne_kernel_inter_of_lt f hab)
	(fun h ↦ False.elim (h q)) (fun h ↦ h)⟩
	theorem map_mono_of_ker_inter_eq {M' : Type*} [AddCommGroup M'] [Module R M']
	{A B : Submodule R M} {f : M →ₗ[R] M'} (hab : A < B)
	(q : LinearMap.ker f ⊓ A = LinearMap.ker f ⊓ B) : Submodule.map f A < Submodule.map f B :=
	lt_iff_le_and_ne.mpr ⟨Set.image_mono hab.le,
	Or.elim (LinearMap.ne_map_or_ne_kernel_inter_of_lt f hab)
	(fun h ↦ h) (fun h ↦ False.elim (h q))⟩
	theorem map_lt_map_or {M' : Type*} [AddCommGroup M'] [Module R M']
	{A B : Submodule R M} (f : M →ₗ[R] M') (hab : A < B) :
	Submodule.map f A < Submodule.map f B ∨ ker f ⊓ A < ker f ⊓ B := by
	obtain (⟨h, -⟩ | ⟨-, h⟩) := Prod.mk_lt_mk.mp <| strictMono_inf_prod_sup (z := ker f) hab
	· exact .inr <| by simpa [inf_comm]
	· simp_rw [← Submodule.comap_map_eq] at h
	exact Or.inl <| lt_of_le_of_ne (Submodule.map_mono hab.le) fun _ ↦ h.ne <| by congr
	theorem ker_inf_lt_ker_inf {M' : Type*} [AddCommGroup M'] [Module R M']
	{A B : Submodule R M} {f : M →ₗ[R] M'} (hab : A < B)
	(q : Submodule.map f A = Submodule.map f B) : LinearMap.ker f ⊓ A < LinearMap.ker f ⊓ B :=
	f.map_lt_map_or hab |>.resolve_left q.not_lt
	theorem map_lt_map_of_ker_inf_eq {M' : Type*} [AddCommGroup M'] [Module R M']
	{A B : Submodule R M} {f : M →ₗ[R] M'} (hab : A < B)
	(q : LinearMap.ker f ⊓ A = LinearMap.ker f ⊓ B) : Submodule.map f A < Submodule.map f B :=
	f.map_lt_map_or hab |>.resolve_right q.not_lt

[Raph-DG]

Thanks so much for the suggestions, these proofs are really nice and compact and the names are much cleaner :)