feat: a supremum of semisimple modules is semisimple (#10086)

Another small step toward Jordan-Chevalley-Dunford.

Author: ocfnash

Mathlib/LinearAlgebra/Basic.lean

@@ -212,6 +212,10 @@ theorem _root_.AddMonoidHom.coe_toIntLinearMap_range {M M₂ : Type*} [AddCommGr
     [AddCommGroup M₂] (f : M →+ M₂) :
     LinearMap.range f.toIntLinearMap = AddSubgroup.toIntSubmodule f.range := rfl
 
+lemma _root_.Submodule.map_comap_eq_of_le [RingHomSurjective τ₁₂] {f : F} {p : Submodule R₂ M₂}
+    (h : p ≤ LinearMap.range f) : (p.comap f).map f = p :=
+  SetLike.coe_injective <| Set.image_preimage_eq_of_subset h
+
 /-- A linear map version of `AddMonoidHom.eqLocusM` -/
 def eqLocus (f g : F) : Submodule R M :=
   { (f : M →+ M₂).eqLocusM g with
@@ -1384,7 +1388,7 @@ namespace Submodule
 
 section Module
 
-variable [Semiring R] [AddCommMonoid M] [Module R M]
+variable [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N]
 
 /-- Given `p` a submodule of the module `M` and `q` a submodule of `p`, `p.equivSubtypeMap q`
 is the natural `LinearEquiv` between `q` and `q.map p.subtype`. -/
@@ -1410,6 +1414,17 @@ theorem equivSubtypeMap_symm_apply {p : Submodule R M} {q : Submodule R p} (x :
   rfl
 #align submodule.equiv_subtype_map_symm_apply Submodule.equivSubtypeMap_symm_apply
 
+/-- A linear injection `M ↪ N` restricts to an equivalence `f⁻¹ p ≃ p` for any submodule `p`
+contained in its range. -/
+@[simps! apply]
+noncomputable def comap_equiv_self_of_inj_of_le {f : M →ₗ[R] N} {p : Submodule R N}
+    (hf : Injective f) (h : p ≤ LinearMap.range f) :
+    p.comap f ≃ₗ[R] p :=
+  LinearEquiv.ofBijective
+  ((f ∘ₗ (p.comap f).subtype).codRestrict p <| fun ⟨x, hx⟩ ↦ mem_comap.mp hx)
+  (⟨fun x y hxy ↦ by simpa using hf (Subtype.ext_iff.mp hxy),
+    fun ⟨x, hx⟩ ↦ by obtain ⟨y, rfl⟩ := h hx; exact ⟨⟨y, hx⟩, by simp [Subtype.ext_iff]⟩⟩)
+
 end Module
 
 end Submodule

Mathlib/Order/CompleteLattice.lean

@@ -697,6 +697,11 @@ theorem biSup_congr {p : ι → Prop} (h : ∀ i, p i → f i = g i) :
     ⨆ (i) (_ : p i), f i = ⨆ (i) (_ : p i), g i :=
   iSup_congr fun i ↦ iSup_congr (h i)
 
+theorem biSup_congr' {p : ι → Prop} {f g : (i : ι) → p i → α}
+    (h : ∀ i (hi : p i), f i hi = g i hi) :
+    ⨆ i, ⨆ (hi : p i), f i hi = ⨆ i, ⨆ (hi : p i), g i hi := by
+  congr; ext i; congr; ext hi; exact h i hi
+
 theorem Function.Surjective.iSup_comp {f : ι → ι'} (hf : Surjective f) (g : ι' → α) :
     ⨆ x, g (f x) = ⨆ y, g y := by
   simp only [iSup._eq_1]
@@ -766,6 +771,11 @@ theorem biInf_congr {p : ι → Prop} (h : ∀ i, p i → f i = g i) :
     ⨅ (i) (_ : p i), f i = ⨅ (i) (_ : p i), g i :=
   biSup_congr (α := αᵒᵈ) h
 
+theorem biInf_congr' {p : ι → Prop} {f g : (i : ι) → p i → α}
+    (h : ∀ i (hi : p i), f i hi = g i hi) :
+    ⨅ i, ⨅ (hi : p i), f i hi = ⨅ i, ⨅ (hi : p i), g i hi := by
+  congr; ext i; congr; ext hi; exact h i hi
+
 theorem Function.Surjective.iInf_comp {f : ι → ι'} (hf : Surjective f) (g : ι' → α) :
     ⨅ x, g (f x) = ⨅ y, g y :=
   @Function.Surjective.iSup_comp αᵒᵈ _ _ _ f hf g
@@ -1307,6 +1317,14 @@ theorem iInf_inf_eq : ⨅ x, f x ⊓ g x = (⨅ x, f x) ⊓ ⨅ x, g x :=
   @iSup_sup_eq αᵒᵈ _ _ _ _
 #align infi_inf_eq iInf_inf_eq
 
+lemma biInf_le {ι : Type*} {s : Set ι} (f : ι → α) {i : ι} (hi : i ∈ s) :
+    ⨅ i ∈ s, f i ≤ f i := by
+  simpa only [iInf_subtype'] using iInf_le (ι := s) (f := f ∘ (↑)) ⟨i, hi⟩
+
+lemma le_biSup {ι : Type*} {s : Set ι} (f : ι → α) {i : ι} (hi : i ∈ s) :
+    f i ≤ ⨆ i ∈ s, f i :=
+  biInf_le (α := αᵒᵈ) f hi
+
 /- TODO: here is another example where more flexible pattern matching
    might help.
 

Mathlib/Order/CompleteLatticeIntervals.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Heather Macbeth. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 -/
+import Mathlib.Order.CompactlyGenerated
 import Mathlib.Order.ConditionallyCompleteLattice.Basic
 import Mathlib.Order.LatticeIntervals
 import Mathlib.Data.Set.Intervals.OrdConnected
@@ -27,7 +28,7 @@ open Classical
 
 open Set
 
-variable {α : Type*} (s : Set α)
+variable {ι : Sort*} {α : Type*} (s : Set α)
 
 section SupSet
 
@@ -231,13 +232,94 @@ lemma Set.Icc.coe_sInf [ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b
   congrArg Subtype.val (dif_neg hS.ne_empty)
 
 lemma Set.Icc.coe_iSup [ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b)
-    {ι : Sort*} [Nonempty ι] {S : ι → Set.Icc a b} : letI := Set.Icc.completeLattice h
+    [Nonempty ι] {S : ι → Set.Icc a b} : letI := Set.Icc.completeLattice h
     ↑(iSup S) = (⨆ i, S i : α) :=
   (Set.Icc.coe_sSup h (range_nonempty S)).trans (congrArg sSup (range_comp Subtype.val S).symm)
 
 lemma Set.Icc.coe_iInf [ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b)
-    {ι : Sort*} [Nonempty ι] {S : ι → Set.Icc a b} : letI := Set.Icc.completeLattice h
+    [Nonempty ι] {S : ι → Set.Icc a b} : letI := Set.Icc.completeLattice h
     ↑(iInf S) = (⨅ i, S i : α) :=
   (Set.Icc.coe_sInf h (range_nonempty S)).trans (congrArg sInf (range_comp Subtype.val S).symm)
 
 end Icc
+
+namespace Set.Iic
+
+variable [CompleteLattice α] {a : α}
+
+instance instCompleteLattice : CompleteLattice (Iic a) where
+  sSup S := ⟨sSup ((↑) '' S), by simpa using fun b hb _ ↦ hb⟩
+  sInf S := ⟨a ⊓ sInf ((↑) '' S), by simp⟩
+  le_sSup S b hb := le_sSup <| mem_image_of_mem Subtype.val hb
+  sSup_le S b hb := sSup_le <| fun c' ⟨c, hc, hc'⟩ ↦ hc' ▸ hb c hc
+  sInf_le S b hb := inf_le_of_right_le <| sInf_le <| mem_image_of_mem Subtype.val hb
+  le_sInf S b hb := le_inf_iff.mpr ⟨b.property, le_sInf fun d' ⟨d, hd, hd'⟩  ↦ hd' ▸ hb d hd⟩
+  le_top := by simp
+  bot_le := by simp
+
+variable (S : Set <| Iic a) (f : ι → Iic a) (p : ι → Prop)
+
+@[simp] theorem coe_sSup : (↑(sSup S) : α) = sSup ((↑) '' S) := rfl
+
+@[simp] theorem coe_iSup : (↑(⨆ i, f i) : α) = ⨆ i, (f i : α) := by
+  rw [iSup, coe_sSup]; congr; ext; simp
+
+theorem coe_biSup : (↑(⨆ i, ⨆ (_ : p i), f i) : α) = ⨆ i, ⨆ (_ : p i), (f i : α) := by simp
+
+@[simp] theorem coe_sInf : (↑(sInf S) : α) = a ⊓ sInf ((↑) '' S) := rfl
+
+@[simp] theorem coe_iInf : (↑(⨅ i, f i) : α) = a ⊓ ⨅ i, (f i : α) := by
+  rw [iInf, coe_sInf]; congr; ext; simp
+
+theorem coe_biInf : (↑(⨅ i, ⨅ (_ : p i), f i) : α) = a ⊓ ⨅ i, ⨅ (_ : p i), (f i : α) := by
+  cases isEmpty_or_nonempty ι
+  · simp
+  · simp_rw [coe_iInf, ← inf_iInf, ← inf_assoc, inf_idem]
+
+theorem isCompactElement {b : Iic a} (h : CompleteLattice.IsCompactElement (b : α)) :
+    CompleteLattice.IsCompactElement b := by
+  simp only [CompleteLattice.isCompactElement_iff, Finset.sup_eq_iSup] at h ⊢
+  intro ι s hb
+  replace hb : (b : α) ≤ iSup ((↑) ∘ s) := le_trans hb <| (coe_iSup s) ▸ le_refl _
+  obtain ⟨t, ht⟩ := h ι ((↑) ∘ s) hb
+  exact ⟨t, (by simpa using ht : (b : α) ≤ _)⟩
+
+instance instIsCompactlyGenerated [IsCompactlyGenerated α] : IsCompactlyGenerated (Iic a) := by
+  refine ⟨fun ⟨x, (hx : x ≤ a)⟩ ↦ ?_⟩
+  obtain ⟨s, hs, rfl⟩ := IsCompactlyGenerated.exists_sSup_eq x
+  rw [sSup_le_iff] at hx
+  let f : s → Iic a := fun y ↦ ⟨y, hx _ y.property⟩
+  refine ⟨range f, ?_, ?_⟩
+  · rintro - ⟨⟨y, hy⟩, hy', rfl⟩
+    exact isCompactElement (hs _ hy)
+  · rw [Subtype.ext_iff]
+    change sSup (((↑) : Iic a → α) '' (range f)) = sSup s
+    congr
+    ext b
+    simpa using hx b
+
+end Set.Iic
+
+theorem complementedLattice_of_complementedLattice_Iic
+    [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α]
+    {ι : Type*} {s : Set ι} {f : ι → α}
+    (h : ∀ i ∈ s, ComplementedLattice <| Iic (f i))
+    (h' : ⨆ i ∈ s, f i = ⊤) :
+    ComplementedLattice α := by
+  apply complementedLattice_of_sSup_atoms_eq_top
+  have : ∀ i ∈ s, ∃ t : Set α, f i = sSup t ∧ ∀ a ∈ t, IsAtom a := fun i hi ↦ by
+    replace h := complementedLattice_iff_isAtomistic.mp (h i hi)
+    obtain ⟨u, hu, hu'⟩ := eq_sSup_atoms (⊤ : Iic (f i))
+    refine ⟨(↑) '' u, ?_, ?_⟩
+    · replace hu : f i = ↑(sSup u) := Subtype.ext_iff.mp hu
+      simp_rw [hu, Iic.coe_sSup]
+    · rintro b ⟨⟨a, ha'⟩, ha, rfl⟩
+      exact IsAtom.of_isAtom_coe_Iic (hu' _ ha)
+  choose t ht ht' using this
+  let u : Set α := ⋃ i, ⋃ hi : i ∈ s, t i hi
+  have hu₁ : u ⊆ {a | IsAtom a} := by
+    rintro a ⟨-, ⟨i, rfl⟩, ⟨-, ⟨hi, rfl⟩, ha : a ∈ t i hi⟩⟩
+    exact ht' i hi a ha
+  have hu₂ : sSup u = ⨆ i ∈ s, f i := by simp_rw [sSup_iUnion, biSup_congr' ht]
+  rw [eq_top_iff, ← h', ← hu₂]
+  exact sSup_le_sSup hu₁

Mathlib/Order/Disjoint.lean

@@ -705,6 +705,12 @@ class ComplementedLattice (α) [Lattice α] [BoundedOrder α] : Prop where
 
 export ComplementedLattice (exists_isCompl)
 
+instance Subsingleton.instComplementedLattice
+    [Lattice α] [BoundedOrder α] [Subsingleton α] : ComplementedLattice α := by
+  refine ⟨fun a ↦ ⟨⊥, disjoint_bot_right, ?_⟩⟩
+  rw [Subsingleton.elim ⊥ ⊤]
+  exact codisjoint_top_right
+
 namespace ComplementedLattice
 
 variable [Lattice α] [BoundedOrder α] [ComplementedLattice α]

Mathlib/RingTheory/SimpleModule.lean

@@ -5,6 +5,7 @@ Authors: Aaron Anderson
 -/
 import Mathlib.LinearAlgebra.Isomorphisms
 import Mathlib.Order.JordanHolder
+import Mathlib.Order.CompleteLatticeIntervals
 
 #align_import ring_theory.simple_module from "leanprover-community/mathlib"@"cce7f68a7eaadadf74c82bbac20721cdc03a1cc1"
 
@@ -29,7 +30,7 @@ import Mathlib.Order.JordanHolder
 -/
 
 
-variable (R : Type*) [Ring R] (M : Type*) [AddCommGroup M] [Module R M]
+variable {ι : Type*} (R : Type*) [Ring R] (M : Type*) [AddCommGroup M] [Module R M]
 
 /-- A module is simple when it has only two submodules, `⊥` and `⊤`. -/
 abbrev IsSimpleModule :=
@@ -119,6 +120,34 @@ theorem is_semisimple_iff_top_eq_sSup_simples :
     exact IsSemisimpleModule.sSup_simples_eq_top⟩
 #align is_semisimple_iff_top_eq_Sup_simples is_semisimple_iff_top_eq_sSup_simples
 
+lemma isSemisimpleModule_of_IsSemisimpleModule_submodule {s : Set ι} {p : ι → Submodule R M}
+    (hp : ∀ i ∈ s, IsSemisimpleModule R (p i)) (hp' : ⨆ i ∈ s, p i = ⊤) :
+    IsSemisimpleModule R M := by
+  refine complementedLattice_of_complementedLattice_Iic (fun i hi ↦ ?_) hp'
+  let e : Submodule R (p i) ≃o Set.Iic (p i) := Submodule.MapSubtype.relIso (p i)
+  simpa only [← e.complementedLattice_iff] using hp i hi
+
+lemma isSemisimpleModule_biSup_of_IsSemisimpleModule_submodule {s : Set ι} {p : ι → Submodule R M}
+    (hp : ∀ i ∈ s, IsSemisimpleModule R (p i)) :
+    IsSemisimpleModule R ↥(⨆ i ∈ s, p i) := by
+  let q := ⨆ i ∈ s, p i
+  let p' : ι → Submodule R q := fun i ↦ (p i).comap q.subtype
+  have hp₀ : ∀ i ∈ s, p i ≤ LinearMap.range q.subtype := fun i hi ↦ by
+    simpa only [Submodule.range_subtype] using le_biSup _ hi
+  have hp₁ : ∀ i ∈ s, IsSemisimpleModule R (p' i) := fun i hi ↦ by
+    let e : p' i ≃ₗ[R] p i := (p i).comap_equiv_self_of_inj_of_le q.injective_subtype (hp₀ i hi)
+    exact (Submodule.orderIsoMapComap e).complementedLattice_iff.mpr <| hp i hi
+  have hp₂ : ⨆ i ∈ s, p' i = ⊤ := by
+    apply Submodule.map_injective_of_injective q.injective_subtype
+    simp_rw [Submodule.map_top, Submodule.range_subtype, Submodule.map_iSup]
+    exact biSup_congr fun i hi ↦ Submodule.map_comap_eq_of_le (hp₀ i hi)
+  exact isSemisimpleModule_of_IsSemisimpleModule_submodule hp₁ hp₂
+
+lemma isSemisimpleModule_of_IsSemisimpleModule_submodule' {p : ι → Submodule R M}
+    (hp : ∀ i, IsSemisimpleModule R (p i)) (hp' : ⨆ i, p i = ⊤) :
+    IsSemisimpleModule R M :=
+  isSemisimpleModule_of_IsSemisimpleModule_submodule (s := Set.univ) (fun i _ ↦ hp i) (by simpa)
+
 namespace LinearMap
 
 theorem injective_or_eq_zero [IsSimpleModule R M] (f : M →ₗ[R] N) :