CrowellExactSequence.presentedCompletedToZC_eq_boundary_comp_closedGenCoords
On the genuine \(A_{\psi}(C)\), the Crowell boundary is obtained by first reading the closed-generated Fox coordinates and then applying the completed Fox boundary.
Source context 18 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
universe u v w
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section ClosedGeneratedCoordinates
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (psi : ContinuousMonoidHom G H)
variable {X : Type u} [Fintype X] [DecidableEq X]
variable (family : X → G)
variable
(hfree :
ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet
(C := C) X G family)
variable
(htarget :
ProCGroups.ProC.HasOpenNormalBasisInClass C
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(C := C) (fun i : X => psi (family i)) : Subgroup
(ZCCompletedFoxSemidirect C X H)))
variable
(hφconv :
ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(C := C) (fun i : X => psi (family i)) : Subgroup
(ZCCompletedFoxSemidirect C X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator
(C := C) (fun i : X => psi (family i))))Lean source · full declaration
theorem presentedCompletedToZC_eq_boundary_comp_closedGenCoords
(hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
(hφHconv :
ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
(G := H) (fun i : X => psi (family i)))
(hφHgen :
ProCGroups.Generation.TopologicallyGenerates
(G := H) (Set.range (fun i : X => psi (family i)))) :
presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
(G := G) (H := H) C psi =
(freeProCZCCompletedFoxBoundary C
(fun i : X => psi (family i))).comp
(closedGeneratedDerivativeCoordinatesLinearMapProCInteger
(G := G) (H := H) C psi family hfree htarget hφconv
hH hφHconv hφHgen) := by
apply
crossedDifferentialModuleHom_ext
(zcCompletedGroupAlgebraScalar C psi.toMonoidHom)
intro g
change
presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
(G := G) (H := H) C psi
(zcUniversalDifferential C psi.toMonoidHom g) =
((freeProCZCCompletedFoxBoundary C
(fun i : X => psi (family i))).comp
(closedGeneratedDerivativeCoordinatesLinearMapProCInteger
(G := G) (H := H) C psi family hfree htarget hφconv
hH hφHconv hφHgen))
(zcUniversalDifferential C psi.toMonoidHom g)
rw [presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger_d,
LinearMap.comp_apply,
closedGeneratedDerivativeCoordinatesLinearMapProCInteger_universal]
have hright :
freeProCZCCompletedFoxRightHomViaClosedGenerated
(C := C) hfree (fun i : X => psi (family i)) htarget hφconv =
psi.toMonoidHom :=
freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_continuousHom
(C := C) X H hfree hH (fun i : X => psi (family i)) htarget hφconv
hφHconv hφHgen psi (by intro i; rfl)
let delta : ScalarCrossedHom
(zcCompletedGroupAlgebraScalar C psi.toMonoidHom)
(ZCFreeFoxCoordinates C (X := X) (H := H)) :=
{ toFun := fun g =>
freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(C := C) hfree (fun i : X => psi (family i)) htarget hφconv g
map_mul' := by
intro a b
rw [← hright]
exact
ScalarCrossedHom.map_mul
(freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(C := C) hfree (fun i : X => psi (family i)) htarget hφconv)
a b }
exact
(freeProCZCBoundary_of_topologicalGeneration
C hfree.generates_range psi.toMonoidHom
delta
(by
change Continuous
(fun g : G =>
freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(C := C) hfree (fun i : X => psi (family i)) htarget hφconv g)
exact
continuous_freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(C := C) X H hfree (fun i : X => psi (family i)) htarget hφconv)
psi.continuous_toFun
(by
intro i
change
freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(C := C) hfree (fun i : X => psi (family i)) htarget hφconv
(family i) =
Pi.single i (1 : ZCCompletedGroupAlgebra C H)
exact
freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated_generator
(C := C) hfree (fun i : X => psi (family i)) htarget hφconv i)
g).symm