FoxDifferential.Completed.Continuous.TailExactness
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
theorem exact_foxBoundaryMap_zcGroupLike_sub_one_of_topologicallyGenerates
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(φ : X → H) (hφ : TopologicallyGenerates (G := H) (Set.range φ)) :
Function.Exact
(foxBoundaryMap (fun x : X => zcGroupLike C H (φ x) - 1) :
(X → ZCCompletedGroupAlgebra C H) → ZCCompletedGroupAlgebra C H)
(zcCompletedGroupAlgebraAugmentation C H :
ZCCompletedGroupAlgebra C H → ZCCoeff C)Show proof
by
let L : (X → ZCCompletedGroupAlgebra C H) →ₗ[ZCCompletedGroupAlgebra C H]
ZCCompletedGroupAlgebra C H :=
foxBoundaryMap (fun x : X => zcGroupLike C H (φ x) - 1)
have hclosedRange :
IsClosed ((LinearMap.range L : Submodule (ZCCompletedGroupAlgebra C H)
(ZCCompletedGroupAlgebra C H)) : Set (ZCCompletedGroupAlgebra C H)) := by
change IsClosed (Set.range L)
have hrange :
Set.range L = (fun v : X → ZCCompletedGroupAlgebra C H => L v) '' Set.univ := by
ext y
constructor
· rintro ⟨v, rfl⟩
exact ⟨v, trivial, rfl⟩
· rintro ⟨v, _hv, rfl⟩
exact ⟨v, rfl⟩
rw [hrange]
simpa [L] using
(isCompact_univ.image (continuous_foxBoundaryMap
(fun x : X => zcGroupLike C H (φ x) - 1))).isClosed
let K : Subgroup H :=
{ carrier := {h | zcGroupLike C H h - 1 ∈ LinearMap.range L}
one_mem' := by
change zcCompletedGroupAlgebraBoundary C (MonoidHom.id H) (1 : H) ∈
LinearMap.range L
simp only [MonoidHom.id_apply, zcCompletedGroupAlgebraBoundary_eq_zero_of_mem_ker, zero_mem]
mul_mem' := by
intro a b ha hb
change zcCompletedGroupAlgebraBoundary C (MonoidHom.id H) (a * b) ∈
LinearMap.range L
rw [zcCompletedGroupAlgebraBoundary_mul]
exact (LinearMap.range L).add_mem ha ((LinearMap.range L).smul_mem _ hb)
inv_mem' := by
intro a ha
change zcCompletedGroupAlgebraBoundary C (MonoidHom.id H) a⁻¹ ∈
LinearMap.range L
rw [zcCompletedGroupAlgebraBoundary_inv]
exact (LinearMap.range L).neg_mem ((LinearMap.range L).smul_mem _ ha) }
have hKclosed : IsClosed ((K : Subgroup H) : Set H) := by
change IsClosed {h : H | zcGroupLike C H h - 1 ∈
(LinearMap.range L : Submodule (ZCCompletedGroupAlgebra C H)
(ZCCompletedGroupAlgebra C H))}
exact hclosedRange.preimage
((continuous_zcGroupLike (C := C) (G := H)).sub continuous_const)
have hsub : Subgroup.closure (Set.range φ) ≤ K := by
rw [Subgroup.closure_le]
rintro h ⟨x, rfl⟩
change zcGroupLike C H (φ x) - 1 ∈ LinearMap.range L
exact ⟨Pi.single x (1 : ZCCompletedGroupAlgebra C H), by
simp only [foxBoundaryMap_single, L]⟩
have htop : (⊤ : Subgroup H) ≤ K := by
have hcl : (Subgroup.closure (Set.range φ)).topologicalClosure ≤ K :=
Subgroup.topologicalClosure_minimal _ hsub hKclosed
rw [TopologicallyGenerates] at hφ
simpa [hφ] using hcl
have hstandard_le_range :
(zcCompletedGroupAlgebraStandardAugmentationIdeal C H :
Submodule (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebra C H)) ≤
LinearMap.range L := by
rw [zcCompletedGroupAlgebraStandardAugmentationIdeal_eq_span]
refine Submodule.span_le.2 ?_
rintro _ ⟨h, rfl⟩
simpa [K, zcCompletedGroupAlgebraBoundary] using
htop (show h ∈ (⊤ : Subgroup H) from by simp only [Subgroup.mem_top])
have hrange_le_standard :
LinearMap.range L ≤
(zcCompletedGroupAlgebraStandardAugmentationIdeal C H :
Submodule (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebra C H)) := by
rintro y ⟨v, rfl⟩
rw [zcCompletedGroupAlgebraStandardAugmentationIdeal_eq_span]
change L v ∈ Submodule.span (ZCCompletedGroupAlgebra C H)
(Set.range fun h : H => zcGroupLike C H h - 1)
rw [show L v =
∑ x : X, v x * (zcGroupLike C H (φ x) - 1) from rfl]
exact Submodule.sum_mem _ fun x _ =>
Submodule.smul_mem _ (v x)
(Submodule.subset_span ⟨φ x, rfl⟩)
have haugmentation_le_range :
zcCompletedGroupAlgebraAugmentationIdeal C H ≤
(LinearMap.range L : Submodule (ZCCompletedGroupAlgebra C H)
(ZCCompletedGroupAlgebra C H)) := by
intro z hz
have hzClosure :
z ∈ closure
((zcCompletedGroupAlgebraStandardAugmentationIdeal C H :
Ideal (ZCCompletedGroupAlgebra C H)) : Set (ZCCompletedGroupAlgebra C H)) := by
rw [closure_zcCompletedGroupAlgebraStandardAugmentationIdeal_eq_augmentationIdeal
(C := C) (H := H) hForm]
exact hz
exact closure_minimal
(by intro y hy; exact hstandard_le_range hy) hclosedRange hzClosure
intro z
constructor
· intro hz
exact haugmentation_le_range
((mem_zcCompletedGroupAlgebraAugmentationIdeal_iff
(C := C) (H := H) (x := z)).2 hz)
· rintro ⟨x, rfl⟩
have hstd :
L x ∈ zcCompletedGroupAlgebraStandardAugmentationIdeal C H :=
hrange_le_standard ⟨x, rfl⟩
have haug :
L x ∈ zcCompletedGroupAlgebraAugmentationIdeal C H :=
zcCompletedGroupAlgebraStandardAugmentationIdeal_le_augmentationIdeal C H hstd
exact (mem_zcCompletedGroupAlgebraAugmentationIdeal_iff
(C := C) (H := H) (x := L x)).1 haugProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). Exactness is proved by identifying the image of the previous boundary map with the elements whose Fox coordinates vanish under the next boundary map, giving both inclusions at the finite stages. Completed assertions are checked after projection to every finite stage; continuity and closure follow from the inverse-limit topology and the closedness of the coordinate conditions. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. 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 exact_freeProCZCCompletedFoxBoundary_of_topologicallyGenerates
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(φ : X₀ → H) (hφ : TopologicallyGenerates (G := H) (Set.range φ)) :
Function.Exact
(freeProCZCCompletedFoxBoundary C φ :
(X₀ → ZCCompletedGroupAlgebra C H) → ZCCompletedGroupAlgebra C H)
(zcCompletedGroupAlgebraAugmentation C H :
ZCCompletedGroupAlgebra C H → ZCCoeff C)The sequence is used by identifying the image of the first map with the kernel of the second and by verifying injectivity and surjectivity at the two ends.
Show proof
by
simpa [freeProCZCCompletedFoxBoundary] using
(exact_foxBoundaryMap_zcGroupLike_sub_one_of_topologicallyGenerates
(C := C) (X := X₀) (H := H) hForm φ hφ)Proof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). Kernel and augmentation-ideal statements use the Fox fundamental identity, which expresses an element minus its augmentation in terms of the Fox derivatives of the chosen generators. Exactness is proved by identifying the image of the previous boundary map with the elements whose Fox coordinates vanish under the next boundary map, giving both inclusions at the finite stages. Surjectivity is obtained by choosing finite-stage lifts of the target coefficients and supports, verifying the derivative formula there, and assembling the compatible lifts. Completed assertions are checked after projection to every finite stage; continuity and closure follow from the inverse-limit topology and the closedness of the coordinate conditions. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. 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.
□