AlgebraClassGrouping.lean

1 import PaperIRelease.AlgebraQuotient
2 
3 set_option autoImplicit false
4 set_option linter.unusedSectionVars false
5 set_option maxHeartbeats 3000000
6 noncomputable section
7 
8 namespace Komorebi.PaperIRelease
9 open Komorebi.Foundation
10 open PacketAggregation
11 
12 universe u v w z
13 variable {K : Type u} [Field K]
14 variable {X : Type v} [AddCommGroup X] [Module K X]
15 variable {I : Type w} [Fintype I] [DecidableEq I]
16 variable {J : Type z} [Fintype J] [DecidableEq J]
17 
18 theorem groupedProjection_original (P : LinearProjectorFamily K X I)
19     (σ : I → J) (a : I) (x : X) :
20     groupedProjection P σ (σ a) (P.proj a x) = P.proj a x := by
21   obtain ⟨y, hy⟩ := original_mem_grouped P σ a ⟨P.proj a x, ⟨x, rfl⟩⟩
22   change (groupedFamily P σ).proj (σ a) (P.proj a x) = P.proj a x
23   change (groupedFamily P σ).proj (σ a) y = P.proj a x at hy
24   rw [← hy]
25   exact (groupedFamily P σ).idempotent (σ a) y
26 
27 /-- Grouping by a relation-compatible class map preserves the exact support condition. -/
28 theorem grouped_operatorSupported_iff (P : LinearProjectorFamily K X I)
29     (σ : I → J) (rel : J → J → Prop) (T : Module.End K X) :
30     OperatorSupported (groupedFamily P σ) rel T ↔
31       OperatorSupported P (fun a b => rel (σ a) (σ b)) T := by
32   rw [operatorSupported_iff_ambient, operatorSupported_iff_ambient]
33   constructor
34   · intro h b a hab
35     ext x
36     have hh := congrArg (P.proj b) (LinearMap.congr_fun (h (σ b) (σ a) hab) (P.proj a x))
37     simpa [transferBlock, groupedFamily,
38       proj_groupedProjection, groupedProjection_original] using hh
39   · intro h d c hcd
40     ext x
41     simp only [transferBlock, LinearMap.comp_apply, groupedFamily,
42       groupedProjection, LinearMap.sum_apply, map_sum, LinearMap.zero_apply]
43     apply Finset.sum_eq_zero
44     intro b hb
45     apply Finset.sum_eq_zero
46     intro a ha
47     have hab : ¬ rel (σ b) (σ a) := by
48       rw [(Finset.mem_filter.mp ha).2, (Finset.mem_filter.mp hb).2]
49       exact hcd
50     exact LinearMap.congr_fun (h a b hab) x
51 
52 section Preorder
53 variable [Preorder I]
54 
55 abbrev PreorderClasses (I : Type w) [Preorder I] := Antisymmetrization I (· ≤ ·)
56 
57 noncomputable instance preorderClassesFintype : Fintype (PreorderClasses I) := by
58   classical
59   exact Fintype.ofSurjective (toAntisymmetrization (· ≤ ·))
60     (fun C => ⟨ofAntisymmetrization (· ≤ ·) C, toAntisymmetrization_ofAntisymmetrization (· ≤ ·) C⟩)
61 noncomputable instance preorderClassesDecidableEq : DecidableEq (PreorderClasses I) := Classical.decEq _
62 
63 /-- The actual quotient class of a packet in the preorder. -/
64 def packetClass : I → PreorderClasses I := toAntisymmetrization (· ≤ ·)
65 
66 /-- Projectors obtained by aggregating precisely the mutual-reachability classes. -/
67 def classPacketFamily (P : LinearProjectorFamily K X I) :
68     LinearProjectorFamily K X (PreorderClasses I) :=
69   groupedFamily P packetClass
70 
71 theorem classSupport_iff (P : LinearProjectorFamily K X I) (T : Module.End K X) :
72     OperatorSupported (classPacketFamily P) (· ≤ ·) T ↔ OperatorSupported P (· ≤ ·) T := by
73   rw [classPacketFamily, grouped_operatorSupported_iff]
74   simp only [packetClass, toAntisymmetrization_le_toAntisymmetrization_iff]
75 
76 /-- Grouping equivalence does not alter the ambient operator: it changes only support coordinates. -/
77 def preorderClassSupportEquiv (P : LinearProjectorFamily K X I) :
78     preorderSupportAlgebra P ≃ₐ[K] preorderSupportAlgebra (classPacketFamily P) where
79   toFun T := ⟨T.1, (classSupport_iff P T.1).mpr T.property⟩
80   invFun T := ⟨T.1, (classSupport_iff P T.1).mp T.property⟩
81   left_inv _ := rfl
82   right_inv _ := rfl
83   map_mul' _ _ := rfl
84   map_add' _ _ := rfl
85   commutes' _ := rfl
86 
87 /-- The diagonal-class map on the original preorder support algebra. -/
88 def preorderDiagonalHom (P : LinearProjectorFamily K X I) :
89     preorderSupportAlgebra P →ₐ[K] ((C : PreorderClasses I) →
90       Module.End K (LinearMap.range ((classPacketFamily P).proj C))) :=
91   (diagonalClassHom (classPacketFamily P)).comp (preorderClassSupportEquiv P).toAlgHom
92 
93 theorem preorderDiagonalHom_surjective (P : LinearProjectorFamily K X I) :
94     Function.Surjective (preorderDiagonalHom P) :=
95   (diagonalClassHom_surjective (classPacketFamily P)).comp (preorderClassSupportEquiv P).surjective
96 
97 /-- The quotient map's kernel is exactly the ideal of strictly-between-class blocks. -/
98 theorem preorderDiagonalHom_eq_zero_iff (P : LinearProjectorFamily K X I)
99     (T : preorderSupportAlgebra P) :
100     preorderDiagonalHom P T = 0 ↔ OperatorSupported P (· < ·) T.1 := by
101   change diagonalClassHom (classPacketFamily P) (preorderClassSupportEquiv P T) = 0 ↔ _
102   rw [diagonalClassHom_eq_zero_iff]
103   change OperatorSupported (classPacketFamily P) (· < ·) T.1 ↔ _
104   rw [classPacketFamily, grouped_operatorSupported_iff]
105   simp only [packetClass, toAntisymmetrization_lt_toAntisymmetrization_iff]
106 
107 theorem preorderDiagonal_kernel_eq (P : LinearProjectorFamily K X I) :
108     RingHom.ker (preorderDiagonalHom P).toRingHom = (strictSupportIdeal P).asIdeal := by
109   ext T
110   change preorderDiagonalHom P T = 0 ↔ T ∈ (strictSupportIdeal P).asIdeal
111   rw [preorderDiagonalHom_eq_zero_iff]
112   simp only [TwoSidedIdeal.mem_asIdeal, mem_strictSupportIdeal]
113 
114 /-- Full preorder support algebra quotient, indexed by the actual quotient classes. -/
115 def preorderQuotientEquiv (P : LinearProjectorFamily K X I) :
116     (preorderSupportAlgebra P ⧸ RingHom.ker (preorderDiagonalHom P).toRingHom) ≃ₐ[K]
117       ((C : PreorderClasses I) → Module.End K (LinearMap.range ((classPacketFamily P).proj C))) :=
118   Ideal.quotientKerAlgEquivOfSurjective (preorderDiagonalHom_surjective P)
119 
120 /-- The quotient by the explicitly constructed nilpotent two-sided ideal. -/
121 def preorderStrictIdealQuotientEquiv (P : LinearProjectorFamily K X I) :
122     (preorderSupportAlgebra P ⧸ (strictSupportIdeal P).asIdeal) ≃ₐ[K]
123       ((C : PreorderClasses I) → Module.End K (LinearMap.range ((classPacketFamily P).proj C))) := by
124   exact (Ideal.quotientEquivAlgOfEq K (preorderDiagonal_kernel_eq P).symm).trans
125     (preorderQuotientEquiv P)
126 
127 private theorem strictPath_map {A B : Type*} [Preorder A] [Preorder B]
128     (f : A → B) (hf : ∀ a b, a < b → f a < f b) {n : ℕ} {a b : A}
129     (h : StrictPath n a b) : StrictPath n (f a) (f b) := by
130   induction n generalizing b with
131   | zero => exact congrArg f h
132   | succ n ih =>
133     obtain ⟨c, hc, hcb⟩ := h
134     exact ⟨f c, ih hc, hf c b hcb⟩
135 
136 /-- Quotienting a preorder by mutual comparability preserves all strict path lengths. -/
137 theorem class_strict_path_lengths :
138     {n | ∃ a b : I, StrictPath n a b} =
139       {n | ∃ A B : PreorderClasses I, StrictPath n A B} := by
140   ext n
141   constructor
142   · rintro ⟨a,b,h⟩
143     exact ⟨packetClass a, packetClass b, strictPath_map packetClass
144       (fun _ _ hlt => toAntisymmetrization_lt_toAntisymmetrization_iff.mpr hlt) h⟩
145   · rintro ⟨A,B,h⟩
146     refine ⟨ofAntisymmetrization (· ≤ ·) A, ofAntisymmetrization (· ≤ ·) B,
147       strictPath_map (ofAntisymmetrization (· ≤ ·)) ?_ h⟩
148     intro C D hCD
149     apply toAntisymmetrization_lt_toAntisymmetrization_iff.mp
150     simpa only [toAntisymmetrization_ofAntisymmetrization] using hCD
151 
152 /-- The exponent is exactly one more than the height of the partial order of quotient classes. -/
153 theorem class_maximalStrictSteps : maximalStrictSteps I = maximalStrictSteps (PreorderClasses I) := by
154   unfold maximalStrictSteps
155   rw [class_strict_path_lengths]
156 
157 /-- Each quotient-class space is canonically the direct sum of its original packet spaces. -/
158 def preorderClassRangeEquiv (P : LinearProjectorFamily K X I) (C : PreorderClasses I) :
159     LinearMap.range ((classPacketFamily P).proj C) ≃ₗ[K]
160       DirectSum {i : I // packetClass i = C} (fun i => LinearMap.range (P.proj i.val)) :=
161   groupedRangeDirectSumEquiv P packetClass C
162 
163 /-- Direct-sum form of the quotient-algebra decomposition printed in Paper I. -/
164 def preorderQuotientDirectSumEquiv (P : LinearProjectorFamily K X I) :
165     (preorderSupportAlgebra P ⧸ (strictSupportIdeal P).asIdeal) ≃ₐ[K]
166       ((C : PreorderClasses I) → Module.End K
167         (DirectSum {i : I // packetClass i = C} (fun i => LinearMap.range (P.proj i.val)))) :=
168   (preorderStrictIdealQuotientEquiv P).trans
169     (AlgEquiv.piCongrRight fun C => (preorderClassRangeEquiv P C).conjAlgEquiv K)
170 
171 end Preorder
172 end Komorebi.PaperIRelease

Back to source controls