CrowellExactSequence.Profinite.FreeProCSourceData
This module develops the Crowell--Blanchfield--Lyndon exact sequence and its completed coordinate forms.
structure FreeProCSourceData (ProC : ProCGroupPredicate.{u}) where
basis : Type u
carrier : Type u
instGroup : Group carrier
instTopologicalSpace : TopologicalSpace carrier
instIsTopologicalGroup : IsTopologicalGroup carrier
inclusion : basis → carrier
isFree :
ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
(ProC := ProC) basis carrier inclusion
proCGroup : ProCGroup ProC carrierPackaged carrier for a free pro-\(C\) group on a set converging to \(1\).
instance FreeProCSourceData.instProCGroup
{ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC) :
ProCGroup ProC sourceData.carrier :=
sourceData.proCGroupThe profinite group carried by the free pro-\(C\) source data is pro-\(C\), because its finite quotients lie in the prescribed class and the class is stable under the required operations.
def freeProCChosenBasisEquivOfBasisCard
{ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
{n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :
sourceData.basis ≃ Fin n :=
Classical.choice ((Cardinal.mk_eq_nat_iff).1 hbasis)Choose an equivalence from a finite free pro-\(C\) basis to \(\operatorname{Fin} n\).
def freeProCChosenFamilyOfBasisCard
{ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
{n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :
Fin n → sourceData.carrier :=
fun i =>
sourceData.inclusion
((freeProCChosenBasisEquivOfBasisCard (ProC := ProC) sourceData hbasis).symm i)The concrete \(\operatorname{Fin} n\)-indexed family obtained from the chosen free pro-\(C\) basis.
def freeProCChosenULiftFamilyOfBasisCard
{ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
{n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :
ULift.{u} (Fin n) → sourceData.carrier :=
fun i => freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis i.downtheorem freeProCChosenULiftFamilyOfBasisCard_range
{ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
{n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :
Set.range (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis) =
Set.range (freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis)The lifted chosen family has the same range as the concrete \(\operatorname{Fin} n\) family.
Show proof
by
ext g
constructor
· rintro ⟨i, rfl⟩
exact ⟨i.down, rfl⟩
· rintro ⟨i, rfl⟩
exact ⟨ULift.up i, rfl⟩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. 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 freeProCChosenFamilyOfBasisCard_isFree
{ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
{n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :
ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
(ProC := ProC) (Fin n) sourceData.carrier
(freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis)The concrete \(\operatorname{Fin} n\)-indexed chosen family is the same free pro-\(C\) converging basis, reindexed. This is the finite-coordinate form used by the Crowell exactness assembly.
Show proof
by
let e : Fin n ≃ sourceData.basis :=
(freeProCChosenBasisEquivOfBasisCard (ProC := ProC) sourceData hbasis).symm
simpa [freeProCChosenFamilyOfBasisCard, e] using
sourceData.isFree.precompEquiv eProof. 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. 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 freeProCChosenULiftFamilyOfBasisCard_isFree
{ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
{n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :
ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
(ProC := ProC) (ULift.{u} (Fin n)) sourceData.carrier
(freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)Reindexing identifies the lifted chosen \(\operatorname{Fin} n\)-indexed family with the same free pro-\(C\) converging basis.
Show proof
by
let e : ULift.{u} (Fin n) ≃ sourceData.basis :=
{ toFun := fun i =>
(freeProCChosenBasisEquivOfBasisCard (ProC := ProC) sourceData hbasis).symm i.down
invFun := fun b =>
ULift.up ((freeProCChosenBasisEquivOfBasisCard (ProC := ProC) sourceData hbasis) b)
left_inv := by
intro i
cases i
simp only [Equiv.apply_symm_apply]
right_inv := by
intro b
simp only [Equiv.symm_apply_apply]}
simpa [freeProCChosenULiftFamilyOfBasisCard, freeProCChosenFamilyOfBasisCard, e] using
sourceData.isFree.precompEquiv eProof. 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 freeProCChosenFamilyOfBasisCard_generates
{ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
{n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :
ProCGroups.Generation.TopologicallyGenerates
(G := sourceData.carrier)
(Set.range (freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis))Reindexing the chosen basis by \(\operatorname{Fin} n\) preserves topological generation.
Show proof
by
classical
have hRange :
Set.range (freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis) =
Set.range sourceData.inclusion := by
ext g
constructor
· rintro ⟨i, rfl⟩
exact
⟨(freeProCChosenBasisEquivOfBasisCard (ProC := ProC) sourceData hbasis).symm i, rfl⟩
· rintro ⟨b, rfl⟩
exact
⟨(freeProCChosenBasisEquivOfBasisCard (ProC := ProC) sourceData hbasis) b, by
simp only [freeProCChosenFamilyOfBasisCard, Equiv.symm_apply_apply]⟩
simpa [hRange] using sourceData.isFree.generates_rangeProof. 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 freeProCChosenFamilyOfBasisCard_image_convergesToOne
{ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
{n : Nat} (hbasis : Cardinal.mk sourceData.basis = n)
{H : Type u} [Group H] [TopologicalSpace H] (ψ : sourceData.carrier → H) :
ProCGroups.FreeProC.FamilyConvergesToOne
(G := H)
(fun i : Fin n =>
ψ (freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis i))The image of the concrete chosen finite free basis under any map converges to \(1\), because the indexing type is finite.
Show proof
by
exact ProCGroups.FreeProC.FamilyConvergesToOne.of_finite_domain
(G := H)
(fun i : Fin n =>
ψ (freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis i))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 freeProCChosenFamilyOfBasisCard_image_generates_of_surjective
{ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
{n : Nat} (hbasis : Cardinal.mk sourceData.basis = n)
{H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi) :
ProCGroups.Generation.TopologicallyGenerates
(G := H)
(Set.range
(fun i : Fin n =>
psi (freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis i)))A surjective continuous homomorphism carries the chosen finite free basis to a topological generating family of the target.
Show proof
by
let family : Fin n → sourceData.carrier :=
freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis
have hsourceGen :
ProCGroups.Generation.TopologicallyGenerates
(G := sourceData.carrier) (Set.range family) := by
simpa [family] using
freeProCChosenFamilyOfBasisCard_generates (ProC := ProC) sourceData hbasis
have himage :=
ProCGroups.Generation.topologicallyGenerates_image_of_continuousMonoidHom_surjective
(G := sourceData.carrier) (H := H) psi hpsi hsourceGen
have hrange :
psi '' Set.range family = Set.range (fun i : Fin n => psi (family i)) := by
ext h
constructor
· rintro ⟨g, ⟨i, rfl⟩, rfl⟩
exact ⟨i, rfl⟩
· rintro ⟨i, rfl⟩
exact ⟨family i, ⟨i, rfl⟩, rfl⟩
simpa [family, hrange] using himageProof. 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 freeProCChosenULiftFamilyOfBasisCard_generates
{ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
{n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :
ProCGroups.Generation.TopologicallyGenerates
(G := sourceData.carrier)
(Set.range (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis))The universe-lifted chosen family also topologically generates the free pro-\(C\) source.
Show proof
by
simpa [freeProCChosenULiftFamilyOfBasisCard_range (ProC := ProC) sourceData hbasis] using
freeProCChosenFamilyOfBasisCard_generates (ProC := ProC) sourceData hbasisProof. 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 freeProCChosenULiftFamilyOfBasisCard_image_convergesToOne
{ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
{n : Nat} (hbasis : Cardinal.mk sourceData.basis = n)
{H : Type u} [Group H] [TopologicalSpace H]
(ψ : sourceData.carrier →* H) :
ProCGroups.FreeProC.FamilyConvergesToOne
(G := H)
(fun i : ULift.{u} (Fin n) =>
ψ (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis i))The image of the finite lifted basis under any target homomorphism converges to \(1\) in the converging-set sense used by the free pro-\(C\) formulation.
Show proof
by
exact ProCGroups.FreeProC.FamilyConvergesToOne.of_finite_domain
(G := H)
(fun i : ULift.{u} (Fin n) =>
ψ (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis i))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 freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
{ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
{n : Nat} (hbasis : Cardinal.mk sourceData.basis = n)
{H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi) :
ProCGroups.Generation.TopologicallyGenerates
(G := H)
(Set.range
(fun i : ULift.{u} (Fin n) =>
psi (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis i)))A surjective continuous homomorphism carries the lifted chosen finite free basis to a topological generating family of the target.
Show proof
by
let family : Fin n → sourceData.carrier :=
freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis
let liftedFamily : ULift.{u} (Fin n) → sourceData.carrier :=
freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
have hfin :
ProCGroups.Generation.TopologicallyGenerates
(G := H) (Set.range (fun i : Fin n => psi (family i))) := by
simpa [family] using
freeProCChosenFamilyOfBasisCard_image_generates_of_surjective
(ProC := ProC) sourceData hbasis psi hpsi
have hrange :
Set.range (fun i : ULift.{u} (Fin n) => psi (liftedFamily i)) =
Set.range (fun i : Fin n => psi (family i)) := by
ext h
constructor
· rintro ⟨i, rfl⟩
exact ⟨i.down, rfl⟩
· rintro ⟨i, rfl⟩
exact ⟨ULift.up i, rfl⟩
simpa [family, liftedFamily, hrange] using hfinProof. 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 freeProCChosenULiftFamilyOfBasisCard_liftHom_eq_of_surjective
{ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
{n : Nat} (hbasis : Cardinal.mk sourceData.basis = n)
{H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(hH : ProC (G := H))
(psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi) :
(freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis).liftHom hH
(fun i : ULift.{u} (Fin n) =>
psi (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis i))
(freeProCChosenULiftFamilyOfBasisCard_image_convergesToOne
(ProC := ProC) sourceData hbasis psi.toMonoidHom)
(freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
(ProC := ProC) sourceData hbasis psi hpsi) =
psiFor the lifted finite free basis, the converging-set universal lift of a surjective target map is the target map itself. This is the concrete bridge needed when Fox constructions produce a right component from the universal property.
Show proof
by
let hfree :=
freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
let liftedFamily : ULift.{u} (Fin n) → sourceData.carrier :=
freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
let φ : ULift.{u} (Fin n) → H := fun i => psi (liftedFamily i)
let hconv :
ProCGroups.FreeProC.FamilyConvergesToOne (G := H) φ :=
by
simpa [φ, liftedFamily] using
freeProCChosenULiftFamilyOfBasisCard_image_convergesToOne
(ProC := ProC) sourceData hbasis psi.toMonoidHom
let hgen :
ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ) := by
simpa [φ, liftedFamily] using
freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
(ProC := ProC) sourceData hbasis psi hpsi
ext g
have hmon :
psi.toMonoidHom = hfree.lift hH φ hconv hgen :=
hfree.lift_unique hH φ hconv hgen psi.continuous_toFun (by
intro i
rfl)
exact (congrArg (fun f : sourceData.carrier →* H => f g) hmon).symmProof. 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.
□