From 1ee23d0ea17a0cb1a5c5cd3c785d2d6e7fb0e19a Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 8 Jul 2026 20:01:30 +0200 Subject: [PATCH 1/3] feat: variations of Submodule.disjoint_map with weaker hypotheses --- Mathlib/Algebra/Module/Submodule/Map.lean | 3 +-- Mathlib/LinearAlgebra/Span/Basic.lean | 21 +++++++++++++++++++++ 2 files changed, 22 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Module/Submodule/Map.lean b/Mathlib/Algebra/Module/Submodule/Map.lean index 2e2f7d8ae98dc0..8ee3ab95cc8422 100644 --- a/Mathlib/Algebra/Module/Submodule/Map.lean +++ b/Mathlib/Algebra/Module/Submodule/Map.lean @@ -452,8 +452,7 @@ end OrderIso --TODO(Mario): is there a way to prove this from order properties? theorem map_inf_eq_map_inf_comap [RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} {p : Submodule R M} {p' : Submodule R₂ M₂} : map f p ⊓ p' = map f (p ⊓ comap f p') := - le_antisymm (by rintro _ ⟨⟨x, h₁, rfl⟩, h₂⟩; exact ⟨_, ⟨h₁, h₂⟩, rfl⟩) - (le_inf (map_mono inf_le_left) (map_le_iff_le_comap.2 inf_le_right)) + .symm <| SetLike.coe_injective <| image_inter_preimage _ _ _ @[simp] theorem map_comap_subtype : map p.subtype (comap p.subtype p') = p ⊓ p' := diff --git a/Mathlib/LinearAlgebra/Span/Basic.lean b/Mathlib/LinearAlgebra/Span/Basic.lean index 2f16a8eb65657b..20d67960899b9e 100644 --- a/Mathlib/LinearAlgebra/Span/Basic.lean +++ b/Mathlib/LinearAlgebra/Span/Basic.lean @@ -561,6 +561,16 @@ theorem comap_map_sup_of_comap_le {f : M →ₛₗ[τ₁₂] M₂} {p : Submodul rw [add_comm, ← eq_sub_iff_add_eq, ← map_sub] at eq; subst eq simpa using p.add_mem (le hz) hy +lemma disjoint_map_of_ker_le_right {f : M →ₛₗ[τ₁₂] M₂} {p q : Submodule R M} + (hpq : Disjoint p q) (hker : f.ker ≤ q) : Disjoint (p.map f) (q.map f) := by + rw [disjoint_iff, map_inf_eq_map_inf_comap, comap_map_eq, eq_bot_iff, map_le_iff_le_comap, + comap_bot, sup_eq_left.mpr hker, hpq.eq_bot] + exact bot_le + +lemma disjoint_map_of_ker_le_left {f : M →ₛₗ[τ₁₂] M₂} {p q : Submodule R M} + (hpq : Disjoint p q) (hker : f.ker ≤ p) : Disjoint (p.map f) (q.map f) := + disjoint_map_of_ker_le_right hpq.symm hker |>.symm + theorem isCoatom_comap_or_eq_top (f : M →ₛₗ[τ₁₂] M₂) {p : Submodule R₂ M₂} (hp : IsCoatom p) : IsCoatom (comap f p) ∨ comap f p = ⊤ := or_iff_not_imp_right.mpr fun h ↦ ⟨h, fun q lt ↦ by @@ -633,6 +643,17 @@ variable [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] variable {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] variable {p p' : Submodule R M} +lemma disjoint_map_of_ker_le_inf_sup {f : M →ₛₗ[τ₁₂] M₂} {p q : Submodule R M} + (hpq : Disjoint p q) (hker : f.ker ≤ (f.ker ⊓ p) ⊔ (f.ker ⊓ q)) : + Disjoint (p.map f) (q.map f) := by + replace hker : f.ker = (f.ker ⊓ p) ⊔ (f.ker ⊓ q) := + le_antisymm hker (sup_le inf_le_left inf_le_left) + have : q ⊔ f.ker = q ⊔ (p ⊓ f.ker) := by + conv_lhs => rw [hker, inf_comm]; simp only [← sup_assoc, inf_left_le_sup_right, sup_of_le_left] + rw [disjoint_iff, map_inf_eq_map_inf_comap, comap_map_eq, eq_bot_iff, map_le_iff_le_comap, + comap_bot, this, ← inf_sup_assoc_of_le _ inf_le_left, hpq.eq_bot, bot_sup_eq] + exact inf_le_right + theorem map_strict_mono_or_ker_sup_lt_ker_sup (f : M →ₛₗ[τ₁₂] M₂) (hab : p < p') : Submodule.map f p < Submodule.map f p' ∨ LinearMap.ker f ⊓ p < LinearMap.ker f ⊓ p' := by obtain (⟨h, -⟩ | ⟨-, h⟩) := Prod.mk_lt_mk.mp <| strictMono_inf_prod_sup (z := LinearMap.ker f) hab From fc047ad0fa85487803b144f97bf354808dcdd208 Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 8 Jul 2026 20:04:19 +0200 Subject: [PATCH 2/3] docstring --- Mathlib/LinearAlgebra/Span/Basic.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Mathlib/LinearAlgebra/Span/Basic.lean b/Mathlib/LinearAlgebra/Span/Basic.lean index 20d67960899b9e..b2319a5241708c 100644 --- a/Mathlib/LinearAlgebra/Span/Basic.lean +++ b/Mathlib/LinearAlgebra/Span/Basic.lean @@ -643,6 +643,9 @@ variable [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] variable {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] variable {p p' : Submodule R M} +/-- Let `f : M →ₗ N`. Assume that `p` and `q` are disjoint submodules of `M`, +and that the kernel of `f` "decomposes well" wrt. `p` and `q`, in the sense that +`f.ker = (f.ker ⊓ p) ⊔ (f.ker ⊓ q)`. Then `map f p` and `map f q` are disjoint. -/ lemma disjoint_map_of_ker_le_inf_sup {f : M →ₛₗ[τ₁₂] M₂} {p q : Submodule R M} (hpq : Disjoint p q) (hker : f.ker ≤ (f.ker ⊓ p) ⊔ (f.ker ⊓ q)) : Disjoint (p.map f) (q.map f) := by From b90eaaf8375bb6cf30813460eb96bbeff431df53 Mon Sep 17 00:00:00 2001 From: ADedecker Date: Fri, 10 Jul 2026 14:50:57 +0200 Subject: [PATCH 3/3] remove not fully satisfying statement --- Mathlib/LinearAlgebra/Span/Basic.lean | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/Mathlib/LinearAlgebra/Span/Basic.lean b/Mathlib/LinearAlgebra/Span/Basic.lean index b2319a5241708c..cd957fe7a6343d 100644 --- a/Mathlib/LinearAlgebra/Span/Basic.lean +++ b/Mathlib/LinearAlgebra/Span/Basic.lean @@ -643,20 +643,6 @@ variable [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] variable {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] variable {p p' : Submodule R M} -/-- Let `f : M →ₗ N`. Assume that `p` and `q` are disjoint submodules of `M`, -and that the kernel of `f` "decomposes well" wrt. `p` and `q`, in the sense that -`f.ker = (f.ker ⊓ p) ⊔ (f.ker ⊓ q)`. Then `map f p` and `map f q` are disjoint. -/ -lemma disjoint_map_of_ker_le_inf_sup {f : M →ₛₗ[τ₁₂] M₂} {p q : Submodule R M} - (hpq : Disjoint p q) (hker : f.ker ≤ (f.ker ⊓ p) ⊔ (f.ker ⊓ q)) : - Disjoint (p.map f) (q.map f) := by - replace hker : f.ker = (f.ker ⊓ p) ⊔ (f.ker ⊓ q) := - le_antisymm hker (sup_le inf_le_left inf_le_left) - have : q ⊔ f.ker = q ⊔ (p ⊓ f.ker) := by - conv_lhs => rw [hker, inf_comm]; simp only [← sup_assoc, inf_left_le_sup_right, sup_of_le_left] - rw [disjoint_iff, map_inf_eq_map_inf_comap, comap_map_eq, eq_bot_iff, map_le_iff_le_comap, - comap_bot, this, ← inf_sup_assoc_of_le _ inf_le_left, hpq.eq_bot, bot_sup_eq] - exact inf_le_right - theorem map_strict_mono_or_ker_sup_lt_ker_sup (f : M →ₛₗ[τ₁₂] M₂) (hab : p < p') : Submodule.map f p < Submodule.map f p' ∨ LinearMap.ker f ⊓ p < LinearMap.ker f ⊓ p' := by obtain (⟨h, -⟩ | ⟨-, h⟩) := Prod.mk_lt_mk.mp <| strictMono_inf_prod_sup (z := LinearMap.ker f) hab