ConditionalAtomicComparison.lean

1 import PaperXI.FiniteBreakAssembly
2 import PaperXI.GluedPacketSections
3 import PaperXI.LocalFactorIdentification
4 
5 /-! The last comparison pipeline. Actual finite tensor intertwiners and global
6 parallel-section equivalences are constructed. Atom realization and normalized
7 pair-factor characterization remain explicit external interfaces. They are not
8 consequences of finite phases or of zero holonomy. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.ConditionalAtomicComparison
12 open Quiver GraphTransport GraphGauge GluedPacketSections LocalFactorIdentification
13 
14 variable {X K G V W : Type*} [Quiver X] [Field K] [Monoid G]
15 variable [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
16 
17 /-- A finite representation diagram retains all fibers and all transports.
18 Its space of parallel sections may be zero and is not identified with an atom. -/
19 structure Diagram (X K G V : Type*) [Quiver X] [Field K] [Monoid G]
20     [AddCommGroup V] [Module K V] where
21   action : X → Representation K G V
22   edge : ∀ {u v : X}, (u ⟶ v) → (V ≃ₗ[K] V)
23   covariance : RepresentationGraph.EdgeEquivariant edge action
24 
25 /-- Local actions and honest transport data. There is no root comparison map,
26 global gauge, global section equivalence, or atomic identification in this record. -/
27 structure Atlas (leftRoot : Representation K G V) (rightRoot : Representation K G W) where
28   root : X
29   connected : GraphTree.Connected (α := X)
30   left : X → Representation K G V
31   right : X → Representation K G W
32   left_root : left root = leftRoot
33   right_root : right root = rightRoot
34   sourceEdge : ∀ {u v : X}, (u ⟶ v) → (V ≃ₗ[K] V)
35   targetEdge : ∀ {u v : X}, (u ⟶ v) → (W ≃ₗ[K] W)
36   sourceCovariance : RepresentationGraph.EdgeEquivariant sourceEdge left
37   targetCovariance : RepresentationGraph.EdgeEquivariant targetEdge right
38 
39 variable {leftRoot : Representation K G V} {rightRoot : Representation K G W}
40 variable (a : Atlas (X := X) leftRoot rightRoot)
41 
42 def targetDiagram : Diagram X K G W :=
43   ⟨a.right, a.targetEdge, a.targetCovariance⟩
44 
45 def sourceDiagram : Diagram X K G V :=
46   ⟨a.left, a.sourceEdge, a.sourceCovariance⟩
47 
48 /-- Root action equality only transports the already constructed finite map. -/
49 def atRoot (U : Representation.Equiv leftRoot rightRoot) :
50     Representation.Equiv (a.left a.root) (a.right a.root) := by
51   refine Representation.Equiv.mk U.toLinearEquiv ?_
52   intro g
53   rw [a.left_root, a.right_root]
54   exact U.toIntertwiningMap.isIntertwining' g
55 
56 @[simp] theorem atRoot_linear (U : Representation.Equiv leftRoot rightRoot) :
57     (atRoot a U).toLinearEquiv = U.toLinearEquiv := rfl
58 
59 /-- The matrix obstruction is tested on actual fundamental cycles of a derived tree. -/
60 def Holonomy (U : V ≃ₗ[K] W) : Prop :=
61   ∀ e : GraphTree.Chord (GraphTree.ofConnected a.root a.connected),
62     CycleCompatible a.sourceEdge a.targetEdge U
63       (GraphTree.rootPath (GraphTree.ofConnected a.root a.connected)) e.val
64 
65 def leftSections := sectionRepresentation a.sourceEdge a.left a.sourceCovariance
66 
67 def rightSections := sectionRepresentation a.targetEdge a.right a.targetCovariance
68 
69 /-- A real equivalence of global section representations, not an assumed record field. -/
70 def glue (U : Representation.Equiv leftRoot rightRoot) (h : Holonomy a U.toLinearEquiv) :
71     Representation.Equiv (leftSections a) (rightSections a) :=
72   fromChords a.sourceEdge a.targetEdge a.left a.right a.connected
73     a.sourceCovariance a.targetCovariance (atRoot a U) h
74 
75 theorem glue_apply (U : Representation.Equiv leftRoot rightRoot) (h : Holonomy a U.toLinearEquiv)
76     (s : sections a.sourceEdge) (v : X) :
77     (glue a U h s).val v =
78       path a.targetEdge (GraphTree.rootPath (GraphTree.ofConnected a.root a.connected) v)
79         (U ((path a.sourceEdge (GraphTree.rootPath (GraphTree.ofConnected a.root a.connected) v)).symm
80           (s.val v))) := rfl
81 
82 /-- Matrix holonomy is necessary as well as sufficient for the based gauge.
83 A scalar determinant, trace, or projective cycle test is not substituted. -/
84 theorem holonomy_iff_gauge (U : Representation.Equiv leftRoot rightRoot) :
85     Holonomy a U.toLinearEquiv ↔
86       ∃ F : X → V ≃ₗ[K] W,
87         F a.root = U.toLinearEquiv ∧ EdgeCompatible a.sourceEdge a.targetEdge F ∧
88           RepresentationGraph.Intertwines a.left a.right F := by
89   exact (RepresentationGraph.connected_iff_chords a.sourceEdge a.targetEdge
90     a.left a.right a.sourceCovariance a.targetCovariance (atRoot a U).toLinearEquiv
91     (fun g x => DFunLike.congr_fun ((atRoot a U).toIntertwiningMap.isIntertwining' g) x) a.connected).symm
92 
93 section Source
94 variable {I Z C : Type*} [Fintype I] [CommGroup Z] [Group C]
95 variable {H A H' A' Vb Wb : I → Type*}
96 variable [∀ i, Group (H i)] [∀ i, CommGroup (A i)] [∀ i, Fintype (A i)]
97 variable [∀ i, Group (H' i)] [∀ i, CommGroup (A' i)]
98 variable [∀ i, AddCommGroup (Vb i)] [∀ i, Module ℂ (Vb i)]
99 variable [∀ i, AddCommGroup (Wb i)] [∀ i, Module ℂ (Wb i)]
100 
101 variable (d : FiniteBreakAssembly.Data (I := I) (Z := Z) (H := H) (A := A)
102   (H' := H') (A' := A') (V := Vb) (W := Wb))
103 variable (α : C →* MulAut (CentralProduct.Group d.source))
104 variable (R : Representation ℂ C (PiTensorProduct ℂ Vb))
105 variable (T : Representation ℂ C (PiTensorProduct ℂ Wb))
106 variable (hR : ∀ g h x, R g (FiniteBreakAssembly.sourceAction d h x) =
107   FiniteBreakAssembly.sourceAction d (α g h) (R g x))
108 variable (hT : ∀ g h x, T g (FiniteBreakAssembly.targetAction d h x) =
109   FiniteBreakAssembly.targetAction d (α g h) (T g x))
110 variable (S : Set C) (hgen : Subgroup.closure S = ⊤)
111 variable (hp : ∀ g ∈ S, FiniteBreakAssembly.discrepancy d α R T hR hT g = 1)
112 variable (a0 : Atlas (X := X)
113   (CyclicBridge.semidirectRepresentation α (FiniteBreakAssembly.sourceAction d) R hR)
114   (CyclicBridge.semidirectRepresentation α (FiniteBreakAssembly.targetAction d) T hT))
115 variable (hhol : Holonomy a0 (FiniteBreakAssembly.tensorBridge d))
116 
117 /-- Source finite endpoint: the root tensor map and the global section bridge
118 are both constructed from the phase, lift and graph data. -/
119 def finiteComparison : Representation.Equiv (leftSections a0) (rightSections a0) :=
120   glue a0 (FiniteBreakAssembly.equivOfPhase d α R T hR hT S hgen hp) hhol
121 
122 include hgen hp hhol in
123 /-- Theorem 16.2 at explicit arithmetic interfaces. The permitted finite data
124 are represented by a subtype; no realization of arbitrary finite data is asserted.
125 The output includes the concrete finite equivalence AND equality of realized
126 atom classes. There is no assumed finite bridge or final atom equality. -/
127 theorem source {Atom Test Value : Type*} {atomIso : Setoid Atom}
128     (sys : FactorSystem atomIso Test Value)
129     (allowed : Set (Diagram X ℂ (CentralProduct.Group d.source ⋊[α] C)
130       (PiTensorProduct ℂ Wb)))
131     (ha : targetDiagram a0 ∈ allowed)
132     (realization : Realization sys allowed)
133     (reference : Atom) (href : sys.admissible reference)
134     (expected : Test → Value)
135     (hfactors : ∀ b, realization.realizes ⟨targetDiagram a0, ha⟩ b →
136       sys.profile b = expected)
137     (hreference : sys.profile reference = expected) :
138     (∃ F : X → PiTensorProduct ℂ Vb ≃ₗ[ℂ] PiTensorProduct ℂ Wb,
139       F a0.root = FiniteBreakAssembly.tensorBridge d ∧
140       EdgeCompatible a0.sourceEdge a0.targetEdge F ∧
141       RepresentationGraph.Intertwines a0.left a0.right F) ∧
142     Nonempty (Representation.Equiv (leftSections a0) (rightSections a0)) ∧
143       candidate sys realization ⟨targetDiagram a0, ha⟩ = Quotient.mk atomIso reference := by
144   refine ⟨?_, ⟨finiteComparison d α R T hR hT S hgen hp a0 hhol⟩,
145     candidate_eq_reference sys realization ⟨targetDiagram a0, ha⟩ reference
146       href expected hfactors hreference⟩
147   exact (holonomy_iff_gauge a0
148     (FiniteBreakAssembly.equivOfPhase d α R T hR hT S hgen hp)).mp hhol
149 
150 end Source
151 end PaperXI.ConditionalAtomicComparison

Back to source controls