ProductPresentation.lean

1 import PaperICompletion8.SemisimpleFormula
2 
3 /-! Coherent multiplicity presentations for actual modules over a product
4 of matrix rings. Simple summands are identified with natural factors by a
5 nonzero column projection and Schur's lemma, then grouped by their factor.
6 No multiplicity equality or module decomposition is supplied by the caller. -/
7 set_option autoImplicit false
8 set_option linter.unusedSectionVars false
9 
10 namespace Komorebi.PaperICompletion8.ProductPresentation
11 
12 open scoped DirectSum
13 open Komorebi.PaperICompletion8.DivisionProduct
14 open Komorebi.PaperICompletion8.RegularMultiplicity
15 open Komorebi.PaperICompletion8.SemisimpleFormula
16 
17 universe u v w
18 variable {I : Type v} [Fintype I] [DecidableEq I]
19 variable {D : I → Type u} [∀ i, DivisionRing (D i)]
20 variable (d : I → ℕ)
21 
22 /-- Every actual simple module is isomorphic to a natural factor, without choosing it as an input. -/
23 theorem simple_equiv_natural (S : Type w) [AddCommGroup S]
24     [Module (DivisionProductAlgebra (D := D) d) S]
25     [IsSimpleModule (DivisionProductAlgebra (D := D) d) S]
26     (hd : ∀ i, 0 < d i) :
27     ∃ i : I, Nonempty (S ≃ₗ[DivisionProductAlgebra (D := D) d] Simple (D := D) d i) := by
28   classical
29   let A := DivisionProductAlgebra (D := D) d
30   let : Nontrivial S := IsSimpleModule.nontrivial A S
31   obtain ⟨J, ⟨e⟩⟩ := IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModule A S
32   let f : S →ₗ[A] MultiplicityModule (D := D) d d :=
33     (regularColumnsEquiv d).toLinearMap ∘ₗ J.subtype ∘ₗ e.toLinearMap
34   have hf : Function.Injective f :=
35     (regularColumnsEquiv d).injective.comp (J.subtype_injective.comp e.injective)
36   obtain ⟨x, hx⟩ := exists_ne (0 : S)
37   have hfx : f x ≠ 0 := by
38     intro h
39     exact hx (hf (h.trans f.map_zero.symm))
40   obtain ⟨i, hi⟩ : ∃ i : I, f x i ≠ 0 := by
41     by_contra h
42     apply hfx
43     funext i
44     by_contra hh
45     exact h ⟨i, hh⟩
46   obtain ⟨j, hj⟩ : ∃ j : Fin (d i), f x i j ≠ 0 := by
47     by_contra h
48     apply hi
49     funext j
50     by_contra hh
51     exact h ⟨j, hh⟩
52   let g : S →ₗ[A] Simple (D := D) d i :=
53     LinearMap.proj j ∘ₗ LinearMap.proj i ∘ₗ f
54   have hg : g ≠ 0 := by
55     intro h
56     exact hj (congrArg (fun h : S →ₗ[A] Simple (D := D) d i ↦ h x) h)
57   let := simple_isSimple (D := D) d i (hd i)
58   exact ⟨i, ⟨LinearEquiv.ofBijective g (LinearMap.bijective_of_ne_zero hg)⟩⟩
59 
60 /-- Grouping a finite family of simple factors is a genuine A-linear reindexing. -/
61 noncomputable def regroupSimpleFactors {J : Type w} [Fintype J] (f : J → I) :
62     (∀ j : J, Simple (D := D) d (f j)) ≃ₗ[DivisionProductAlgebra (D := D) d]
63       MultiplicityModule (D := D) d (fun i ↦ Fintype.card {j : J // f j = i}) := by
64   classical
65   let A := DivisionProductAlgebra (D := D) d
66   let e (i : I) :
67       (∀ j : {j : J // f j = i}, Simple (D := D) d (f j.1)) ≃ₗ[A]
68         (Fin (Fintype.card {j : J // f j = i}) → Simple (D := D) d i) :=
69     (LinearEquiv.piCongrRight fun j ↦ by
70       rcases j with ⟨j, hj⟩
71       subst i
72       exact LinearEquiv.refl A _).trans
73     (LinearEquiv.piCongrLeft A (fun _ : Fin (Fintype.card {j : J // f j = i}) ↦
74       Simple (D := D) d i) (Fintype.equivFin {j : J // f j = i}))
75   refine { __ := Equiv.piCongrFiberwise (fun i ↦ (e i).toEquiv)
76            map_add' := ?_, map_smul' := ?_ }
77   · intro x y
78     funext i
79     exact (e i).map_add _ _
80   · intro a x
81     funext i
82     exact (e i).map_smul a _
83 
84 /-- Every finitely generated module over the actual matrix product has a compatible multiplicity presentation. -/
85 theorem exists_multiplicity_presentation (M : Type w) [AddCommGroup M]
86     [Module (DivisionProductAlgebra (D := D) d) M]
87     [Module.Finite (DivisionProductAlgebra (D := D) d) M]
88     (hd : ∀ i, 0 < d i) :
89     ∃ m : I → ℕ,
90       Nonempty (M ≃ₗ[DivisionProductAlgebra (D := D) d] MultiplicityModule (D := D) d m) := by
91   classical
92   let A := DivisionProductAlgebra (D := D) d
93   obtain ⟨n, S, e, hS⟩ := IsSemisimpleModule.exists_linearEquiv_fin_dfinsupp A M
94   let (j : Fin n) : IsSimpleModule A (S j) := hS j
95   choose f ef using fun j : Fin n ↦ simple_equiv_natural (D := D) d (S j) hd
96   exact ⟨fun i ↦ Fintype.card {j : Fin n // f j = i}, ⟨e.trans
97     (DirectSum.linearEquivFunOnFintype A (Fin n) (fun j ↦ S j)) |>.trans
98     (LinearEquiv.piCongrRight fun j ↦ (ef j).some) |>.trans
99     (regroupSimpleFactors d f)⟩⟩
100 
101 end Komorebi.PaperICompletion8.ProductPresentation

Back to source controls