AlgebraQuotient.lean

1 import PaperIRelease.AlgebraPreorder
2 import Mathlib.RingTheory.Ideal.Quotient.Operations
3 
4 set_option autoImplicit false
5 set_option linter.unusedSectionVars false
6 set_option maxHeartbeats 3000000
7 noncomputable section
8 
9 namespace Komorebi.PaperIRelease
10 open Komorebi.Foundation
11 open Komorebi.PacketNaturalityCompletion.FullBlocks
12 
13 universe u v w
14 variable {K : Type u} [Field K]
15 variable {X : Type v} [AddCommGroup X] [Module K X]
16 variable {I : Type w} [Fintype I] [DecidableEq I] [PartialOrder I]
17 
18 /-- Diagonal packets are multiplicative for a partial-order support pattern. -/
19 theorem restrict_diagonal_mul (P : LinearProjectorFamily K X I)
20     (S T : preorderSupportAlgebra P) (i : I) :
21     restrictBlocks P (S.1 * T.1) i i =
22       (restrictBlocks P S.1 i i).comp (restrictBlocks P T.1 i i) := by
23   change restrictBlocks P (S.1.comp T.1) i i = _
24   rw [restrictBlocks_comp]
25   change (∑ j, (restrictBlocks P S.1 i j).comp (restrictBlocks P T.1 j i)) = _
26   rw [Finset.sum_eq_single i]
27   · intro j _ hji
28     by_cases hij : i ≤ j
29     · have hji' : ¬ j ≤ i := fun h => hji (le_antisymm h hij)
30       rw [S.property i j hji']
31       simp
32     · rw [T.property j i hij]
33       simp
34   · simp
35 
36 /-- Projection to all diagonal packet endomorphisms is an algebra homomorphism. -/
37 def diagonalClassHom (P : LinearProjectorFamily K X I) :
38     preorderSupportAlgebra P →ₐ[K] ((i : I) → Module.End K (LinearMap.range (P.proj i))) where
39   toFun T i := restrictBlocks P T.1 i i
40   map_one' := by
41     ext i x
42     exact congrArg Subtype.val (packetProjection_apply_coe P i x)
43   map_mul' S T := by
44     funext i
45     exact restrict_diagonal_mul P S T i
46   map_zero' := by
47     ext i x
48     simp [restrictBlocks, packetProjection, packetInclusion]
49   map_add' S T := by
50     ext i x
51     simp [restrictBlocks, packetProjection, packetInclusion]
52   commutes' c := by
53     ext i x
54     change P.proj i (c • (x : X)) = c • (x : X)
55     rw [map_smul]
56     congr 1
57     exact congrArg Subtype.val (packetProjection_apply_coe P i x)
58 
59 /-- Every prescribed diagonal-class operator family has a supported ambient lift. -/
60 theorem diagonalClassHom_surjective (P : LinearProjectorFamily K X I) :
61     Function.Surjective (diagonalClassHom P) := by
62   intro f
63   let B : PacketBlocks P := ∑ i, singleBlock P i i (f i)
64   have hB : BlocksSupported P (· ≤ ·) B := by
65     intro b a hab
66     change (∑ i, singleBlock P i i (f i)) b a = 0
67     simp only [Finset.sum_apply]
68     apply Finset.sum_eq_zero
69     intro i _
70     exact singleBlock_supported P (· ≤ ·) le_rfl (f i) b a hab
71   refine ⟨⟨synthesizeBlocks P B, ?_⟩, ?_⟩
72   · change BlocksSupported P (· ≤ ·) (restrictBlocks P (synthesizeBlocks P B))
73     rw [restrictBlocks_synthesizeBlocks]
74     exact hB
75   · funext i
76     change restrictBlocks P (synthesizeBlocks P B) i i = f i
77     rw [restrictBlocks_synthesizeBlocks]
78     dsimp only [B]
79     simp only [Finset.sum_apply]
80     rw [Finset.sum_eq_single i]
81     · simp [singleBlock]
82     · intro j _ hji
83       simp [singleBlock, Ne.symm hji]
84     · simp
85 
86 /-- The kernel consists exactly of the strict-class support ideal. -/
87 theorem diagonalClassHom_eq_zero_iff (P : LinearProjectorFamily K X I)
88     (T : preorderSupportAlgebra P) :
89     diagonalClassHom P T = 0 ↔ OperatorSupported P (· < ·) T.1 := by
90   rw [strictSupport_iff_same_class_zero]
91   constructor
92   · intro h a b hab
93     have hab' : a = b := le_antisymm hab.1 hab.2
94     subst b
95     apply (restricted_block_zero_iff P T.1 a a).mp
96     exact congrFun h a
97   · intro h
98     funext i
99     apply (restricted_block_zero_iff P T.1 i i).mpr
100     exact h i i ⟨le_rfl, le_rfl⟩
101 
102 /-- The diagonal-class quotient is the full product of packet endomorphism algebras. -/
103 def diagonalClassQuotientEquiv (P : LinearProjectorFamily K X I) :
104     (preorderSupportAlgebra P ⧸ RingHom.ker (diagonalClassHom P).toRingHom) ≃ₐ[K]
105       ((i : I) → Module.End K (LinearMap.range (P.proj i))) :=
106   Ideal.quotientKerAlgEquivOfSurjective (diagonalClassHom_surjective P)
107 
108 end Komorebi.PaperIRelease

Back to source controls