CrowellExactSequence.Profinite.Exactness
This module develops the Crowell--Blanchfield--Lyndon exact sequence and its completed coordinate forms.
import
Imported by
theorem presentedSepToZC_profiniteKernelAbelianizationBoundaryAddSep
(C : ProCGroups.FiniteGroupClass.{u})
(hC : ProCGroups.FiniteGroupClass.Hereditary C)
(psi : ContinuousMonoidHom G H)
(x : ProfiniteKernelAbelianizationAdd psi) :
presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
(G := G) (H := H) C hC psi
(profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := G) (H := H) C psi x) =
0The separated displayed boundary kills the separated kernel boundary.
Show proof
by
change
(fun y : ProfiniteKernelAbelianization psi =>
presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
(G := G) (H := H) C hC psi
(profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := G) (H := H) C psi (Additive.ofMul y)) =
0) (Additive.toMul x)
refine QuotientGroup.induction_on (Additive.toMul x) ?_
intro n
change
presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
(G := G) (H := H) C hC psi
(profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := G) (H := H) C psi
(Additive.ofMul
(QuotientGroup.mk'
(Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n))) =
0
rw [profiniteKernelAbelianizationBoundaryAddProCIntegerSep_of,
presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger_d]
exact zcCompletedGroupAlgebraBoundary_eq_zero_of_mem_ker
(C := C) (H := H) psi.toMonoidHom n.2Proof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. The augmentation module terms are generated by the chosen basis elements, so equality on those generators determines each coordinate map. The finite-stage exactness assertions are stable under the comparison isomorphisms used to move between separated and unseparated coordinates. Consequently the completed sequence inherits the same exactness calculation. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem exact_boundaryAddZC_sep_iff_delta_cycles_integrate
(C : ProCGroups.FiniteGroupClass.{u})
(hC : ProCGroups.FiniteGroupClass.Hereditary C)
(psi : ContinuousMonoidHom G H) :
Function.Exact
(profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := G) (H := H) C psi)
(presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
(G := G) (H := H) C hC psi) ↔
∀ a : ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom,
presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
(G := G) (H := H) C hC psi a = 0 →
∃ n : ProfiniteKernelSubgroup psi,
zcSeparatedUniversalDifferential C psi.toMonoidHom n.1 = aExactness of the separated additive boundary is equivalent to integrability of all separated delta cycles.
Show proof
by
let dN :=
profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := G) (H := H) C psi
let delta :=
presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
(G := G) (H := H) C hC psi
constructor
· intro hexact a ha
rcases (hexact a).1 ha with ⟨x, hx⟩
revert hx
change
(fun q : ProfiniteKernelAbelianization psi =>
dN (Additive.ofMul q) = a →
∃ n : ProfiniteKernelSubgroup psi,
zcSeparatedUniversalDifferential C psi.toMonoidHom n.1 = a) (Additive.toMul x)
refine QuotientGroup.induction_on (Additive.toMul x) ?_
intro n hn
refine ⟨n, ?_⟩
simpa [dN] using hn
· intro hintegrates a
constructor
· intro ha
rcases hintegrates a ha with ⟨n, hn⟩
refine ⟨Additive.ofMul
(QuotientGroup.mk'
(Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n), ?_⟩
simpa [dN] using hn
· rintro ⟨x, hx⟩
rw [← hx]
exact
presentedSepToZC_profiniteKernelAbelianizationBoundaryAddSep
(G := G) (H := H) C hC psi xProof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. The augmentation module terms are generated by the chosen basis elements, so equality on those generators determines each coordinate map. The finite-stage exactness assertions are stable under the comparison isomorphisms used to move between separated and unseparated coordinates. Consequently the completed sequence inherits the same exactness calculation. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem exact_boundaryAddZC_sep_of_coord_cycle_lift
(C : ProCGroups.FiniteGroupClass.{u})
(hC : ProCGroups.FiniteGroupClass.Hereditary C)
(psi : ContinuousMonoidHom G H)
{X : Type u} [Fintype X] [DecidableEq X] (family : X → G)
(coords :
ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom ≃ₗ[
ZCCompletedGroupAlgebra C H]
ZCFreeFoxCoordinates C (X := X) (H := H))
(hcoords_symm :
coords.symm.toLinearMap =
presentedSeparatedDifferentialFamilyMapProCInteger
(G := G) (H := H) C psi family)
(Dcoords : G → ZCFreeFoxCoordinates C (X := X) (H := H))
(hDcoords_kernel :
∀ n : ProfiniteKernelSubgroup psi,
Dcoords n.1 =
coords (zcSeparatedUniversalDifferential C psi.toMonoidHom n.1))
(hcycle_lift :
∀ v : ZCFreeFoxCoordinates C (X := X) (H := H),
blanchfieldLyndonFiniteFamilyMap
(R := ZCCompletedGroupAlgebra C H)
(fun i : X =>
presentedCompletedDifferentialBoundaryProCInteger
(G := G) (H := H) C psi (family i)) v = 0 →
∃ n : ProfiniteKernelSubgroup psi, Dcoords n.1 = v) :
Function.Exact
(profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := G) (H := H) C psi)
(presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
(G := G) (H := H) C hC psi)A coordinate lift for each cycle gives exactness of the separated additive boundary sequence.
Show proof
by
let dN :=
profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := G) (H := H) C psi
let delta :=
presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
(G := G) (H := H) C hC psi
let blDelta :=
blanchfieldLyndonFiniteFamilyMap
(R := ZCCompletedGroupAlgebra C H)
(fun i : X =>
presentedCompletedDifferentialBoundaryProCInteger
(G := G) (H := H) C psi (family i))
have hblDelta_comp : delta.comp coords.symm.toLinearMap = blDelta := by
rw [hcoords_symm]
exact
presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger_comp_familyMap
(G := G) (H := H) C hC psi family
have hblDelta_apply (y) : blDelta y = delta (coords.symm y) := by
have h := congrArg (fun f => f y) hblDelta_comp
simpa [LinearMap.comp_apply, delta, blDelta] using h.symm
change Function.Exact dN delta
intro a
constructor
· intro ha
have hcoord_cycle : blDelta (coords a) = 0 := by
calc
blDelta (coords a) = delta (coords.symm (coords a)) := hblDelta_apply (coords a)
_ = delta a := by rw [coords.symm_apply_apply]
_ = 0 := ha
rcases hcycle_lift (coords a) hcoord_cycle with ⟨n, hncoords⟩
refine ⟨Additive.ofMul
(QuotientGroup.mk'
(Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n), ?_⟩
apply coords.injective
calc
coords
(dN (Additive.ofMul
(QuotientGroup.mk'
(Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n))) =
coords (zcSeparatedUniversalDifferential C psi.toMonoidHom n.1) := by
rw [profiniteKernelAbelianizationBoundaryAddProCIntegerSep_of]
_ = Dcoords n.1 := (hDcoords_kernel n).symm
_ = coords a := hncoords
· rintro ⟨x, hx⟩
rw [← hx]
exact
presentedSepToZC_profiniteKernelAbelianizationBoundaryAddSep
(G := G) (H := H) C hC psi xProof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. The augmentation module terms are generated by the chosen basis elements, so equality on those generators determines each coordinate map. The finite-stage exactness assertions are stable under the comparison isomorphisms used to move between separated and unseparated coordinates. Consequently the completed sequence inherits the same exactness calculation. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem continuous_familyCoordinatesZC_zcUnivDiff_of_closedGen_leftGraph
(ProC : ProCGroupPredicate.{u}) (psi : ContinuousMonoidHom G H)
{X : Type u} [Fintype X] [DecidableEq X] (family : X → G)
(hbasis_A :
IsPresentedCompletedDifferentialFamilyBasisProCInteger
(G := G) (H := H) ProC.finiteQuotientClass psi family)
(hfree :
ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
(ProC := ProC) X G family)
(htarget :
ProC
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) (fun i : X => psi (family i)) : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
(hφconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) (fun i : X => psi (family i)) : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator
(ProC := ProC) (fun i : X => psi (family i))))
(hleft_graph_eq :
∀ g : G,
freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g =
presentedCompletedDifferentialFamilyCoordinatesProCInteger
(G := G) (H := H) ProC.finiteQuotientClass psi family hbasis_A
(zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g)) :
Continuous
(fun g : G =>
presentedCompletedDifferentialFamilyCoordinatesProCInteger
(G := G) (H := H) ProC.finiteQuotientClass psi family hbasis_A
(zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g))The paper coordinate universal differential is continuous once it is identified with the closed-generated completed Fox derivative vector.
Show proof
by
let Dclosed : G → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
fun g =>
freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g
have hclosed_continuous : Continuous Dclosed := by
simpa [Dclosed] using
continuous_freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC) X H hfree (fun i : X => psi (family i)) htarget hφconv
have hcoords_eq :
(fun g : G =>
presentedCompletedDifferentialFamilyCoordinatesProCInteger
(G := G) (H := H) ProC.finiteQuotientClass psi family hbasis_A
(zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g)) = Dclosed := by
funext g
exact (hleft_graph_eq g).symm
rw [hcoords_eq]
exact hclosed_continuousProof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. For separated or completed versions, each map is compared after all finite-stage projections; those projections separate points and commute with the sequence maps. Linear equivalences preserve exactness because composing with an isomorphism does not change kernels or images after transporting them along the equivalence. The passage from finite stages to the profinite object uses the inverse-limit topology, so compatibility of all coordinates gives a continuous completed map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem freeProCZCCompletedFoxDerivativeVectorViaClosedGen_eq_presentedCoordinates_zcUnivDiff
(ProC : ProCGroupPredicate.{u}) (psi : ContinuousMonoidHom G H)
{X : Type u} [Fintype X] [DecidableEq X] (family : X → G)
(hbasis_A :
IsPresentedCompletedDifferentialFamilyBasisProCInteger
(G := G) (H := H) ProC.finiteQuotientClass psi family)
(hfree :
ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
(ProC := ProC) X G family)
(hH : ProC (G := H))
(htarget :
ProC
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) (fun i : X => psi (family i)) : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
(hφconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) (fun i : X => psi (family i)) : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator
(ProC := ProC) (fun i : X => psi (family i))))
(hφHconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G := H) (fun i : X => psi (family i)))
(hφHgen :
ProCGroups.Generation.TopologicallyGenerates
(G := H) (Set.range (fun i : X => psi (family i)))) :
∀ g : G,
freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g =
presentedCompletedDifferentialFamilyCoordinatesProCInteger
(G := G) (H := H) ProC.finiteQuotientClass psi family hbasis_A
(zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g)The left coordinate of the closed-generated completed Fox graph agrees with the paper coordinate universal differential.
Show proof
by
let coords :=
presentedCompletedDifferentialFamilyCoordinatesProCInteger
(G := G) (H := H) ProC.finiteQuotientClass psi family hbasis_A
let f :
(X → ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) →ₗ[
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H]
ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom :=
presentedCompletedDifferentialFamilyMapProCInteger
(G := G) (H := H) ProC.finiteQuotientClass psi family
let L :
ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom →ₗ[
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H]
ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
closedGeneratedDerivativeCoordinatesLinearMapProCInteger
(G := G) (H := H) ProC psi family hfree htarget hφconv hH hφHconv hφHgen
have hL_comp : L.comp f = LinearMap.id := by
exact
closedGeneratedDerivativeCoordinatesLinearMapProCInteger_comp_familyMap
(G := G) (H := H) ProC psi family hfree htarget hφconv hH hφHconv hφHgen
have hL_eq_coords : L = coords.toLinearMap := by
exact
presentedCompletedDifferentialFamilyCoordinatesProCInteger_eq_of_leftInverse
(G := G) (H := H) ProC.finiteQuotientClass psi family hbasis_A L hL_comp
intro g
calc
freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g =
L (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) := by
rw [closedGeneratedDerivativeCoordinatesLinearMapProCInteger_universal
(G := G) (H := H) ProC psi family hfree htarget hφconv hH hφHconv hφHgen g]
_ = coords
(zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) := by
rw [hL_eq_coords]
rflProof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. For separated or completed versions, each map is compared after all finite-stage projections; those projections separate points and commute with the sequence maps. Linear equivalences preserve exactness because composing with an isomorphism does not change kernels or images after transporting them along the equivalence. The passage from finite stages to the profinite object uses the inverse-limit topology, so compatibility of all coordinates gives a continuous completed map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem completedBoundaryKillsTopCommZC_of_closedGen_leftGraph
(ProC : ProCGroupPredicate.{u}) (psi : ContinuousMonoidHom G H)
{X : Type u} [Fintype X] [DecidableEq X] (family : X → G)
[T1Space (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))]
(hbasis_A :
IsPresentedCompletedDifferentialFamilyBasisProCInteger
(G := G) (H := H) ProC.finiteQuotientClass psi family)
(hfree :
ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
(ProC := ProC) X G family)
(htarget :
ProC
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) (fun i : X => psi (family i)) : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
(hφconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) (fun i : X => psi (family i)) : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator
(ProC := ProC) (fun i : X => psi (family i))))
(hleft_graph_eq :
∀ g : G,
freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g =
presentedCompletedDifferentialFamilyCoordinatesProCInteger
(G := G) (H := H) ProC.finiteQuotientClass psi family hbasis_A
(zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g)) :
CompletedBoundaryKillsTopologicalCommutatorProCInteger
(G := G) (H := H) ProC.finiteQuotientClass psiThe Crowell--Blanchfield coordinate formula agrees with the quotient-level construction after passage to the separated or completed module.
Show proof
by
let Dclosed : G → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
fun g =>
freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g
refine
completedBoundaryKillsTopCommZC_of_continuous_ambient_familyCoords_fintype
(G := G) (H := H) ProC.finiteQuotientClass psi family hbasis_A Dclosed ?_ ?_
· simpa [Dclosed] using
continuous_freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC) X H hfree (fun i : X => psi (family i)) htarget hφconv
· intro n
exact hleft_graph_eq n.1Proof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. The passage from finite stages to the profinite object uses the inverse-limit topology, so compatibility of all coordinates gives a continuous completed map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. The augmentation module terms are generated by the chosen basis elements, so equality on those generators determines each coordinate map. The finite-stage exactness assertions are stable under the comparison isomorphisms used to move between separated and unseparated coordinates. Consequently the completed sequence inherits the same exactness calculation. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem freeProCZCBifilteredAllFiniteQuotientStageCoeffMap_additive_basis
{ProC : ProCGroupPredicate.{u}} [ProC.HasFiniteQuotientFormation]
{X H : Type u} [DecidableEq X]
[Group H] [TopologicalSpace H] [IsTopologicalGroup H]
[Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)]
(φ : X → H)
(hφgen :
ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :
HasAdditiveIdentityQuotientKernelNeighbourhoodBasis
(A := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
(fun j : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H =>
(freeProCZCBifilteredAllFiniteQuotientStageCoeffMap
(ProC := ProC) (X := X) (H := H) φ hφgen j).toAddMonoidHom)The Crowell--Blanchfield coordinate formula agrees with the quotient-level construction after passage to the separated or completed module.
Show proof
by
letI : ProCGroups.FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass :=
ProC.finiteQuotientContainsTrivialQuotients
letI : Nonempty (ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H) :=
⟨(ProCIntegerIndex.terminal (C := ProC.finiteQuotientClass) inferInstance,
zcCompletedGroupAlgebraTopIndex ProC.finiteQuotientClass H)⟩
let S := zcCompletedGroupAlgebraSystem ProC.finiteQuotientClass H
have hdir :
Directed (· ≤ ·) (id : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H →
ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H) :=
directed_zcCompletedGroupAlgebraIndex
(C := ProC.finiteQuotientClass) (H := H) ProC.finiteQuotientFormation
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 ProC.finiteQuotientClass H j z ∈ V
letI :
∀ j : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H,
DiscreteTopology
(CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass 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 := ProC.finiteQuotientClass) φ
(id : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H →
ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H) hφgen j) := by
exact
freeProCFiniteQuotientStageQMapFamily_injective
(C := ProC.finiteQuotientClass) φ
(id : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H →
ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H) hφgen j
have hstage_inj :
Function.Injective
(zcCompletedGroupAlgebraStageToFiniteFoxStage
(ProC := ProC) (X := X) (H := H)
(freeProCFiniteQuotientStageKernelFamily
(C := ProC.finiteQuotientClass) φ
(id : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H →
ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H) j)
j.1.modulus j dvd_rfl
(freeProCFiniteQuotientStageQMapFamily
(C := ProC.finiteQuotientClass) φ
(id : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H →
ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H) hφgen j)) := by
exact
zcCompletedGroupAlgebraStageToFiniteFoxStage_self_injective
(ProC := ProC) (X := X) (H := H)
(freeProCFiniteQuotientStageKernelFamily
(C := ProC.finiteQuotientClass) φ
(id : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H →
ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H) j)
j
(freeProCFiniteQuotientStageQMapFamily
(C := ProC.finiteQuotientClass) φ
(id : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H →
ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H) hφgen j)
hqmap_inj
have hzstage :
zcCompletedGroupAlgebraProjection ProC.finiteQuotientClass H j z = 0 := by
apply hstage_inj
simpa [freeProCZCBifilteredAllFiniteQuotientStageCoeffMap,
freeProCZCBifilteredFiniteQuotientStageCoeffMap,
zcCompletedGroupAlgebraBifilteredStageCoeffMap,
zcCompletedGroupAlgebraFiniteFoxStageCoeffMap] using hz
simpa [hzstage] using hzeroVProof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. The augmentation module terms are generated by the chosen basis elements, so equality on those generators determines each coordinate map. The finite-stage exactness assertions are stable under the comparison isomorphisms used to move between separated and unseparated coordinates. Consequently the completed sequence inherits the same exactness calculation. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_zcBiAllStages_coeffGraphRelDeriv
{ProC : ProCGroupPredicate.{u}} [ProC.HasFiniteQuotientFormation]
{X H : Type u} [Fintype X] [DecidableEq X]
[Group H] [TopologicalSpace H] [IsTopologicalGroup H]
[Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)]
(φ : X → H)
(hH_isProC : IsProCGroup ProC.finiteQuotientClass H)
(hφgen :
ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))The Crowell--Blanchfield coordinate formula agrees with the quotient-level construction after passage to the separated or completed module.
Show proof
by
letI : ProCGroups.FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass :=
ProC.finiteQuotientContainsTrivialQuotients
letI : Nonempty (ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H) :=
⟨(ProCIntegerIndex.terminal (C := ProC.finiteQuotientClass) inferInstance,
zcCompletedGroupAlgebraTopIndex ProC.finiteQuotientClass H)⟩
letI :
∀ j : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H,
Fact (0 < j.1.modulus) :=
fun j => ProCIntegerIndex.positiveFact j.1
letI :
∀ j : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H,
DiscreteTopology
(CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.2) :=
fun j =>
QuotientGroup.discreteTopology
(ProCGroups.openNormalSubgroup_isOpen (G := H)
((OrderDual.ofDual j.2).1 : OpenNormalSubgroup H))
let J := ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H
let Nstage : J → Subgroup (FreeGroup X) :=
freeProCFiniteQuotientStageKernelFamily
(C := ProC.finiteQuotientClass) φ
(id : J → J)
let nstage : J → ℕ := fun j => j.1.modulus
let zcIndex : J → ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H := id
let qmap : ∀ j : J,
CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass (zcIndex j).2 →*
finiteFoxStageTargetQuotient (X := X) (Nstage j) :=
freeProCFiniteQuotientStageQMapFamily
(C := ProC.finiteQuotientClass) φ
(id : J → J) hφgen
have hdir : Directed (· ≤ ·) (id : J → J) :=
directed_zcCompletedGroupAlgebraIndex
(C := ProC.finiteQuotientClass) (H := H) ProC.finiteQuotientFormation
have hN :
∀ {i j : J}, i ≤ j → Nstage j ≤ Nstage i :=
freeProCFiniteQuotientStageKernelFamily_antitone
(C := ProC.finiteQuotientClass) φ
(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
simp only [id_eq, modNCompletedCoeffMap_rfl, RingHomCompTriple.comp_apply, RingHom.id_apply, nstage, zcIndex]
have hqmap_transition :
∀ {i j : J} (hij : i ≤ j),
∀ q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass (zcIndex j).2,
qmap i
((OpenNormalSubgroupInClass.map
(C := ProC.finiteQuotientClass) (G := H)
(U := OrderDual.ofDual (zcIndex i).2)
(V := OrderDual.ofDual (zcIndex j).2)
(hij.2) q)) =
finiteFoxStageTargetQuotientMap (X := X) (hN hij) (qmap j q) := by
intro i j hij q
exact
freeProCFiniteQuotientStageQMapFamily_transition
(C := ProC.finiteQuotientClass) φ 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 := ProC.finiteQuotientClass) φ
(id : J → J) hφgen
have hcoeff_basis :
HasAdditiveIdentityQuotientKernelNeighbourhoodBasis
(A := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
(fun j : J =>
(zcCompletedGroupAlgebraBifilteredStageCoeffMap
(ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex
(fun _ => dvd_rfl) qmap j).toAddMonoidHom) := by
simpa [J, nstage, zcIndex, qmap, freeProCZCBifilteredFiniteQuotientStageCoeffMap] using
freeProCZCBifilteredAllFiniteQuotientStageCoeffMap_additive_basis
(ProC := ProC) (X := X) (H := H) φ hφgen
exact
boundaryCycles_subset_closedGenTarget_of_zcBiGraph
(ProC := ProC) (X := X) (H := H)
(J := J) (Nstage := Nstage) (nstage := nstage)
(hN := hN) (hn := fun hij => hij.1)
(zcIndex := zcIndex) (hzcIndex := fun hij => hij)
(hmod := fun _ => dvd_rfl) (qmap := qmap)
φ hcoeff_mod hqmap_transition hgenerators
(freeProCZCFoxSemiZCBifilteredStageMap_identity_basis_of_component_bases_standardTopology
(ProC := ProC) (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
(ProC := ProC) (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
(ProC := ProC) (X := X) (H := H)
(Nstage := Nstage) (zcIndex := zcIndex) (qmap := qmap)
(by
simpa [J, zcIndex] using
zcCompletedGroupAlgebraAllStageQuotientMap_identity_basis_of_isProCGroup
(C := ProC.finiteQuotientClass) (H := H) hH_isProC)
(by
intro j
simpa [J, Nstage, zcIndex, qmap] using
freeProCFiniteQuotientStageQMapFamily_injective
(C := ProC.finiteQuotientClass) φ
(id : J → J) hφgen j)))Proof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. For separated or completed versions, each map is compared after all finite-stage projections; those projections separate points and commute with the sequence maps. The passage from finite stages to the profinite object uses the inverse-limit topology, so compatibility of all coordinates gives a continuous completed map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□