SemisimpleExistence.lean

1 import PaperICompletion8.ProductPresentation
2 
3 /-! Certificate-free public existence and seed formulas. The ring and
4 compatible module presentations are constructed inside each theorem.
5 Classical choice selects proved decompositions, not assumed conclusions. -/
6 set_option autoImplicit false
7 
8 namespace Komorebi.PaperICompletion8.SemisimpleExistence
9 
10 open scoped DirectSum
11 open Komorebi.SeedRankBasics
12 open Komorebi.PaperICompletion8.DivisionProduct
13 open Komorebi.PaperICompletion8.RegularMultiplicity
14 open Komorebi.PaperICompletion8.SemisimpleFormula
15 open Komorebi.PaperICompletion8.ProductPresentation
16 open Komorebi.PaperICompletion7.ModuleTop
17 
18 universe u v
19 attribute [local instance] RingHomInvPair.of_ringEquiv
20 
21 section Transport
22 variable {I : Type v} [Fintype I] [DecidableEq I]
23 variable {D : I → Type u} [∀ i, DivisionRing (D i)]
24 variable (d : I → ℕ)
25 variable {R M : Type (max u v)} [Ring R] [AddCommGroup M] [Module R M] [Module.Finite R M]
26 
27 /-- Any actual Wedderburn ring isomorphism admits a compatible natural-factor module decomposition. -/
28 theorem exists_compatible_presentation
29     (eR : R ≃+* DivisionProductAlgebra (D := D) d) (hd : ∀ i, 0 < d i) :
30     ∃ m : I → ℕ, Nonempty (M ≃ₛₗ[(RingHomClass.toRingHom eR)]
31       (⨁ i : I, (Fin (m i) → Simple (D := D) d i))) := by
32   classical
33   let A := DivisionProductAlgebra (D := D) d
34   let : Module A M := Module.compHom M eR.symm.toRingHom
35   let e : M ≃ₛₗ[(RingHomClass.toRingHom eR)] M :=
36     { __ := AddEquiv.refl M
37       map_smul' a x := by
38         change a • x = eR.symm (eR a) • x
39         rw [eR.symm_apply_apply] }
40   let : RingHomSurjective (RingHomClass.toRingHom eR) := ⟨eR.surjective⟩
41   let : Module.Finite A M := Module.Finite.of_surjective e.toLinearMap e.surjective
42   obtain ⟨m, ⟨em⟩⟩ := exists_multiplicity_presentation (D := D) d M hd
43   exact ⟨m, ⟨(e.trans em).trans (multiplicityDirectSumEquiv (D := D) d m)⟩⟩
44 
45 end Transport
46 
47 section Existence
48 variable (R M : Type u) [Ring R] [AddCommGroup M] [Module R M] [Module.Finite R M]
49 
50 /-- Full semisimple seed formula with the ring and compatible module decompositions built internally. -/
51 theorem exists_semisimple_seed_formula [IsSemisimpleRing R] :
52     ∃ (q : ℕ) (D : Fin q → Type u) (d m : Fin q → ℕ) (_ : ∀ i, DivisionRing (D i)),
53       (∀ i, 0 < d i) ∧
54       ∃ eR : R ≃+* DivisionProductAlgebra (D := D) d,
55         Nonempty (M ≃ₛₗ[(RingHomClass.toRingHom eR)]
56           (⨁ i : Fin q, (Fin (m i) → Simple (D := D) d i))) ∧
57         seedRank R M = (maxCeilDiv d m : Cardinal) := by
58   classical
59   obtain ⟨q, D, d, hD, hd, ⟨eR⟩⟩ := exists_wedderburn_decomposition R
60   let := hD
61   have hpos : ∀ i, 0 < d i := fun i ↦ Nat.pos_of_ne_zero (hd i).out
62   obtain ⟨m, ⟨eM⟩⟩ := exists_compatible_presentation (M := M) (D := D) d eR hpos
63   exact ⟨q, D, d, m, hD, hpos, eR, ⟨eM⟩,
64     semisimple_seedRank_of_decompositions d m eR eM hpos⟩
65 
66 /-- The same construction for an Artinian ring uses its literal radical quotient and module top. -/
67 theorem exists_artinian_radicalTop_seed_formula [IsArtinianRing R] :
68     ∃ (q : ℕ) (D : Fin q → Type u) (d m : Fin q → ℕ) (_ : ∀ i, DivisionRing (D i)),
69       (∀ i, 0 < d i) ∧
70       ∃ eR : (R ⧸ Ring.jacobson R) ≃+* DivisionProductAlgebra (D := D) d,
71         Nonempty (RadicalTop R M ≃ₛₗ[(RingHomClass.toRingHom eR)]
72           (⨁ i : Fin q, (Fin (m i) → Simple (D := D) d i))) ∧
73         seedRank R M = (maxCeilDiv d m : Cardinal) := by
74   let : Module.Finite (R ⧸ Ring.jacobson R) (RadicalTop R M) :=
75     idealTop_finite (Ring.jacobson R) le_rfl
76   obtain ⟨q, D, d, m, hD, hd, eR, heM, hr⟩ :=
77     exists_semisimple_seed_formula (R ⧸ Ring.jacobson R) (RadicalTop R M)
78   exact ⟨q, D, d, m, hD, hd, eR, heM, seedRank_eq_radicalTop.trans hr⟩
79 
80 /-- Manuscript-facing finite-dimensional-algebra formula with no caller-supplied decomposition. -/
81 theorem exists_finiteAlgebra_seed_formula
82     (k : Type u) [Field k] [Algebra k R] [Module.Finite k R] :
83     ∃ (q : ℕ) (D : Fin q → Type u) (d m : Fin q → ℕ) (_ : ∀ i, DivisionRing (D i)),
84       (∀ i, 0 < d i) ∧
85       ∃ eR : (R ⧸ Ring.jacobson R) ≃+* DivisionProductAlgebra (D := D) d,
86         Nonempty (RadicalTop R M ≃ₛₗ[(RingHomClass.toRingHom eR)]
87           (⨁ i : Fin q, (Fin (m i) → Simple (D := D) d i))) ∧
88         seedRank R M = (maxCeilDiv d m : Cardinal) := by
89   let : IsArtinianRing R := isArtinian_of_tower k inferInstance
90   exact exists_artinian_radicalTop_seed_formula R M
91 
92 end Existence
93 end Komorebi.PaperICompletion8.SemisimpleExistence

Back to source controls