Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates.Comparison
ProCGroups/FoxDifferential/Completed/Continuous/ClosedGeneratedCoordinates/Comparison/Source

Source: ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates.Comparison

1import ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates.Equiv
2import ProCGroups.FoxDifferential.Completed.Continuous.SemidirectKernelBasis
4/-!
5# Fox differential: completed — continuous — closed generated coordinates — comparison
7The principal declarations in this module are:
9- `continuous_familyCoordinatesZC_zcUnivDiff_of_closedGen_leftGraph`
10 The paper coordinate universal differential is continuous once it is identified with the
11 closed-generated completed Fox derivative vector.
12- `freeProCZCCompletedFoxDerivativeVectorViaClosedGen_eq_presentedCoordinates_zcUnivDiff`
13 The left coordinate of the closed-generated completed Fox graph agrees with the paper coordinate
14 universal differential.
15-/
17namespace CrowellExactSequence
19noncomputable section
21open FoxDifferential
22open ProCGroups.ProC
23open ProCGroups.Completion
24open ProCGroups.InverseSystems
26universe u v
28variable {G H : Type u}
29variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
30variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
32/--
33The paper coordinate universal differential is continuous once it is identified with the
34closed-generated completed Fox derivative vector.
35-/
36theorem continuous_familyCoordinatesZC_zcUnivDiff_of_closedGen_leftGraph
37 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
38 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
39 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
40 {X : Type u} [Fintype X] [DecidableEq X] (family : X → G)
41 (hbasis_A :
42 IsPresentedCompletedDifferentialFamilyBasisProCInteger
43 (G := G) (H := H) C psi family)
44 (hfree :
46 (C := C) X G family)
47 (htarget :
48 HasOpenNormalBasisInClass C
49 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
50 (C := C) (fun i : X => psi (family i)) : Subgroup
51 (ZCCompletedFoxSemidirect C X H)))
52 (hφconv :
54 (G :=
55 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
56 (C := C) (fun i : X => psi (family i)) : Subgroup
57 (ZCCompletedFoxSemidirect C X H)))
58 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator
59 (C := C) (fun i : X => psi (family i))))
60 (hleft_graph_eq :
61 ∀ g : G,
62 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
63 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g =
64 presentedCompletedDifferentialFamilyCoordinatesProCInteger
65 (G := G) (H := H) C psi family hbasis_A
66 (zcUniversalDifferential C psi.toMonoidHom g)) :
67 Continuous
68 (fun g : G =>
69 presentedCompletedDifferentialFamilyCoordinatesProCInteger
70 (G := G) (H := H) C psi family hbasis_A
71 (zcUniversalDifferential C psi.toMonoidHom g)) := by
72 let Dclosed : G → ZCFreeFoxCoordinates C (X := X) (H := H) :=
73 fun g =>
74 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
75 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g
76 have hclosed_continuous : Continuous Dclosed := by
77 simpa [Dclosed] using
78 continuous_freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
79 (C := C) X H hfree (fun i : X => psi (family i)) htarget hφconv
80 have hcoords_eq :
81 (fun g : G =>
82 presentedCompletedDifferentialFamilyCoordinatesProCInteger
83 (G := G) (H := H) C psi family hbasis_A
84 (zcUniversalDifferential C psi.toMonoidHom g)) = Dclosed := by
85 funext g
86 exact (hleft_graph_eq g).symm
87 rw [hcoords_eq]
88 exact hclosed_continuous
90/--
91The left coordinate of the closed-generated completed Fox graph agrees with the paper
92coordinate universal differential.
93-/
94theorem freeProCZCCompletedFoxDerivativeVectorViaClosedGen_eq_presentedCoordinates_zcUnivDiff
95 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
96 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
97 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
98 {X : Type u} [Fintype X] [DecidableEq X] (family : X → G)
99 (hbasis_A :
100 IsPresentedCompletedDifferentialFamilyBasisProCInteger
101 (G := G) (H := H) C psi family)
102 (hfree :
104 (C := C) X G family)
106 (htarget :
107 HasOpenNormalBasisInClass C
108 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
109 (C := C) (fun i : X => psi (family i)) : Subgroup
110 (ZCCompletedFoxSemidirect C X H)))
111 (hφconv :
113 (G :=
114 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
115 (C := C) (fun i : X => psi (family i)) : Subgroup
116 (ZCCompletedFoxSemidirect C X H)))
117 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator
118 (C := C) (fun i : X => psi (family i))))
119 (hφHconv :
121 (G := H) (fun i : X => psi (family i)))
122 (hφHgen :
124 (G := H) (Set.range (fun i : X => psi (family i)))) :
125 ∀ g : G,
126 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
127 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g =
128 presentedCompletedDifferentialFamilyCoordinatesProCInteger
129 (G := G) (H := H) C psi family hbasis_A
130 (zcUniversalDifferential C psi.toMonoidHom g) := by
131 let coords :=
132 presentedCompletedDifferentialFamilyCoordinatesProCInteger
133 (G := G) (H := H) C psi family hbasis_A
134 let f :
135 (X → ZCCompletedGroupAlgebra C H) →ₗ[
136 ZCCompletedGroupAlgebra C H]
137 ZCCompletedDifferentialModule C psi.toMonoidHom :=
138 presentedCompletedDifferentialFamilyMapProCInteger
139 (G := G) (H := H) C psi family
140 let L :
141 ZCCompletedDifferentialModule C psi.toMonoidHom →ₗ[
142 ZCCompletedGroupAlgebra C H]
143 ZCFreeFoxCoordinates C (X := X) (H := H) :=
144 closedGeneratedDerivativeCoordinatesLinearMapProCInteger
145 (G := G) (H := H) C psi family hfree htarget hφconv hH hφHconv hφHgen
146 have hL_comp : L.comp f = LinearMap.id := by
147 exact
148 closedGeneratedDerivativeCoordinatesLinearMapProCInteger_comp_familyMap
149 (G := G) (H := H) C psi family hfree htarget hφconv hH hφHconv hφHgen
150 have hL_eq_coords : L = coords.toLinearMap := by
151 exact
152 presentedCompletedDifferentialFamilyCoordinatesProCInteger_eq_of_leftInverse
153 (G := G) (H := H) C psi family hbasis_A L hL_comp
154 intro g
155 calc
156 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
157 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g =
158 L (zcUniversalDifferential C psi.toMonoidHom g) := by
159 rw [closedGeneratedDerivativeCoordinatesLinearMapProCInteger_universal
160 (G := G) (H := H) C psi family hfree htarget hφconv hH hφHconv hφHgen g]
161 _ = coords
162 (zcUniversalDifferential C psi.toMonoidHom g) := by
163 rw [hL_eq_coords]
164 rfl
166end
168end CrowellExactSequence