CrowellExactSequence.Profinite.RelationReflection
This module develops the Crowell--Blanchfield--Lyndon exact sequence and its completed coordinate forms.
import
Imported by
theorem zcCompletedDifferentialModulePreStageMap_relation_iff_stage_mkQ_eq_zero
(C : ProCGroups.FiniteGroupClass.{u})
{G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(ψ : G →* H)
(i : ZCCompletedDifferentialModuleIndex C ψ)
(x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :
zcCompletedDifferentialModulePreStageMap C ψ i x ∈
crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i) ↔
((crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
(zcCompletedDifferentialModulePreStageMap C ψ i x) = 0)Show proof
by
constructor
· intro hx
exact
(Submodule.Quotient.mk_eq_zero
(p := crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i))
(x := zcCompletedDifferentialModulePreStageMap C ψ i x)).2 hx
· intro hx
exact
(Submodule.Quotient.mk_eq_zero
(p := crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i))
(x := zcCompletedDifferentialModulePreStageMap C ψ i x)).1 hxProof. 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.
□theorem freeProC_zcCompletedDifferentialModuleIndex_nonempty
(sourceData : FreeProCSourceData ProC)
(psi : ContinuousMonoidHom sourceData.carrier H) :
Nonempty
(ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom)Nonempty finite stage index set for a continuous map out of a free pro-\(C\) group.
Show proof
by
exact ⟨zcCompletedDifferentialModuleComapIndex
(C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi
((ProCGroups.Completion.ProCIntegerIndex.terminal
(C := ProC.finiteQuotientClass) inferInstance),
zcCompletedGroupAlgebraTopIndex ProC.finiteQuotientClass H)⟩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.
□theorem freeProC_directed_zcCompletedDifferentialModuleIndex
(sourceData : FreeProCSourceData ProC)
(psi : ContinuousMonoidHom sourceData.carrier H) :
Directed (· ≤ ·)
(id :
ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom →
ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom)Show proof
directed_zcCompletedDifferentialModuleIndex
(C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
(ProCGroupPredicate.finiteQuotientFormation ProC)
(ProCGroupPredicate.finiteQuotientHereditary ProC) psiProof. 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. Injectivity follows by applying the separating family of finite-stage projections to the difference of two possible preimages. Surjectivity is proved by lifting the target coordinates at finite stages and checking that the boundary formula maps the lift to the prescribed target element. 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.
□abbrev freeProCReflectionFamily
(sourceData : FreeProCSourceData ProC) {r : Nat}
(hbasis : Cardinal.mk sourceData.basis = r) : ULift.{u} (Fin r) → sourceData.carrier :=
freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasisThe universe-lifted finite free basis supplies the reflection family used in the proof.
theorem freeProCReflectionFamily_target_generates
(sourceData : FreeProCSourceData ProC) {r : Nat}
(hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi) :
ProCGroups.Generation.TopologicallyGenerates
(G := H)
(Set.range (fun i : ULift.{u} (Fin r) =>
psi (freeProCReflectionFamily (ProC := ProC) sourceData hbasis i)))The target images of the chosen basis topologically generate a surjective target.
Show proof
by
simpa [freeProCReflectionFamily] using
freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
(ProC := ProC) sourceData hbasis psi hpsiProof. 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. For separated or completed versions, each map is compared after all finite-stage projections; those projections separate points and commute with the sequence maps. Surjectivity is proved by lifting the target coordinates at finite stages and checking that the boundary formula maps the lift to the prescribed target element. 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. For surjectivity, choose a representative of the target coordinate and lift it through the underlying surjective group, quotient, or coefficient map. The defining formula for the induced map sends the constructed preimage to the chosen representative at every finite stage, so inverse-limit extensionality gives the required global preimage.
□def freeProCRelationReflectionStageSourceHom
(sourceData : FreeProCSourceData ProC) {r : Nat}
(hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(i : ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :
FreeGroup (ULift.{u} (Fin r)) →*
zcCompletedDifferentialModuleStageSource
ProC.finiteQuotientClass psi.toMonoidHom i :=
(zcCompletedDifferentialModuleStageSourceProj
ProC.finiteQuotientClass psi.toMonoidHom i).comp
(FreeGroup.lift (freeProCReflectionFamily (ProC := ProC) sourceData hbasis))The free-group map onto the source quotient used by a differential-module finite stage.
def freeProCRelationReflectionStageKernel
(sourceData : FreeProCSourceData ProC) {r : Nat}
(hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(i : ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :
Subgroup (FreeGroup (ULift.{u} (Fin r))) :=
MonoidHom.ker
(freeProCRelationReflectionStageSourceHom (ProC := ProC) sourceData hbasis psi i)The source kernel used by a differential-module stage, pulled back to the abstract free group on the chosen basis.
instance freeProCRelationReflectionStageKernel_normal
(sourceData : FreeProCSourceData ProC) {r : Nat}
(hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(i : ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :
(freeProCRelationReflectionStageKernel (ProC := ProC) sourceData hbasis psi i).Normal := by
dsimp [freeProCRelationReflectionStageKernel]
infer_instanceThe relation-reflection stage kernel is a normal subgroup of the free group on the lifted finite basis.
theorem freeProCRelationReflectionStageSourceHom_surjective
(sourceData : FreeProCSourceData ProC) {r : Nat}
(hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(i : ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :
Function.Surjective
(freeProCRelationReflectionStageSourceHom (ProC := ProC) sourceData hbasis psi i)The chosen free basis surjects onto every finite source quotient stage.
Show proof
by
classical
let X : Type u := ULift.{u} (Fin r)
let ι : X → sourceData.carrier := freeProCReflectionFamily (ProC := ProC) sourceData hbasis
let Q : Type u :=
zcCompletedDifferentialModuleStageSource
ProC.finiteQuotientClass psi.toMonoidHom i
letI : DiscreteTopology Q :=
QuotientGroup.discreteTopology i.source.1.toOpenSubgroup.isOpen'
let g : X → Q := fun x =>
zcCompletedDifferentialModuleStageSourceProj
ProC.finiteQuotientClass psi.toMonoidHom i (ι x)
have hsource :
ProCGroups.Generation.TopologicallyGenerates
(G := sourceData.carrier) (Set.range ι) := by
simpa [ι, freeProCReflectionFamily] using
freeProCChosenULiftFamilyOfBasisCard_generates (ProC := ProC) sourceData hbasis
have hquot_image :
ProCGroups.Generation.TopologicallyGenerates
(G := Q)
((QuotientGroup.mk' (i.source.1 : Subgroup sourceData.carrier)) '' Set.range ι) := by
simpa [Q] using
ProCGroups.Generation.topologicallyGenerates_quotient_image
(G := sourceData.carrier) (N := (i.source.1 : Subgroup sourceData.carrier)) hsource
have hrange :
((QuotientGroup.mk' (i.source.1 : Subgroup sourceData.carrier)) '' Set.range ι) =
Set.range g := by
ext y
constructor
· rintro ⟨x, ⟨a, rfl⟩, rfl⟩
exact ⟨a, rfl⟩
· rintro ⟨a, rfl⟩
exact ⟨ι a, ⟨a, rfl⟩, rfl⟩
have hg :
ProCGroups.Generation.TopologicallyGenerates (G := Q) (Set.range g) := by
rw [← hrange]
exact hquot_image
have hsurj : Function.Surjective (FreeGroup.lift g) :=
ProCGroups.FiniteGeneration.freeGroup_lift_surjective_of_topologicallyGenerates_discrete
(G := Q) g hg
have hlift :
FreeGroup.lift g =
freeProCRelationReflectionStageSourceHom (ProC := ProC) sourceData hbasis psi i := by
apply FreeGroup.ext_hom
intro x
rw [FreeGroup.lift_apply_of]
change
zcCompletedDifferentialModuleStageSourceProj
ProC.finiteQuotientClass psi.toMonoidHom i (ι x) =
zcCompletedDifferentialModuleStageSourceProj
ProC.finiteQuotientClass psi.toMonoidHom i
((FreeGroup.lift (freeProCReflectionFamily (ProC := ProC) sourceData hbasis))
(FreeGroup.of x))
rw [FreeGroup.lift_apply_of]
simpa [hlift] using hsurjProof. 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. Surjectivity is proved by lifting the target coordinates at finite stages and checking that the boundary formula maps the lift to the prescribed target element. 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.
□def freeProCRelationReflectionStageSourceEquiv
(sourceData : FreeProCSourceData ProC) {r : Nat}
(hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(i : ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :
finiteFoxStageTargetQuotient
(X := ULift.{u} (Fin r))
(freeProCRelationReflectionStageKernel (ProC := ProC) sourceData hbasis psi i) ≃*
zcCompletedDifferentialModuleStageSource
ProC.finiteQuotientClass psi.toMonoidHom i :=
QuotientGroup.quotientKerEquivOfSurjective
(freeProCRelationReflectionStageSourceHom (ProC := ProC) sourceData hbasis psi i)
(freeProCRelationReflectionStageSourceHom_surjective
(ProC := ProC) sourceData hbasis psi i)Identification of the source quotient stage with the corresponding free-group quotient.
theorem freeProCRelationReflectionStageSourceEquiv_mk
(sourceData : FreeProCSourceData ProC) {r : Nat}
(hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(i : ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom)
(w : FreeGroup (ULift.{u} (Fin r))) :
freeProCRelationReflectionStageSourceEquiv (ProC := ProC) sourceData hbasis psi i
(QuotientGroup.mk'
(freeProCRelationReflectionStageKernel (ProC := ProC) sourceData hbasis psi i) w) =
freeProCRelationReflectionStageSourceHom (ProC := ProC) sourceData hbasis psi i wThe relation-reflection source-stage equivalence sends the quotient class of a free word to its image under the corresponding source-stage homomorphism.
Show proof
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.
□abbrev freeProCRelationReflectionTargetStageKernel
(sourceData : FreeProCSourceData ProC) {r : Nat}
(hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(i : ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :
Subgroup (FreeGroup (ULift.{u} (Fin r))) :=
freeProCFiniteQuotientStageKernel
(C := ProC.finiteQuotientClass)
(fun x : ULift.{u} (Fin r) =>
psi (freeProCReflectionFamily (ProC := ProC) sourceData hbasis x))
i.target.2The target finite Fox relation kernel attached to the target quotient of a \(\mathbb{Z}_C\)-completed differential-module index.
instance freeProCRelationReflectionTargetStageKernel_normal
(sourceData : FreeProCSourceData ProC) {r : Nat}
(hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(i : ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :
(freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi i).Normal :=
inferInstanceThe target finite Fox relation kernel is normal.
theorem freeProCRelationReflectionTargetStageKernel_antitone
(sourceData : FreeProCSourceData ProC) {r : Nat}
(hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
{i j : ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom} (hij : i ≤ j) :
freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi j ≤
freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi iShow proof
by
exact freeProCFiniteQuotientStageKernel_antitone
(C := ProC.finiteQuotientClass)
(fun x : ULift.{u} (Fin r) =>
psi (freeProCReflectionFamily (ProC := ProC) sourceData hbasis x))
hij.2.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. 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.
□def freeProCRelationReflectionTargetStageQMap
(sourceData : FreeProCSourceData ProC) {r : Nat}
(hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi)
(i : ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :
CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.target.2 →*
finiteFoxStageTargetQuotient
(X := ULift.{u} (Fin r))
(freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi i) := by
let φ : ULift.{u} (Fin r) → H := fun x =>
psi (freeProCReflectionFamily (ProC := ProC) sourceData hbasis x)
have hφgen :
ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ) := by
simpa [φ] using
freeProCReflectionFamily_target_generates (ProC := ProC) sourceData hbasis psi hpsi
letI : DiscreteTopology
(CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.target.2) :=
QuotientGroup.discreteTopology
(ProCGroups.openNormalSubgroup_isOpen (G := H)
((OrderDual.ofDual i.target.2).1 : OpenNormalSubgroup H))
exact freeProCFiniteQuotientStageQMap
(C := ProC.finiteQuotientClass) φ i.target.2
(freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates
(C := ProC.finiteQuotientClass) φ i.target.2 hφgen)The canonical target quotient comparison map \(H/U_i \to F_X/N_i\).
theorem freeProCRelationReflectionTargetStageQMap_generator
(sourceData : FreeProCSourceData ProC) {r : Nat}
(hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi)
(i : ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom)
(x : ULift.{u} (Fin r)) :
freeProCRelationReflectionTargetStageQMap (ProC := ProC) sourceData hbasis psi hpsi i
(QuotientGroup.mk
(psi (freeProCReflectionFamily (ProC := ProC) sourceData hbasis x))) =
QuotientGroup.mk'
(freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi i)
(FreeGroup.of x)Show proof
by
let φ : ULift.{u} (Fin r) → H := fun x =>
psi (freeProCReflectionFamily (ProC := ProC) sourceData hbasis x)
change
freeProCRelationReflectionTargetStageQMap
(ProC := ProC) sourceData hbasis psi hpsi i (QuotientGroup.mk (φ x)) =
QuotientGroup.mk'
(freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi i)
(FreeGroup.of x)
unfold freeProCRelationReflectionTargetStageQMap
simp only [freeProCFiniteQuotientStageQMap_generator,
freeProCRelationReflectionTargetStageKernel, ContinuousMonoidHom.coe_toMonoidHom,
QuotientGroup.mk'_apply, φ]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. Surjectivity is proved by lifting the target coordinates at finite stages and checking that the boundary formula maps the lift to the prescribed target element. 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 freeProCRelationReflectionTargetStageQMap_transition
(sourceData : FreeProCSourceData ProC) {r : Nat}
(hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi)
{i j : ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom} (hij : i ≤ j)
(q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.target.2) :
freeProCRelationReflectionTargetStageQMap (ProC := ProC) sourceData hbasis psi hpsi i
((OpenNormalSubgroupInClass.map
(C := ProC.finiteQuotientClass) (G := H)
(U := OrderDual.ofDual i.target.2)
(V := OrderDual.ofDual j.target.2) hij.2.2) q) =
finiteFoxStageTargetQuotientMap
(X := ULift.{u} (Fin r))
(freeProCRelationReflectionTargetStageKernel_antitone
(ProC := ProC) sourceData hbasis psi hij)
(freeProCRelationReflectionTargetStageQMap
(ProC := ProC) sourceData hbasis psi hpsi j q)Target quotient comparison maps commute with differential-module stage refinement.
Show proof
by
let φ : ULift.{u} (Fin r) → H := fun x =>
psi (freeProCReflectionFamily (ProC := ProC) sourceData hbasis x)
have hφgen :
ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ) := by
simpa [φ] using
freeProCReflectionFamily_target_generates (ProC := ProC) sourceData hbasis psi hpsi
letI : DiscreteTopology
(CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.target.2) :=
QuotientGroup.discreteTopology
(ProCGroups.openNormalSubgroup_isOpen (G := H)
((OrderDual.ofDual i.target.2).1 : OpenNormalSubgroup H))
letI : DiscreteTopology
(CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.target.2) :=
QuotientGroup.discreteTopology
(ProCGroups.openNormalSubgroup_isOpen (G := H)
((OrderDual.ofDual j.target.2).1 : OpenNormalSubgroup H))
unfold freeProCRelationReflectionTargetStageQMap
exact freeProCFiniteQuotientStageQMap_transition
(C := ProC.finiteQuotientClass) φ hij.2.2
(freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates
(C := ProC.finiteQuotientClass) φ i.target.2 hφgen)
(freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates
(C := ProC.finiteQuotientClass) φ j.target.2 hφgen)
qProof. 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. Surjectivity is proved by lifting the target coordinates at finite stages and checking that the boundary formula maps the lift to the prescribed target element. 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.
□def freeProCRelationReflectionTargetStageRight
(sourceData : FreeProCSourceData ProC) {r : Nat}
(hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi)
(i : ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :
H →* finiteFoxStageTargetQuotient
(X := ULift.{u} (Fin r))
(freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi i) :=
(freeProCRelationReflectionTargetStageQMap
(ProC := ProC) sourceData hbasis psi hpsi i).comp
(openNormalSubgroupInClassProj
(C := ProC.finiteQuotientClass) (G := H) i.target.2)The target component map used by finite Fox semidirect stages.
theorem freeProCRelationReflectionTargetStageRight_generator
(sourceData : FreeProCSourceData ProC) {r : Nat}
(hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi)
(i : ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom)
(x : ULift.{u} (Fin r)) :
freeProCRelationReflectionTargetStageRight (ProC := ProC) sourceData hbasis psi hpsi i
(psi (freeProCReflectionFamily (ProC := ProC) sourceData hbasis x)) =
QuotientGroup.mk'
(freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi i)
(FreeGroup.of x)The target-stage right map sends the chosen generator to its quotient class in the relation-reflection target stage.
Show proof
by
change
freeProCRelationReflectionTargetStageQMap
(ProC := ProC) sourceData hbasis psi hpsi i
(QuotientGroup.mk
(psi (freeProCReflectionFamily (ProC := ProC) sourceData hbasis x))) =
QuotientGroup.mk'
(freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi i)
(FreeGroup.of x)
exact freeProCRelationReflectionTargetStageQMap_generator
(ProC := ProC) sourceData hbasis psi hpsi i 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. For separated or completed versions, each map is compared after all finite-stage projections; those projections separate points and commute with the sequence maps. Injectivity follows by applying the separating family of finite-stage projections to the difference of two possible preimages. Surjectivity is proved by lifting the target coordinates at finite stages and checking that the boundary formula maps the lift to the prescribed target element. 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.
□def freeProCRelationReflectionTargetStageMap
(sourceData : FreeProCSourceData ProC) {r : Nat}
(hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi)
(i : ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :
ZCCompletedFoxSemidirect ProC.finiteQuotientClass (ULift.{u} (Fin r)) H →*
FiniteFoxStageSemidirect
(X := ULift.{u} (Fin r))
(freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi i)
i.target.1.modulus := by
letI : ∀ j : ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom,
Fact (0 < j.target.1.modulus) :=
fun j => ProCGroups.Completion.ProCIntegerIndex.positiveFact j.target.1
exact
freeProCZCCompletedFoxSemidirectZCBifilteredStageMap
(ProC := ProC) (X := ULift.{u} (Fin r)) (H := H)
(Nstage := fun j =>
freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi j)
(nstage := fun j => j.target.1.modulus)
(zcIndex := fun j => j.target)
(hmod := fun _ => dvd_rfl)
(qmap := fun j =>
freeProCRelationReflectionTargetStageQMap
(ProC := ProC) sourceData hbasis psi hpsi j)
itheorem freeProCRelationReflection_finiteStage_relationBoundaryModuleExact
(sourceData : FreeProCSourceData ProC) {r : Nat}
(hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(i : ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :
finiteFoxStageRelationBoundaryModuleExact
(X := ULift.{u} (Fin r))
(freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi i)
i.target.1.modulusShow proof
by
exact
finiteFoxStageRelationBoundaryModuleExact_of_sourceBoundaryRelReduction
(X := ULift.{u} (Fin r))
(freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi i)
i.target.1.modulus
(finiteFoxStageSourceBoundaryRelationIdealReduction_of_relationIdeal_derivatives
(X := ULift.{u} (Fin r))
(freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi i)
i.target.1.modulus)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.
□