FiniteCommonRefinement.lean

1 import KomorebiVerification.PaperII.CommonRefinement
2 
3 /-!
4 # Finite collections of commuting packet systems
5 
6 A finite-list induction constructs the coarsest common refinement by supported
7 binary products. The empty list uses the supported identity family. In a zero
8 module this support is empty, rather than containing a forbidden zero packet.
9 -/
10 
11 set_option autoImplicit false
12 noncomputable section
13 namespace Komorebi.PaperII.CommonRefinement
14 
15 open Komorebi.Foundation Komorebi.PaperII.NestedRefinement
16 
17 universe u v w z
18 variable {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M]
19 
20 /-- A finite, zero-free packet system with its actual index type. -/
21 structure Packet (R : Type u) (M : Type v)
22     [Semiring R] [AddCommMonoid M] [Module R M] where
23   Index : Type w
24   indexFintype : Fintype Index
25   family : @LinearProjectorFamily R M Index _ _ _ indexFintype
26   nonzero : @Nonzero R M _ _ _ Index indexFintype family
27 
28 attribute [instance] Packet.indexFintype
29 
30 /-- The second packet is a refinement of the first, using the inherited relation. -/
31 def HasRefinement (P S : Packet.{u,v,w} R M) : Prop :=
32   ∃ parent : S.Index → P.Index, Refines P.family S.family parent
33 
34 theorem refinement_trans (P Q S : Packet.{u,v,w} R M)
35     (hp : HasRefinement P Q) (hq : HasRefinement Q S) : HasRefinement P S := by
36   rcases hp with ⟨p, hp⟩
37   rcases hq with ⟨q, hq⟩
38   exact ⟨p ∘ q, hp.trans hq⟩
39 
40 /-- The binary meet constructs its own index subtype and both projector axioms. -/
41 def meetPacket (P Q : Packet.{u,v,w} R M)
42     (h : CrossCommutes P.family Q.family) : Packet.{u,v,w} R M where
43   Index := Support (product P.family Q.family h)
44   indexFintype := inferInstance
45   family := common P.family Q.family h
46   nonzero := supported_nonzero _
47 
48 theorem meet_left (P Q : Packet.{u,v,w} R M)
49     (h : CrossCommutes P.family Q.family) : HasRefinement P (meetPacket P Q h) :=
50   ⟨fun k => k.val.1, common_refines_left P.family Q.family h P.nonzero⟩
51 
52 theorem meet_right (P Q : Packet.{u,v,w} R M)
53     (h : CrossCommutes P.family Q.family) : HasRefinement Q (meetPacket P Q h) :=
54   ⟨fun k => k.val.2, common_refines_right P.family Q.family h Q.nonzero⟩
55 
56 theorem meet_coarsest (P Q S : Packet.{u,v,w} R M)
57     (h : CrossCommutes P.family Q.family)
58     (hp : HasRefinement P S) (hq : HasRefinement Q S) :
59     HasRefinement (meetPacket P Q h) S := by
60   rcases hp with ⟨p, hp⟩
61   rcases hq with ⟨q, hq⟩
62   exact ⟨jointParent P.family Q.family h S.family S.nonzero p q hp hq,
63     common_coarsest P.family Q.family h S.family S.nonzero p q hp hq⟩
64 
65 theorem cross_symm (P Q : Packet.{u,v,w} R M)
66     (h : CrossCommutes P.family Q.family) : CrossCommutes Q.family P.family :=
67   fun j i x => (h i j x).symm
68 
69 theorem cross_self (P : Packet.{u,v,w} R M) : CrossCommutes P.family P.family := by
70   intro i j x
71   by_cases h : i = j
72   · subst j
73     rfl
74   · rw [P.family.orthogonal h, P.family.orthogonal (Ne.symm h)]
75 
76 /-- A product of two families commuting with a third still commutes with it. -/
77 theorem meet_cross (P Q S : Packet.{u,v,w} R M)
78     (h : CrossCommutes P.family Q.family)
79     (hp : CrossCommutes P.family S.family) (hq : CrossCommutes Q.family S.family) :
80     CrossCommutes (meetPacket P Q h).family S.family := by
81   intro k j x
82   change P.family.proj k.val.1 (Q.family.proj k.val.2 (S.family.proj j x)) =
83     S.family.proj j (P.family.proj k.val.1 (Q.family.proj k.val.2 x))
84   rw [hq k.val.2 j x, hp k.val.1 j (Q.family.proj k.val.2 x)]
85 
86 /-- A single identity before zero removal, valid even on the zero module. -/
87 def oneFamily : LinearProjectorFamily R M (ULift.{w} Unit) where
88   proj _ := LinearMap.id
89   idempotent := by intros; rfl
90   orthogonal := by
91     intro i j h
92     exact False.elim (h (Subsingleton.elim i j))
93   complete := by intro x; simp
94 
95 /-- The actual empty-family meet: identity on a nonzero module, empty on a zero module. -/
96 def identityPacket : Packet.{u,v,w} R M where
97   Index := Support (oneFamily (R := R) (M := M))
98   indexFintype := inferInstance
99   family := supported oneFamily
100   nonzero := supported_nonzero _
101 
102 theorem identity_cross (P : Packet.{u,v,w} R M) :
103     CrossCommutes (identityPacket (R := R) (M := M)).family P.family := by
104   intro i j x
105   rfl
106 
107 /-- Every zero-free packet system refines the supported identity family. -/
108 theorem identity_coarsest (P : Packet.{u,v,w} R M) :
109     HasRefinement (identityPacket (R := R) (M := M)) P := by
110   classical
111   let parent : P.Index → Support (oneFamily (R := R) (M := M)) := fun a =>
112     ⟨ULift.up (), by
113       intro hz
114       have hz' : ∀ x : M, x = 0 := by
115         intro x
116         exact LinearMap.congr_fun hz x
117       exact P.nonzero a (by ext x; exact hz' _)⟩
118   refine ⟨parent, refines_of_absorption _ P.family (supported_nonzero _) parent ?_⟩
119   intro i a x
120   have hi : parent a = i := Subtype.ext (Subsingleton.elim _ _)
121   simp only [hi, ↓reduceIte]
122   rfl
123 
124 /-- Binary existence is equivalent to cross commutation; no host is assumed. -/
125 theorem exists_common_iff (P Q : Packet.{u,v,w} R M) :
126     (∃ S : Packet.{u,v,w} R M, HasRefinement P S ∧ HasRefinement Q S) ↔
127       CrossCommutes P.family Q.family := by
128   constructor
129   · rintro ⟨S, ⟨p, hp⟩, ⟨q, hq⟩⟩
130     exact commutes_of_common_refinement P.family Q.family S.family p q hp hq
131   · intro h
132     exact ⟨meetPacket P Q h, meet_left P Q h, meet_right P Q h⟩
133 
134 /-- Construct a coarsest common refinement for a finite list, allowing repeats. -/
135 theorem list_common_coarsest {T : Type z} (F : T → Packet.{u,v,w} R M)
136     (hc : ∀ s t, CrossCommutes (F s).family (F t).family) (l : List T) :
137     ∃ S : Packet.{u,v,w} R M,
138       (∀ t, CrossCommutes S.family (F t).family) ∧
139       (∀ t ∈ l, HasRefinement (F t) S) ∧
140       (∀ U : Packet.{u,v,w} R M,
141         (∀ t ∈ l, HasRefinement (F t) U) → HasRefinement S U) := by
142   induction l with
143   | nil =>
144     refine ⟨identityPacket, ?_, ?_, ?_⟩
145     · intro t
146       exact identity_cross (F t)
147     · intro t ht
148       simp only [List.not_mem_nil] at ht
149     · intro U _
150       exact identity_coarsest U
151   | cons t l ih =>
152     rcases ih with ⟨S, hs, hr, hu⟩
153     let h : CrossCommutes (F t).family S.family := cross_symm S (F t) (hs t)
154     refine ⟨meetPacket (F t) S h, ?_, ?_, ?_⟩
155     · intro s
156       exact meet_cross (F t) S (F s) h (hc t s) (hs s)
157     · intro s hsl
158       rcases List.mem_cons.mp hsl with hst | hsl
159       · subst s
160         exact meet_left (F t) S h
161       · exact refinement_trans (F s) S _ (hr s hsl) (meet_right (F t) S h)
162     · intro U hU
163       exact meet_coarsest (F t) S U h (hU t (by simp))
164         (hu U (fun s hsl => hU s (List.mem_cons_of_mem t hsl)))
165 
166 /-- The finite-family part of the manuscript theorem, together with its universal property. -/
167 theorem finite_common_coarsest {T : Type z} [Fintype T]
168     (F : T → Packet.{u,v,w} R M)
169     (hc : ∀ s t, s ≠ t → CrossCommutes (F s).family (F t).family) :
170     ∃ S : Packet.{u,v,w} R M,
171       (∀ t, HasRefinement (F t) S) ∧
172       (∀ U : Packet.{u,v,w} R M,
173         (∀ t, HasRefinement (F t) U) → HasRefinement S U) := by
174   classical
175   have hc' : ∀ s t, CrossCommutes (F s).family (F t).family := by
176     intro s t
177     by_cases h : s = t
178     · subst t
179       exact cross_self (F s)
180     · exact hc s t h
181   obtain ⟨S, _, hr, hu⟩ := list_common_coarsest F hc' Finset.univ.toList
182   refine ⟨S, ?_, ?_⟩
183   · intro t
184     exact hr t (by simp)
185   · intro U hU
186     exact hu U (fun t _ => hU t)
187 
188 end Komorebi.PaperII.CommonRefinement

Back to source controls