ProCGroups.FoxDifferential.Completed.FiniteStage.ClosedGeneratedCycles
The principal declarations in this module are:
freeProCZCBifilteredAllFiniteQuotientStageCoeffMap_additive_basisThe bifiltered coefficient maps form an additive identity-quotient kernel neighbourhood basis. -freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_zcBiAllStages_coeffGraphRelDerivIf all coefficient-stage graph relations vanish, every completed Fox boundary cycle lies in the closed subgroup generated by the graph elements.
imports
theorem freeProCZCBifilteredAllFiniteQuotientStageCoeffMap_additive_basis
{C : ProCGroups.FiniteGroupClass.{u}} (hForm : ProCGroups.FiniteGroupClass.Formation C)
{X H : Type u}
[Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(φ : X → H)
(hφgen :
ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :
HasAdditiveIdentityQuotientKernelNeighbourhoodBasis
(A := ZCCompletedGroupAlgebra C H)
(fun j : ZCCompletedGroupAlgebraIndex C H =>
(freeProCZCBifilteredAllFiniteQuotientStageCoeffMap
(C := C) (X := X) (H := H) φ hφgen j).toAddMonoidHom)The bifiltered coefficient maps form an additive identity-quotient kernel neighbourhood basis.
Show Lean proof
by
classical
letI : ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C :=
hForm.containsTrivialQuotients
letI : Nonempty (ZCCompletedGroupAlgebraIndex C H) :=
⟨(ProCIntegerIndex.terminal (C := C) inferInstance,
zcCompletedGroupAlgebraTopIndex C H)⟩
let S := zcCompletedGroupAlgebraSystem C H
have hdir :
Directed (· ≤ ·) (id : ZCCompletedGroupAlgebraIndex C H →
ZCCompletedGroupAlgebraIndex C H) :=
directed_zcCompletedGroupAlgebraIndex_of_formation
(C := C) (H := H) hForm
intro U hU hUzero
rcases S.exists_projection_preimage_subset hdir hU hUzero with
⟨j, V, _hVopen, hzeroV, hpre⟩
refine ⟨j, ?_⟩
intro z hz
apply hpre
change zcCompletedGroupAlgebraProjection C H j z ∈ V
letI :
∀ j : ZCCompletedGroupAlgebraIndex C H,
DiscreteTopology
(CompletedGroupAlgebraQuotientInClass H C j.2) :=
fun j =>
QuotientGroup.discreteTopology
(ProCGroups.openNormalSubgroup_isOpen (G := H)
((OrderDual.ofDual j.2).1 : OpenNormalSubgroup H))
have hqmap_inj :
Function.Injective
(freeProCFiniteQuotientStageQMapFamily
(C := C) φ
(id : ZCCompletedGroupAlgebraIndex C H →
ZCCompletedGroupAlgebraIndex C H) hφgen j) := by
exact
freeProCFiniteQuotientStageQMapFamily_injective
(C := C) φ
(id : ZCCompletedGroupAlgebraIndex C H →
ZCCompletedGroupAlgebraIndex C H) hφgen j
have hstage_inj :
Function.Injective
(zcCompletedGroupAlgebraStageToFoxAlgebraicStage
(C := C) (X := X) (H := H)
(freeProCFiniteQuotientStageKernelFamily
(C := C) φ
(id : ZCCompletedGroupAlgebraIndex C H →
ZCCompletedGroupAlgebraIndex C H) j)
j.1.modulus j dvd_rfl
(freeProCFiniteQuotientStageQMapFamily
(C := C) φ
(id : ZCCompletedGroupAlgebraIndex C H →
ZCCompletedGroupAlgebraIndex C H) hφgen j)) := by
exact
zcCompletedGroupAlgebraStageToFoxAlgebraicStage_self_injective
(C := C) (X := X) (H := H)
(freeProCFiniteQuotientStageKernelFamily
(C := C) φ
(id : ZCCompletedGroupAlgebraIndex C H →
ZCCompletedGroupAlgebraIndex C H) j)
j
(freeProCFiniteQuotientStageQMapFamily
(C := C) φ
(id : ZCCompletedGroupAlgebraIndex C H →
ZCCompletedGroupAlgebraIndex C H) hφgen j)
hqmap_inj
have hzstage :
zcCompletedGroupAlgebraProjection C H j z = 0 := by
let stageMap :=
zcCompletedGroupAlgebraStageToFoxAlgebraicStage
(C := C) (X := X) (H := H)
(freeProCFiniteQuotientStageKernelFamily
(C := C) φ
(id : ZCCompletedGroupAlgebraIndex C H →
ZCCompletedGroupAlgebraIndex C H) j)
j.1.modulus j dvd_rfl
(freeProCFiniteQuotientStageQMapFamily
(C := C) φ
(id : ZCCompletedGroupAlgebraIndex C H →
ZCCompletedGroupAlgebraIndex C H) hφgen j)
have hstage_inj' : Function.Injective stageMap := hstage_inj
have hzmap := hz
simp only [freeProCZCBifilteredAllFiniteQuotientStageCoeffMap,
freeProCZCBifilteredFiniteQuotientStageCoeffMap,
zcCompletedGroupAlgebraBifilteredStageCoeffMap,
zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap] at hzmap
change
stageMap (zcCompletedGroupAlgebraProjection C H j z) = 0 at hzmap
apply hstage_inj'
rw [hzmap, map_zero]
rw [hzstage]
exact hzeroVtheorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_zcBiAllStages_coeffGraphRelDeriv
{C : ProCGroups.FiniteGroupClass.{u}} (hForm : ProCGroups.FiniteGroupClass.Formation C)
{X H : Type u} [Fintype X] [DecidableEq X]
[Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(φ : X → H)
(hHbasis : HasOpenNormalBasisInClass C H)
(hφgen :
ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(C := C) φ : Subgroup
(ZCCompletedFoxSemidirect C X H)) : Set
(ZCCompletedFoxSemidirect C X H))If all coefficient-stage graph relations vanish, every completed Fox boundary cycle lies in the closed subgroup generated by the graph elements.
Show Lean proof
by
letI : ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C :=
hForm.containsTrivialQuotients
letI : Nonempty (ZCCompletedGroupAlgebraIndex C H) :=
⟨(ProCIntegerIndex.terminal (C := C) inferInstance,
zcCompletedGroupAlgebraTopIndex C H)⟩
letI :
∀ j : ZCCompletedGroupAlgebraIndex C H,
Fact (0 < j.1.modulus) :=
fun j => ProCIntegerIndex.positiveFact j.1
letI :
∀ j : ZCCompletedGroupAlgebraIndex C H,
DiscreteTopology
(CompletedGroupAlgebraQuotientInClass H C j.2) :=
fun j =>
QuotientGroup.discreteTopology
(ProCGroups.openNormalSubgroup_isOpen (G := H)
((OrderDual.ofDual j.2).1 : OpenNormalSubgroup H))
let J := ZCCompletedGroupAlgebraIndex C H
let Nstage : J → Subgroup (FreeGroup X) :=
freeProCFiniteQuotientStageKernelFamily
(C := C) φ
(id : J → J)
let nstage : J → ℕ := fun j => j.1.modulus
let zcIndex : J → ZCCompletedGroupAlgebraIndex C H := id
let qmap : ∀ j : J,
CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2 →*
foxAlgebraicStageTargetQuotient (X := X) (Nstage j) :=
freeProCFiniteQuotientStageQMapFamily
(C := C) φ
(id : J → J) hφgen
have hdir : Directed (· ≤ ·) (id : J → J) :=
directed_zcCompletedGroupAlgebraIndex_of_formation
(C := C) (H := H) hForm
have hN :
∀ {i j : J}, i ≤ j → Nstage j ≤ Nstage i :=
freeProCFiniteQuotientStageKernelFamily_antitone
(C := C) φ
(id : J → J) (fun hij => hij)
have hcoeff_mod :
∀ {i j : J} (hij : i ≤ j),
∀ a : ModNCompletedCoeff (zcIndex j).1.modulus,
modNCompletedCoeffMap
(n := nstage i) (m := (zcIndex i).1.modulus) (dvd_rfl)
(modNCompletedCoeffMap
(n := (zcIndex i).1.modulus) (m := (zcIndex j).1.modulus)
(hij.1) a) =
modNCompletedCoeffMap (n := nstage i) (m := nstage j) (hij.1)
(modNCompletedCoeffMap
(n := nstage j) (m := (zcIndex j).1.modulus) (dvd_rfl) a) := by
intro i j hij a
change
modNCompletedCoeffMap
(n := i.1.modulus) (m := i.1.modulus) dvd_rfl
(modNCompletedCoeffMap
(n := i.1.modulus) (m := j.1.modulus) hij.1 a) =
modNCompletedCoeffMap
(n := i.1.modulus) (m := j.1.modulus) hij.1
(modNCompletedCoeffMap
(n := j.1.modulus) (m := j.1.modulus) dvd_rfl a)
rw [modNCompletedCoeffMap_rfl, modNCompletedCoeffMap_rfl]
change
modNCompletedCoeffMap
(n := i.1.modulus) (m := j.1.modulus) hij.1 a =
modNCompletedCoeffMap
(n := i.1.modulus) (m := j.1.modulus) hij.1 a
rfl
have hqmap_transition :
∀ {i j : J} (hij : i ≤ j),
∀ q : CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2,
qmap i
((OpenNormalSubgroupInClass.map
(C := C) (G := H)
(U := OrderDual.ofDual (zcIndex i).2)
(V := OrderDual.ofDual (zcIndex j).2)
(hij.2) q)) =
foxAlgebraicStageTargetQuotientMap (X := X) (hN hij) (qmap j q) := by
intro i j hij q
exact
freeProCFiniteQuotientStageQMapFamily_transition
(C := C) φ zcIndex (fun hij => hij) hφgen hij q
have hgenerators :
∀ j : J, ∀ x : X,
qmap j (QuotientGroup.mk (φ x)) =
QuotientGroup.mk' (Nstage j) (FreeGroup.of x) := by
simpa [J, Nstage, zcIndex, qmap] using
freeProCFiniteQuotientStageQMapFamily_generator
(C := C) φ
(id : J → J) hφgen
have hcoeff_basis :
HasAdditiveIdentityQuotientKernelNeighbourhoodBasis
(A := ZCCompletedGroupAlgebra C H)
(fun j : J =>
(zcCompletedGroupAlgebraBifilteredStageCoeffMap
(C := C) (X := X) (H := H) Nstage nstage zcIndex
(fun _ => dvd_rfl) qmap j).toAddMonoidHom) := by
simpa [J, Nstage, nstage, zcIndex, qmap,
freeProCZCBifilteredAllFiniteQuotientStageCoeffMap,
freeProCZCBifilteredFiniteQuotientStageCoeffMap] using
freeProCZCBifilteredAllFiniteQuotientStageCoeffMap_additive_basis
(C := C) hForm (X := X) (H := H) φ hφgen
exact
boundaryCycles_subset_closedGenTarget_of_zcBiGraph
(C := C) (X := X) (H := H)
(J := J) (Nstage := Nstage) (nstage := nstage)
(zcIndex := zcIndex)
(hmod := fun _ => dvd_rfl) (qmap := qmap)
φ hgenerators
(freeProCZCFoxSemiZCBifilteredStageMap_identity_basis_of_component_bases_standardTopology
(C := C) (X := X) (H := H)
(Nstage := Nstage) (nstage := nstage) (hN := hN) (hn := fun hij => hij.1)
(zcIndex := zcIndex) (hzcIndex := fun hij => hij)
(hmod := fun _ => dvd_rfl) (qmap := qmap)
hdir hcoeff_mod hqmap_transition
(zcFreeFoxCoordinatesBifilteredStageMap_additive_basis_of_coeff_basis_standardTopology
(C := C) (X := X) (H := H)
(Nstage := Nstage) (nstage := nstage) (hN := hN) (hn := fun hij => hij.1)
(zcIndex := zcIndex) (hzcIndex := fun hij => hij)
(hmod := fun _ => dvd_rfl) (qmap := qmap)
hdir hcoeff_mod hqmap_transition hcoeff_basis)
(zcCompletedGABifilteredStageRightMap_identity_basis_of_stageQuotient_basis
(C := C) (X := X) (H := H)
(Nstage := Nstage) (zcIndex := zcIndex) (qmap := qmap)
(by
change
HasIdentityQuotientKernelNeighbourhoodBasis
(Y := H)
(fun j : ZCCompletedGroupAlgebraIndex C H =>
openNormalSubgroupInClassProj (C := C) (G := H) j.2)
exact
zcCompletedGroupAlgebraAllStageQuotientMap_identity_basis_of_hasOpenNormalBasisInClass
(C := C) (H := H) hHbasis)
(by
intro j
simpa [J, Nstage, zcIndex, qmap] using
freeProCFiniteQuotientStageQMapFamily_injective
(C := C) φ
(id : J → J) hφgen j)))