SemisimpleFormula.lean

1 import PaperICompletion8.RegularMultiplicity
2 import PaperICompletion7.ModuleTop
3 import Mathlib.RingTheory.SimpleModule.WedderburnArtin
4 import Mathlib.RingTheory.Artinian.Module
5 
6 /-! The manuscript's semisimple formula, with genuine nonsplit ring and
7 module decompositions. Abstract ring and simple-module decomposition
8 existence is explicitly integrated from the proved upstream theorems.
9 The radical-top formula uses the existing canonical quotient and rank. -/
10 set_option autoImplicit false
11 set_option linter.unusedSectionVars false
12 
13 namespace Komorebi.PaperICompletion8.SemisimpleFormula
14 
15 open scoped DirectSum
16 open Komorebi.SeedRankBasics Komorebi.SeedRankOperations
17 open Komorebi.PaperICompletion8.DivisionProduct
18 open Komorebi.PaperICompletion8.RegularMultiplicity
19 open Komorebi.PaperICompletion7.ModuleTop
20 
21 universe u v
22 attribute [local instance] RingHomInvPair.of_ringEquiv
23 
24 section AbstractExistence
25 variable (R M : Type u) [Ring R] [AddCommGroup M] [Module R M]
26 
27 /-- Actual Wedderburn-Artin existence over arbitrary division rings. -/
28 theorem exists_wedderburn_decomposition [IsSemisimpleRing R] :
29     ∃ (q : ℕ) (D : Fin q → Type u) (d : Fin q → ℕ) (_ : ∀ i, DivisionRing (D i)),
30       (∀ i, NeZero (d i)) ∧
31       Nonempty (R ≃+* ∀ i, Matrix (Fin (d i)) (Fin (d i)) (D i)) :=
32   IsSemisimpleRing.exists_ringEquiv_pi_matrix_divisionRing R
33 
34 /-- Every finitely generated module over a semisimple ring really decomposes into simple modules. -/
35 theorem exists_finite_simple_decomposition [IsSemisimpleRing R] [Module.Finite R M] :
36     ∃ (n : ℕ) (S : Fin n → Submodule R M),
37       Nonempty (M ≃ₗ[R] ⨁ i : Fin n, S i) ∧ ∀ i, IsSimpleModule R (S i) := by
38   obtain ⟨n, S, e, hS⟩ := IsSemisimpleModule.exists_linearEquiv_fin_dfinsupp R M
39   exact ⟨n, S, ⟨e⟩, hS⟩
40 
41 /-- A finite-dimensional algebra has an actually semisimple radical quotient. -/
42 theorem finiteAlgebra_radicalQuotient_isSemisimple
43     (k : Type u) [Field k] [Algebra k R] [Module.Finite k R] :
44     IsSemisimpleRing (R ⧸ Ring.jacobson R) := by
45   let : IsArtinianRing R := isArtinian_of_tower k inferInstance
46   infer_instance
47 
48 /-- The decomposition of a finite algebra's radical quotient is constructed, not assumed. -/
49 theorem finiteAlgebra_radicalQuotient_decomposition
50     (k : Type u) [Field k] [Algebra k R] [Module.Finite k R] :
51     ∃ (q : ℕ) (D : Fin q → Type u) (d : Fin q → ℕ) (_ : ∀ i, DivisionRing (D i)),
52       (∀ i, NeZero (d i)) ∧
53       Nonempty ((R ⧸ Ring.jacobson R) ≃+* ∀ i, Matrix (Fin (d i)) (Fin (d i)) (D i)) := by
54   let := finiteAlgebra_radicalQuotient_isSemisimple R k
55   exact exists_wedderburn_decomposition (R ⧸ Ring.jacobson R)
56 
57 end AbstractExistence
58 
59 section Formula
60 variable {I : Type v} [Fintype I] [DecidableEq I]
61 variable {D : I → Type u} [∀ i, DivisionRing (D i)]
62 variable (d m : I → ℕ)
63 variable {R M : Type (max u v)} [Ring R] [AddCommGroup M] [Module R M]
64 
65 /-- The printed nonsplit formula for the actual displayed ring and module equivalences. -/
66 theorem semisimple_seedRank_of_decompositions
67     (eR : R ≃+* DivisionProductAlgebra (D := D) d)
68     (eM : M ≃ₛₗ[(RingHomClass.toRingHom eR)] (⨁ i : I, (Fin (m i) → Simple (D := D) d i)))
69     (hd : ∀ i, 0 < d i) : seedRank R M = (maxCeilDiv d m : Cardinal) := by
70   let : RingHomSurjective (RingHomClass.toRingHom eR) := ⟨eR.surjective⟩
71   exact (seedRank_eq_of_bijective_semilinear eM.toLinearMap eM.bijective).trans
72     (directSum_seedRank d m hd)
73 
74 /-- The same result in natural-valued canonical rank. -/
75 theorem semisimple_seedFinrank_of_decompositions
76     (eR : R ≃+* DivisionProductAlgebra (D := D) d)
77     (eM : M ≃ₛₗ[(RingHomClass.toRingHom eR)] (⨁ i : I, (Fin (m i) → Simple (D := D) d i)))
78     (hd : ∀ i, 0 < d i) : seedFinrank R M = maxCeilDiv d m := by
79   simpa only [Cardinal.toNat_natCast, seedFinrank, seedRank, Submodule.spanFinrank] using
80     congrArg Cardinal.toNat (semisimple_seedRank_of_decompositions d m eR eM hd)
81 
82 /-- Generator rank is computed by the nonsplit decomposition of the ACTUAL module top. -/
83 theorem radicalTop_seedRank_of_decompositions [Module.Finite R M]
84     (eR : (R ⧸ Ring.jacobson R) ≃+* DivisionProductAlgebra (D := D) d)
85     (eM : RadicalTop R M ≃ₛₗ[(RingHomClass.toRingHom eR)]
86       (⨁ i : I, (Fin (m i) → Simple (D := D) d i)))
87     (hd : ∀ i, 0 < d i) : seedRank R M = (maxCeilDiv d m : Cardinal) := by
88   rw [seedRank_eq_radicalTop]
89   exact semisimple_seedRank_of_decompositions d m eR eM hd
90 
91 /-- Natural-valued radical-top multiplicity formula. -/
92 theorem radicalTop_seedFinrank_of_decompositions [Module.Finite R M]
93     (eR : (R ⧸ Ring.jacobson R) ≃+* DivisionProductAlgebra (D := D) d)
94     (eM : RadicalTop R M ≃ₛₗ[(RingHomClass.toRingHom eR)]
95       (⨁ i : I, (Fin (m i) → Simple (D := D) d i)))
96     (hd : ∀ i, 0 < d i) : seedFinrank R M = maxCeilDiv d m := by
97   simpa only [Cardinal.toNat_natCast, seedFinrank, seedRank, Submodule.spanFinrank] using
98     congrArg Cardinal.toNat (radicalTop_seedRank_of_decompositions d m eR eM hd)
99 
100 end Formula
101 
102 section RestrictedTop
103 variable {R M : Type u} [Ring R] [AddCommGroup M] [Module R M] [Module.Finite R M]
104 
105 /-- The literal module top has the same generator rank even when its action
106 is viewed over the original ring. Scalar restriction changes no generating set. -/
107 theorem seedRank_eq_radicalTop_restricted :
108     seedRank R M = seedRank R (RadicalTop R M) := by
109   let f : RadicalTop R M →ₛₗ[Ideal.Quotient.mk (Ring.jacobson R)] RadicalTop R M :=
110     { toFun := id
111       map_add' := fun _ _ ↦ rfl
112       map_smul' := fun _ _ ↦ rfl }
113   have h := seedRank_eq_of_bijective_semilinear f Function.bijective_id
114   exact seedRank_eq_radicalTop.trans h.symm
115 
116 end RestrictedTop
117 
118 section SplitSpecialization
119 variable {I : Type v} [Fintype I] [DecidableEq I]
120 variable (k : Type u) [Field k] (d m : I → ℕ)
121 variable {R M : Type (max u v)} [Ring R] [AddCommGroup M] [Module R M] [Module.Finite R M]
122 
123 /-- The split top formula needs no algebraic closure once the split decomposition is supplied. -/
124 theorem split_radicalTop_seedRank
125     (eR : (R ⧸ Ring.jacobson R) ≃+* DivisionProductAlgebra (D := fun _ : I ↦ k) d)
126     (eM : RadicalTop R M ≃ₛₗ[(RingHomClass.toRingHom eR)]
127       (⨁ i : I, (Fin (m i) → Simple (D := fun _ : I ↦ k) d i)))
128     (hd : ∀ i, 0 < d i) : seedRank R M = (maxCeilDiv d m : Cardinal) :=
129   radicalTop_seedRank_of_decompositions d m eR eM hd
130 
131 /-- Exact printed split corollary with a decomposition of the original ring
132 and the original-ring action on its literal module top. Algebraic closure is
133 unnecessary once the displayed split decomposition is given. -/
134 theorem split_originalRing_top_seedRank
135     (eR : R ≃+* DivisionProductAlgebra (D := fun _ : I ↦ k) d)
136     (eM : RadicalTop R M ≃ₛₗ[(RingHomClass.toRingHom eR)]
137       (⨁ i : I, (Fin (m i) → Simple (D := fun _ : I ↦ k) d i)))
138     (hd : ∀ i, 0 < d i) : seedRank R M = (maxCeilDiv d m : Cardinal) := by
139   rw [seedRank_eq_radicalTop_restricted]
140   exact semisimple_seedRank_of_decompositions d m eR eM hd
141 
142 end SplitSpecialization
143 end Komorebi.PaperICompletion8.SemisimpleFormula

Back to source controls