[Merged by Bors] - feat: add lemma LinearMap.trace_restrict_eq_sum_trace_restrict

Mathlib/Algebra/DirectSum/Basic.lean

@@ -378,7 +378,7 @@ theorem coe_of_apply {M S : Type*} [DecidableEq ι] [AddCommMonoid M] [SetLike S
 
 For the alternate statement in terms of independence and spanning, see
 `DirectSum.subgroup_isInternal_iff_independent_and_supr_eq_top` and
-`DirectSum.isInternalSubmodule_iff_independent_and_supr_eq_top`. -/
+`DirectSum.isInternal_submodule_iff_independent_and_iSup_eq_top`. -/
 def IsInternal {M S : Type*} [DecidableEq ι] [AddCommMonoid M] [SetLike S M]
     [AddSubmonoidClass S M] (A : ι → S) : Prop :=
   Function.Bijective (DirectSum.coeAddMonoidHom A)

Mathlib/Algebra/DirectSum/LinearMap.lean

@@ -41,6 +41,9 @@ lemma toMatrix_directSum_collectedBasis_eq_blockDiagonal' {R M₁ M₂ : Type*}
 
 variable [∀ i, Module.Finite R (N i)] [∀ i, Module.Free R (N i)]
 
+/-- The trace of an endomorphism of a direct sum is the sum of the traces on each component.
+
+See also `LinearMap.trace_restrict_eq_sum_trace_restrict`. -/
 lemma trace_eq_sum_trace_restrict [Fintype ι]
     {f : M →ₗ[R] M} (hf : ∀ i, MapsTo f (N i) (N i)) :
     trace R M f = ∑ i, trace R (N i) (f.restrict (hf i)) := by
@@ -86,4 +89,38 @@ lemma trace_comp_eq_zero_of_commute_of_trace_restrict_eq_zero
   rw [restrict_comp, trace_comp_eq_mul_of_commute_of_isNilpotent μ h_comm
     (f.isNilpotent_restrict_iSup_sub_algebraMap μ), hg, mul_zero]
 
+lemma mapsTo_biSup_of_mapsTo (s : Set ι) {f : Module.End R M} (hf : ∀ i, MapsTo f (N i) (N i)) :
+    MapsTo f ↑(⨆ i ∈ s, N i) ↑(⨆ i ∈ s, N i) := by
+  intro x hx
+  induction' hx using Submodule.iSup_induction' with i m hm y z _ _ hy hz
+  · by_cases hi : i ∈ s
+    · apply Submodule.mem_iSup_of_mem i
+      simp only [hi, iSup_pos] at hm ⊢
+      exact hf i hm
+    · replace hm : m = 0 := by simpa [hi] using hm
+      simp [hm]
+  · simp
+  · rw [map_add]
+    exact add_mem hy hz
+
+/-- The trace of an endomorphism of a direct sum is the sum of the traces on each component.
+
+Note that it is important the statement gives the user definitional control over `p` since the
+_type_ of the term `trace R p (f.restrict hp')` depends on `p`. -/
+lemma trace_eq_sum_trace_restrict_of_eq_biSup
+    (s : Finset ι) (h : CompleteLattice.Independent <| fun i : s ↦ N i)
+    {f : Module.End R M} (hf : ∀ i, MapsTo f (N i) (N i))
+    (p : Submodule R M) (hp : p = ⨆ i ∈ s, N i)
+    (hp' : MapsTo f p p := hp ▸ mapsTo_biSup_of_mapsTo (s : Set ι) hf) :
+    trace R p (f.restrict hp') = ∑ i in s, trace R (N i) (f.restrict (hf i)) := by
+  let N' : s → Submodule R p := fun i ↦ (N i).comap p.subtype
+  replace h : IsInternal N' := hp ▸ isInternal_biSup_submodule_of_independent (s : Set ι) h
+  have hf' : ∀ i, MapsTo (restrict f hp') (N' i) (N' i) := fun i x hx' ↦ by simpa using hf i hx'
+  let e : (i : s) → N' i ≃ₗ[R] N i := fun ⟨i, hi⟩ ↦ (N i).comapSubtypeEquivOfLe (hp ▸ le_biSup N hi)
+  have _i1 : ∀ i, Module.Finite R (N' i) := fun i ↦ Module.Finite.equiv (e i).symm
+  have _i2 : ∀ i, Module.Free R (N' i) := fun i ↦ Module.Free.of_equiv (e i).symm
+  rw [trace_eq_sum_trace_restrict h hf', ← s.sum_coe_sort]
+  have : ∀ i : s, f.restrict (hf i) = (e i).conj ((f.restrict hp').restrict (hf' i)) := fun _ ↦ rfl
+  exact Finset.sum_congr rfl <| by simp [this]
+
 end LinearMap

Mathlib/Algebra/DirectSum/Module.lean

@@ -461,6 +461,20 @@ theorem isInternal_ne_bot_iff {A : ι → Submodule R M} :
   simp only [isInternal_submodule_iff_independent_and_iSup_eq_top]
   exact Iff.and CompleteLattice.independent_ne_bot_iff_independent <| by simp
 
+lemma isInternal_biSup_submodule_of_independent {A : ι → Submodule R M} (s : Set ι)
+    (h : CompleteLattice.Independent <| fun i : s ↦ A i) :
+    IsInternal <| fun (i : s) ↦ (A i).comap (⨆ i ∈ s, A i).subtype := by
+  refine (isInternal_submodule_iff_independent_and_iSup_eq_top _).mpr ⟨?_, by simp [iSup_subtype]⟩
+  let p := ⨆ i ∈ s, A i
+  have hp : ∀ i ∈ s, A i ≤ p := fun i hi ↦ le_biSup A hi
+  let e : Submodule R p ≃o Set.Iic p := Submodule.MapSubtype.relIso p
+  suffices (e ∘ fun i : s ↦ (A i).comap p.subtype) = fun i ↦ ⟨A i, hp i i.property⟩ by
+    rw [← CompleteLattice.independent_map_orderIso_iff e, this]
+    exact CompleteLattice.independent_of_independent_coe_Iic_comp h
+  ext i m
+  change m ∈ ((A i).comap p.subtype).map p.subtype ↔ _
+  rw [Submodule.map_comap_subtype, inf_of_le_right (hp i i.property)]
+
 /-! Now copy the lemmas for subgroup and submonoids. -/
 
 

Mathlib/LinearAlgebra/Basic.lean

@@ -567,21 +567,25 @@ theorem submoduleImage_apply_of_le {M' : Type*} [AddCommGroup M'] [Module R M']
 
 end Image
 
-end Semiring
+section rangeRestrict
 
-end LinearMap
+variable [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂)
 
-@[simp]
-theorem LinearMap.range_rangeRestrict [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M]
-    [Module R M₂] (f : M →ₗ[R] M₂) : range f.rangeRestrict = ⊤ := by simp [f.range_codRestrict _]
+@[simp] theorem range_rangeRestrict : range f.rangeRestrict = ⊤ := by simp [f.range_codRestrict _]
 #align linear_map.range_range_restrict LinearMap.range_rangeRestrict
 
-@[simp]
-theorem LinearMap.ker_rangeRestrict [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M]
-    [Module R M₂] (f : M →ₗ[R] M₂) : ker f.rangeRestrict = ker f :=
-  LinearMap.ker_codRestrict _ _ _
+theorem surjective_rangeRestrict : Surjective f.rangeRestrict := by
+  rw [← range_eq_top, range_rangeRestrict]
+
+@[simp] theorem ker_rangeRestrict : ker f.rangeRestrict = ker f := LinearMap.ker_codRestrict _ _ _
 #align linear_map.ker_range_restrict LinearMap.ker_rangeRestrict
 
+end rangeRestrict
+
+end Semiring
+
+end LinearMap
+
 /-! ### Linear equivalences -/
 
 

Mathlib/LinearAlgebra/Span.lean

@@ -919,6 +919,38 @@ lemma _root_.LinearMap.range_domRestrict_eq_range_iff {f : M →ₛₗ[τ₁₂]
   rw [← hf]
   exact LinearMap.range_domRestrict_eq_range_iff
 
+@[simp]
+lemma biSup_comap_subtype_eq_top {ι : Type*} (s : Set ι) (p : ι → Submodule R M) :
+    ⨆ i ∈ s, (p i).comap (⨆ i ∈ s, p i).subtype = ⊤ := by
+  refine eq_top_iff.mpr fun ⟨x, hx⟩ _ ↦ ?_
+  suffices x ∈ (⨆ i ∈ s, (p i).comap (⨆ i ∈ s, p i).subtype).map (⨆ i ∈ s, (p i)).subtype by
+    obtain ⟨y, hy, rfl⟩ := Submodule.mem_map.mp this
+    exact hy
+  suffices ∀ i ∈ s, (comap (⨆ i ∈ s, p i).subtype (p i)).map (⨆ i ∈ s, p i).subtype = p i by
+    simpa only [map_iSup, biSup_congr this]
+  intro i hi
+  rw [map_comap_eq, range_subtype, inf_eq_right]
+  exact le_biSup p hi
+
+lemma biSup_comap_eq_top_of_surjective {ι : Type*} (s : Set ι) (hs : s.Nonempty)
+    (p : ι → Submodule R₂ M₂) (hp : ⨆ i ∈ s, p i = ⊤)
+    (f : M →ₛₗ[τ₁₂] M₂) (hf : Surjective f) :
+    ⨆ i ∈ s, (p i).comap f = ⊤ := by
+  obtain ⟨k, hk⟩ := hs
+  suffices (⨆ i ∈ s, (p i).comap f) ⊔ LinearMap.ker f = ⊤ by
+    rw [← this, left_eq_sup]; exact le_trans f.ker_le_comap (le_biSup (fun i ↦ (p i).comap f) hk)
+  rw [iSup_subtype'] at hp ⊢
+  rw [← comap_map_eq, map_iSup_comap_of_sujective hf, hp, comap_top]
+
+lemma biSup_comap_eq_top_of_range_eq_biSup
+    {R R₂ : Type*} [Ring R] [Ring R₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂]
+    [Module R M] [Module R₂ M₂] {ι : Type*} (s : Set ι) (hs : s.Nonempty)
+    (p : ι → Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (hf : LinearMap.range f = ⨆ i ∈ s, p i) :
+    ⨆ i ∈ s, (p i).comap f = ⊤ := by
+  suffices ⨆ i ∈ s, (p i).comap (LinearMap.range f).subtype = ⊤ by
+    rw [← biSup_comap_eq_top_of_surjective s hs _ this _ f.surjective_rangeRestrict]; rfl
+  exact hf ▸ biSup_comap_subtype_eq_top s p
+
 end AddCommGroup
 
 section DivisionRing

Mathlib/Order/SupIndep.lean

@@ -7,6 +7,7 @@ import Mathlib.Data.Finset.Sigma
 import Mathlib.Data.Finset.Pairwise
 import Mathlib.Data.Finset.Powerset
 import Mathlib.Data.Fintype.Basic
+import Mathlib.Order.CompleteLatticeIntervals
 
 #align_import order.sup_indep from "leanprover-community/mathlib"@"c4c2ed622f43768eff32608d4a0f8a6cec1c047d"
 
@@ -473,6 +474,13 @@ theorem Independent.disjoint_biSup {ι : Type*} {α : Type*} [CompleteLattice α
   Disjoint.mono_right (biSup_mono fun _ hi => (ne_of_mem_of_not_mem hi hx : _)) (ht x)
 #align complete_lattice.independent.disjoint_bsupr CompleteLattice.Independent.disjoint_biSup
 
+lemma independent_of_independent_coe_Iic_comp {ι : Sort*} {a : α} {t : ι → Set.Iic a}
+    (ht : Independent ((↑) ∘ t : ι → α)) : Independent t := by
+  intro i x
+  specialize ht i
+  simp_rw [Function.comp_apply, ← Set.Iic.coe_iSup] at ht
+  exact @ht x
+
 end CompleteLattice
 
 theorem CompleteLattice.independent_iff_supIndep [CompleteLattice α] {s : Finset ι} {f : ι → α} :