Source: ProCGroups.FoxDifferential.Completed.Continuous.Free.SourceFormula
1import ProCGroups.FoxDifferential.Completed.Continuous.Free.Continuity
3/-!
4# Fox differential: completed — continuous — free — source formula
6The principal declarations in this module are:
8- `freeProCZCCompletedFoxBoundary_of_continuousCrossedDifferential`
9 Source-shaped completed Fox boundary formula for continuous crossed differentials out of a free
10 pro-\(C\) source.
11-/
13namespace FoxDifferential
15noncomputable section
17open scoped BigOperators
19universe u
22variable {C : ProCGroups.FiniteGroupClass.{u}}
23variable (X H : Type u) [DecidableEq X]
24variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
27variable {F : Type u}
28variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
29variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
30variable [TopologicalSpace X]
32section SourceFormula
34variable [Fintype X]
35variable [CompactSpace (ZCCompletedFoxSemidirect C PUnit.{u + 1} H)]
36variable [T2Space (ZCCompletedFoxSemidirect C PUnit.{u + 1} H)]
37variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C PUnit.{u + 1} H)]
39/--
40Source-shaped completed Fox boundary formula for continuous crossed differentials out of a free
41pro-\(C\) source.
42-/
43theorem freeProCZCCompletedFoxBoundary_of_continuousCrossedDifferential
44 {ι : X → F}
45 (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
46 (htargetUnit :
47 ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C PUnit H))
48 (ψ : F →* H)
49 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
50 (ZCFreeFoxCoordinates C (X := X) (H := H)))
51 (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
52 (hbasis :
53 ∀ x : X, delta (ι x) =
54 Pi.single x (1 : ZCCompletedGroupAlgebra C H))
55 (g : F) :
56 freeProCZCCompletedFoxBoundary C (fun x : X => ψ (ι x))
57 (delta g) =
58 zcCompletedGroupAlgebraBoundary C ψ g := by
59 let toPUnitCoordinates :
60 ZCCompletedGroupAlgebra C H →ₗ[ZCCompletedGroupAlgebra C H]
61 ZCFreeFoxCoordinates C (X := PUnit) (H := H) :=
62 { toFun := fun a _ => a
63 map_add' := fun _ _ => rfl
64 map_smul' := fun _ _ => rfl }
65 let beta :
66 ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
67 (ZCCompletedGroupAlgebra C H) :=
68 delta.mapLinear
69 (freeProCZCCompletedFoxBoundary C (fun x : X => ψ (ι x)))
70 let betaVec :
71 ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
72 (ZCFreeFoxCoordinates C (X := PUnit) (H := H)) :=
73 beta.mapLinear toPUnitCoordinates
74 let boundaryVec :
75 ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
76 (ZCFreeFoxCoordinates C (X := PUnit) (H := H)) :=
77 (coefficientFoxBoundaryCrossedHom
78 (zcCompletedGroupAlgebraScalar C ψ)).mapLinear toPUnitCoordinates
79 have hbeta_continuous : Continuous beta := by
80 exact (continuous_freeProCZCCompletedFoxBoundary C
81 (fun x : X => ψ (ι x))).comp hdelta_continuous
82 have hbetaVec_continuous : Continuous betaVec := by
83 exact continuous_pi fun _ => hbeta_continuous
84 have hboundary_continuous :
85 Continuous (zcCompletedGroupAlgebraBoundary C ψ) :=
86 continuous_zcCompletedGroupAlgebraBoundary
87 (C := C) (G := H) ψ hψ_continuous
88 have hboundaryVec_continuous : Continuous boundaryVec := by
89 exact continuous_pi fun _ => hboundary_continuous
90 let f : F →* ZCCompletedFoxSemidirect C PUnit H :=
91 freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
92 (C := C) (X := PUnit) (F := F) (H := H) ψ betaVec
93 let h : F →* ZCCompletedFoxSemidirect C PUnit H :=
94 freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
95 (C := C) (X := PUnit) (F := F) (H := H) ψ boundaryVec
96 have hf_continuous : Continuous f :=
97 continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
98 (C := C) (X := PUnit) (F := F) (H := H)
99 ψ betaVec hbetaVec_continuous hψ_continuous
100 have hh_continuous : Continuous h :=
101 continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
102 (C := C) (X := PUnit) (F := F) (H := H) ψ boundaryVec
103 hboundaryVec_continuous hψ_continuous
104 have hgen : ∀ x : X, f (ι x) = h (ι x) := by
105 intro x
106 apply ZCCompletedFoxSemidirect.ext
107 · funext u
108 simp only [freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential_left,
109 ScalarCrossedHom.mapLinear_apply, hbasis x,
110 freeProCZCCompletedFoxBoundary_single,
111 coefficientFoxBoundaryCrossedHom_apply,
112 zcCompletedGroupAlgebraScalar_apply, f, betaVec, beta, h, boundaryVec,
113 toPUnitCoordinates]
114 · rfl
115 have hfh : f = h := hι.hom_ext htargetUnit hf_continuous hh_continuous hgen
116 have hleft := congrArg
117 (fun q : F →* ZCCompletedFoxSemidirect C PUnit H =>
118 (q g).left PUnit.unit) hfh
119 convert hleft using 1
120 all_goals
121 simp [f, h, betaVec, boundaryVec, beta, toPUnitCoordinates,
122 zcCompletedGroupAlgebraBoundary]
123 all_goals rfl
125end SourceFormula
129end
131end FoxDifferential