theorem eq_of_continuous_of_topologicallyGenerates
(hdelta : IsCrossedDifferential coeff delta)
(hepsilon : IsCrossedDifferential coeff epsilon)
(hdelta_continuous : Continuous delta) (hepsilon_continuous : Continuous epsilon)
{s : Set G} (hsgen : TopologicallyGenerates (G := G) s)
(hs : Set.EqOn delta epsilon s) :
delta = epsilonContinuous crossed differentials with the same coefficients are determined by a topological generating set.
Show proof
by
let K : Subgroup G :=
{ carrier := {g | delta g = epsilon g}
one_mem' := by
change delta 1 = epsilon 1
rw [hdelta.one, hepsilon.one]
mul_mem' := by
intro a b ha hb
change delta (a * b) = epsilon (a * b)
rw [hdelta.mul a b, hepsilon.mul a b, ha, hb]
inv_mem' := by
intro a ha
change delta a⁻¹ = epsilon a⁻¹
rw [hdelta.inv a, hepsilon.inv a, ha] }
have hKclosed : IsClosed ((K : Subgroup G) : Set G) := by
change IsClosed {g | delta g = epsilon g}
exact isClosed_eq hdelta_continuous hepsilon_continuous
have hsub : Subgroup.closure s ≤ K := by
rw [Subgroup.closure_le]
intro x hx
exact hs hx
have htop : (⊤ : Subgroup G) ≤ K := by
have hcl : (Subgroup.closure s).topologicalClosure ≤ K :=
Subgroup.topologicalClosure_minimal _ hsub hKclosed
rw [TopologicallyGenerates] at hsgen
simpa [hsgen] using hcl
funext g
simpa [K] using htop (show g ∈ (⊤ : Subgroup G) from by simp only [Subgroup.mem_top])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\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. 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. 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. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. 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 eq_of_freeProC_of_continuous
{ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
{coeff : F →* R} {delta epsilon : F → A}
(hdelta : IsCrossedDifferential coeff delta)
(hepsilon : IsCrossedDifferential coeff epsilon)
(hdelta_continuous : Continuous delta) (hepsilon_continuous : Continuous epsilon)
(hbasis : ∀ x : X, delta (ι x) = epsilon (ι x)) :
delta = epsilonContinuous crossed differentials on a free pro-\(C\) source are determined by their values on the free pro-\(C\) generators.
Show proof
by
refine
eq_of_continuous_of_topologicallyGenerates
hdelta hepsilon hdelta_continuous hepsilon_continuous hι.generates_range ?_
rintro _ ⟨x, rfl⟩
exact hbasis xProof. 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\). 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. 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. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. 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 zcUniversalDifferential_kernel_le_closedCommutator_of_crossedDifferential
(ψ : G →ₜ* H) (D : G → A)
(hD : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) D)
(hkerD :
∀ n : ProfiniteKernelSubgroup ψ, D n.1 = 0 →
n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) :
∀ n : ProfiniteKernelSubgroup ψ,
zcUniversalDifferential C ψ.toMonoidHom n.1 = 0 →
n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)To prove the universal completed Magnus-kernel criterion, it is enough to prove it for any crossed differential represented by the completed universal differential.
Show proof
by
intro n hn
exact hkerD n
(crossedDifferential_eq_zero_of_zcUniversalDifferential_eq_zero
(C := C) ψ.toMonoidHom D hD hn)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\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. 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. 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. 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.
□instance instT1SpaceMultiplicativeTarget : T1Space (Multiplicative A) := by
change T1Space A
infer_instanceThe multiplicative target object is \(T_1\) for its finite-stage topology.
def zcCrossedDifferentialKernelHom
(ψ : G →ₜ* H) (D : G → A)
(hD : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) D) :
ProfiniteKernelSubgroup ψ →* Multiplicative A where
toFun n := Multiplicative.ofAdd (D n.1)
map_one' := by
rw [Submonoid.coe_one]
exact congrArg Multiplicative.ofAdd (IsCrossedDifferential.one hD)
map_mul' n m := by
apply Multiplicative.ext
change D ((n * m : ProfiniteKernelSubgroup ψ) : G) = D n.1 + D m.1
rw [Submonoid.coe_mul, hD n.1 m.1]
have hn : ψ n.1 = 1 := n.2
simp only [ContinuousMonoidHom.coe_toMonoidHom, zcCompletedGroupAlgebraScalar_apply, MonoidHom.coe_coe, hn,
map_one, one_smul]The restriction of a completed crossed differential to the kernel of its coefficient homomorphism, multiplicatively valued in the additive target.
theorem continuous_zcCrossedDifferentialKernelHom
(ψ : G →ₜ* H) (D : G → A)
(hD : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) D)
(hcont : Continuous D) :
Continuous (zcCrossedDifferentialKernelHom (C := C) ψ D hD)The crossed-differential kernel homomorphism is continuous for the topology determined by the completed Fox coordinates.
Show proof
by
change Continuous fun n : ProfiniteKernelSubgroup ψ => Multiplicative.ofAdd (D n.1)
exact continuous_ofAdd.comp (hcont.comp continuous_subtype_val)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\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. 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. 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. 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. 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 zcCrossedDifferentialProfiniteKernelAbelianizationHom
(ψ : G →ₜ* H) (D : G → A)
(hD : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) D)
(hcont : Continuous D) :
ProfiniteKernelAbelianization ψ →* Multiplicative A :=
(ProCGroups.Abelian.TopologicalAbelianization.lift
{ toMonoidHom := zcCrossedDifferentialKernelHom (C := C) ψ D hD
continuous_toFun :=
continuous_zcCrossedDifferentialKernelHom (C := C) ψ D hD hcont }).toMonoidHomA continuous crossed differential on G descends along the completed kernel abelianization of its coefficient homomorphism. This is the natural target of the completed relation-module map.
def zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom
(ψ : G →ₜ* H) (D : G → A)
(hD : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) D)
(hcont : Continuous D) :
ProfiniteKernelAbelianizationAdd ψ →+ A :=
(zcCrossedDifferentialProfiniteKernelAbelianizationHom
(C := C) ψ D hD hcont).toAdditiveLeftAdditive form of \(\mathrm{zcCrossedDifferentialProfiniteKernelAbelianizationHom}\).
theorem zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom_mk
(ψ : G →ₜ* H) (D : G → A)
(hD : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) D)
(hcont : Continuous D) (n : ProfiniteKernelSubgroup ψ) :
zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom
(C := C) ψ D hD hcont
(Additive.ofMul (QuotientGroup.mk' (Subgroup.closedCommutator _) n)) =
D n.1The completed crossed differential induces an additive monoid homomorphism from the topological kernel abelianization.
Show proof
by
have h :=
ProCGroups.Abelian.TopologicalAbelianization.lift_apply_mk
({ toMonoidHom := zcCrossedDifferentialKernelHom (C := C) ψ D hD
continuous_toFun :=
continuous_zcCrossedDifferentialKernelHom (C := C) ψ D hD hcont } :
ProfiniteKernelSubgroup ψ →ₜ* Multiplicative A) n
simpa [zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom,
zcCrossedDifferentialProfiniteKernelAbelianizationHom,
zcCrossedDifferentialKernelHom,
ProCGroups.Abelian.TopologicalAbelianization.mk] using
congrArg Multiplicative.toAdd hProof. 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\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. 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. 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. 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 zcCrossedDifferential_eq_zero_of_mem_closedCommutator
(ψ : G →ₜ* H) (D : G → A)
(hD : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) D)
(hcont : Continuous D) {n : ProfiniteKernelSubgroup ψ}
(hn : n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) :
D n.1 = 0A continuous completed crossed differential kills the closed commutator subgroup of the kernel of its coefficient homomorphism.
Show proof
by
let F :=
zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom
(C := C) ψ D hD hcont
have hnq :
QuotientGroup.mk' (Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) n = 1 :=
(QuotientGroup.eq_one_iff
(N := Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) n).2 hn
have h :=
congrArg (fun q : ProfiniteKernelAbelianization ψ => F (Additive.ofMul q)) hnq
simpa [F] using hProof. 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\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. 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. 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. 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 zcCrossedDiffProfiniteKernelAbelianizationAddMonoidHom_inj_of_kernel_le_closedCommutator
(ψ : G →ₜ* H) (D : G → A)
(hD : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) D)
(hcont : Continuous D)
(hker :
∀ n : ProfiniteKernelSubgroup ψ, D n.1 = 0 →
n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) :
Function.Injective
(zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom
(C := C) ψ D hD hcont)The induced map from the topological kernel abelianization is injective when the kernel of the crossed differential is contained in the closed commutator subgroup.
Show proof
by
intro x y hxy
suffices x - y = 0 by exact sub_eq_zero.mp this
let F :=
zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom
(C := C) ψ D hD hcont
have hmap : F (x - y) = 0 := by
rw [map_sub, hxy, sub_self]
have hzero_of_map_zero :
∀ z : ProfiniteKernelAbelianizationAdd ψ, F z = 0 → z = 0 := by
intro z hz
apply Additive.toMul.injective
change (Additive.toMul z : ProfiniteKernelAbelianization ψ) = 1
revert hz
change
(fun q : ProfiniteKernelAbelianization ψ =>
F (Additive.ofMul q) = 0 → q = 1) (Additive.toMul z)
refine QuotientGroup.induction_on (Additive.toMul z) ?_
intro n hn
change QuotientGroup.mk' (Subgroup.closedCommutator _) n = 1
exact (QuotientGroup.eq_one_iff
(N := Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) n).2
(hker n (by simpa [F] using hn))
exact hzero_of_map_zero (x - y) hmapProof. 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\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. 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. 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. 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 zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom_injective_iff
(ψ : G →ₜ* H) (D : G → A)
(hD : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) D)
(hcont : Continuous D) :
Function.Injective
(zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom
(C := C) ψ D hD hcont) ↔
∀ n : ProfiniteKernelSubgroup ψ, D n.1 = 0 →
n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)Injectivity of the induced map on the topological kernel abelianization is equivalent to the continuous Magnus-kernel criterion.
Show proof
by
constructor
· intro hinj n hn
let F :=
zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom
(C := C) ψ D hD hcont
have hzero :
F (Additive.ofMul
(QuotientGroup.mk' (Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) n)) =
F 0 := by
simpa [F, hn]
have hclass :
Additive.ofMul
(QuotientGroup.mk' (Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) n) =
0 := hinj hzero
have hmk :
QuotientGroup.mk' (Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) n = 1 := by
simpa using congrArg Additive.toMul hclass
exact (QuotientGroup.eq_one_iff
(N := Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) n).1 hmk
· intro hker
exact
zcCrossedDiffProfiniteKernelAbelianizationAddMonoidHom_inj_of_kernel_le_closedCommutator
(C := C) ψ D hD hcont hkerProof. 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\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. 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. 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.
□theorem freeProCZCBoundary_of_topologicalGeneration
{ι : X → G}
(hgen : TopologicallyGenerates (G := G) (Set.range ι))
(ψ : G →* H) (delta : G → ZCFreeFoxCoordinates C (X := X) (H := H))
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
(hbasis :
∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H))
(g : G) :
freeProCZCCompletedFoxBoundary C (fun x : X => ψ (ι x)) (delta g) =
zcCompletedGroupAlgebraBoundary C ψ gShow proof
by
let beta : G → ZCCompletedGroupAlgebra C H :=
fun g => freeProCZCCompletedFoxBoundary C (fun x : X => ψ (ι x)) (delta g)
have hbeta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) beta :=
IsCrossedDifferential.map_linear hdelta
(freeProCZCCompletedFoxBoundary C (fun x : X => ψ (ι x)))
have hboundary :
IsCrossedDifferential
(zcCompletedGroupAlgebraScalar C ψ) (zcCompletedGroupAlgebraBoundary C ψ) :=
zcCompletedGroupAlgebraBoundary_isCrossedDifferential C ψ
have hbeta_continuous : Continuous beta :=
(continuous_freeProCZCCompletedFoxBoundary C (fun x : X => ψ (ι x))).comp hdelta_continuous
have hboundary_continuous : Continuous (zcCompletedGroupAlgebraBoundary C ψ) :=
continuous_zcCompletedGroupAlgebraBoundary (C := C) (G := H) ψ hψ_continuous
have hEqOn :
Set.EqOn beta (zcCompletedGroupAlgebraBoundary C ψ) (Set.range ι) := by
intro y hy
rcases hy with ⟨x, rfl⟩
simp only [hbasis x, freeProCZCCompletedFoxBoundary_single, zcCompletedGroupAlgebraBoundary, beta]
have hEq :=
IsCrossedDifferential.eq_of_continuous_of_topologicallyGenerates
hbeta hboundary hbeta_continuous hboundary_continuous hgen hEqOn
exact congrFun hEq gProof. 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\). 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. 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. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. 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_zcCrossedDiffKernelAddMonoidHom_freeProCZCCompletedFoxBoundary_of_surj_semi
(φ : X → H)
(ψ : G →* H) (delta : G → ZCFreeFoxCoordinates C (X := X) (H := H))
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(hboundary :
∀ g : G,
freeProCZCCompletedFoxBoundary C φ (delta g) =
zcCompletedGroupAlgebraBoundary C ψ g)
(hgraph :
Function.Surjective
(fun g : G =>
({ left := delta g, right := ψ g } :
ZCCompletedFoxSemidirect C X H))) :
Function.Exact
(zcCrossedDifferentialKernelAddMonoidHom C ψ delta hdelta)
(freeProCZCCompletedFoxBoundary C φ)Exactness at the finite completed Fox-coordinate term from a surjective semidirect graph. The hypothesis says that the crossed-differential graph g \(\mapsto\) (delta g, \(\psi(g)\)) fills \(\mathbb{Z}_C\llbracket H\rrbracket^{X}\) \(\rtimes\) H. Then every vector killed by the source-shaped Fox boundary is the derivative of an element of \(\ker \psi\).
Show proof
by
intro v
constructor
· intro hv
rcases hgraph
({ left := v, right := 1 } :
ZCCompletedFoxSemidirect C X H) with
⟨g, hg⟩
have hdelta_g : delta g = v := congrArg ZCCompletedFoxSemidirect.left hg
have hψ_g : ψ g = 1 := congrArg ZCCompletedFoxSemidirect.right hg
refine ⟨Additive.ofMul (⟨g, hψ_g⟩ : ψ.ker), ?_⟩
simp only [zcCrossedDifferentialKernelAddMonoidHom_apply, hdelta_g]
· rintro ⟨n, hn⟩
rw [← hn]
change
freeProCZCCompletedFoxBoundary C φ
(delta (((Additive.toMul n : ψ.ker) : G))) = 0
rw [hboundary (((Additive.toMul n : ψ.ker) : G))]
exact zcCompletedGroupAlgebraBoundary_eq_zero_of_mem_ker
(C := C) (ψ := ψ) (g := ((Additive.toMul n : ψ.ker) : G))
(Additive.toMul n).2Proof. 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\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. 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. 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.
□theorem zcCompletedFoxSemidirect_surjective_forces_generator_boundary_zero
(φ : X → H)
(ψ : G →* H) (delta : G → ZCFreeFoxCoordinates C (X := X) (H := H))
(hboundary :
∀ g : G,
freeProCZCCompletedFoxBoundary C φ (delta g) =
zcCompletedGroupAlgebraBoundary C ψ g)
(hgraph :
Function.Surjective
(fun g : G =>
({ left := delta g, right := ψ g } :
ZCCompletedFoxSemidirect C X H))) (x : X) :
zcGroupLike C H (φ x) - 1 = 0If a completed semidirect Fox lift onto \(\mathbb{Z}_C\llbracket H\rrbracket^{X} \rtimes H\) is actually surjective, then every generator boundary \([\varphi(x)]-1\) must vanish. This is a useful diagnostic obstruction: the graph generators of a free source cannot generally topologically generate the whole semidirect product.
Show proof
by
rcases hgraph
({ left := Pi.single x (1 : ZCCompletedGroupAlgebra C H), right := 1 } :
ZCCompletedFoxSemidirect C X H) with
⟨g, hg⟩
have hdelta_g : delta g = Pi.single x (1 : ZCCompletedGroupAlgebra C H) :=
congrArg ZCCompletedFoxSemidirect.left hg
have hψ_g : ψ g = 1 := congrArg ZCCompletedFoxSemidirect.right hg
calc
zcGroupLike C H (φ x) - 1 =
freeProCZCCompletedFoxBoundary C φ
(Pi.single x (1 : ZCCompletedGroupAlgebra C H)) := by
rw [freeProCZCCompletedFoxBoundary_single]
_ = freeProCZCCompletedFoxBoundary C φ (delta g) := by rw [hdelta_g]
_ = zcCompletedGroupAlgebraBoundary C ψ g := hboundary g
_ = 0 := by simp only [zcCompletedGroupAlgebraBoundary, hψ_g, map_one, sub_self]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\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. 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. 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. 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. 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_zcKernelAdd_freeProCZCFoxBoundary_of_topGen
{ι : X → G}
(hgen : TopologicallyGenerates (G := G) (Set.range ι))
(ψ : G →* H) (delta : G → ZCFreeFoxCoordinates C (X := X) (H := H))
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
(hbasis :
∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H))
(hgraph :
Function.Surjective
(fun g : G =>
({ left := delta g, right := ψ g } :
ZCCompletedFoxSemidirect C X H))) :
Function.Exact
(zcCrossedDifferentialKernelAddMonoidHom C ψ delta hdelta)
(freeProCZCCompletedFoxBoundary C (fun x : X => ψ (ι x)))Exactness at the finite completed Fox-coordinate term, with the boundary identity supplied by continuity and topological generation of the source generators.
Show proof
by
exact
exact_zcCrossedDiffKernelAddMonoidHom_freeProCZCCompletedFoxBoundary_of_surj_semi
(C := C) (X := X) (G := G) (H := H)
(fun x : X => ψ (ι x)) ψ delta hdelta
(freeProCZCBoundary_of_topologicalGeneration
(C := C) (X := X) (G := G) (H := H)
hgen ψ delta hdelta hdelta_continuous hψ_continuous hbasis)
hgraphProof. 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\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. 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. 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.
□theorem freeProCZCFundamentalFormula_of_topologicalGeneration
{ι : X → G}
(hgen : TopologicallyGenerates (G := G) (Set.range ι))
(ψ : G →* H) (delta : G → ZCFreeFoxCoordinates C (X := X) (H := H))
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
(hbasis :
∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H))
(g : G) :
zcCompletedGroupAlgebraBoundary C ψ g =
∑ x : X, delta g x * (zcGroupLike C H (ψ (ι x)) - 1)Source-shaped completed Fox fundamental formula from continuity and topological generation.
Show proof
by
simpa [freeProCZCCompletedFoxBoundary_apply] using
(freeProCZCBoundary_of_topologicalGeneration
(X := X) (G := G) (H := H) C hgen ψ delta hdelta hdelta_continuous hψ_continuous hbasis g).symmProof. 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\). 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. 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. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. 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 freeProCZCFundamentalFormula_stage_of_topologicalGeneration
{ι : X → G}
(hgen : TopologicallyGenerates (G := G) (Set.range ι))
(ψ : G →* H) (delta : G → ZCFreeFoxCoordinates C (X := X) (H := H))
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
(hbasis :
∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H))
(j : ZCCompletedGroupAlgebraIndex C H) (g : G) :
zcCompletedGroupAlgebraProjection C H j
(zcCompletedGroupAlgebraBoundary C ψ g) =
zcCompletedGroupAlgebraProjection C H j
(∑ x : X, delta g x * (zcGroupLike C H (ψ (ι x)) - 1))The finite-stage projection of the source-shaped completed Fox formula obtained from continuity and topological generation.
Show proof
by
exact congrArg (zcCompletedGroupAlgebraProjection C H j)
(freeProCZCFundamentalFormula_of_topologicalGeneration
(X := X) (G := G) (H := H) C hgen ψ delta hdelta hdelta_continuous hψ_continuous hbasis g)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\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. 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. 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 freeProCZCEulerFormula_of_topologicalGeneration
{ι : X → G}
(hgen : TopologicallyGenerates (G := G) (Set.range ι))
(ψ : G →* H) (delta : G → ZCFreeFoxCoordinates C (X := X) (H := H))
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
(hbasis :
∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H))
(g : G) :
zcGroupLike C H (ψ g) - 1 =
∑ x : X, delta g x * (zcGroupLike C H (ψ (ι x)) - 1)Explicit Euler-sum form from continuity and topological generation.
Show proof
by
simpa [zcCompletedGroupAlgebraBoundary] using
freeProCZCFundamentalFormula_of_topologicalGeneration
(X := X) (G := G) (H := H) C hgen ψ delta hdelta hdelta_continuous hψ_continuous hbasis gProof. 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\). 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. 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. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. 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 freeProCZCCompletedCrossedDifferential_ext_of_continuous
{ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
(ψ : F →* H)
(delta epsilon :
F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
(hdelta :
IsCrossedDifferential (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) delta)
(hepsilon :
IsCrossedDifferential (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) epsilon)
(hdelta_continuous : Continuous delta) (hepsilon_continuous : Continuous epsilon)
(hbasis : ∀ x : X, delta (ι x) = epsilon (ι x)) :
delta = epsilonExtensionality for continuous completed crossed differentials on a free pro-\(C\) source, using continuity of the coordinate-valued maps themselves.
Show proof
by
exact IsCrossedDifferential.eq_of_freeProC_of_continuous
(ProC := ProC) hι hdelta hepsilon hdelta_continuous hepsilon_continuous hbasisProof. 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\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. 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. 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. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. 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.
□