FoxDifferential.Completed.FreeProC.CofinalQuotientKernelBasis
This module supplies the topological part of the construction. It checks continuity and stagewise neighborhood properties so that the completed object inherits the required topology.
theorem HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_ker_le
(hbasis : HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π)
(hcofinal : ∀ j : J, ∃ k : K, (π' k).ker ≤ (π j).ker) :
HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π'Reindex an identity-neighborhood quotient-kernel basis along a cofinal refinement of kernels. The hypothesis says that every kernel in the original quotient family contains the kernel of some refined quotient. This is the topological input used to pass from all finite quotients to prime-power or otherwise cofinal stages.
Show proof
by
intro U hU hUone
rcases hbasis U hU hUone with ⟨j, hj⟩
rcases hcofinal j with ⟨k, hk⟩
refine ⟨k, ?_⟩
intro z hz
exact hj z (hk hz)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. 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 HasLeftQuotientKernelNeighbourhoodBasis.reindex_of_ker_le
(hbasis : HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) π)
(hcofinal : ∀ j : J, ∃ k : K, (π' k).ker ≤ (π j).ker) :
HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) π'Reindex an identity-neighborhood quotient-kernel basis along a cofinal refinement of kernels. The hypothesis says that every kernel in the original quotient family contains the kernel of some refined quotient. This is the topological input used to pass from all finite quotients to prime-power or otherwise cofinal stages.
Show proof
by
intro y U hU hyU
rcases hbasis y U hU hyU with ⟨j, hj⟩
rcases hcofinal j with ⟨k, hk⟩
refine ⟨k, ?_⟩
intro z hz
exact hj z (hk hz)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. 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 HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_factor
(hbasis : HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π)
(hrefine : ∀ j : J, ∃ k : K, ∃ τ : Q' k →* Q j, τ.comp (π' k) = π j) :
HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π'A factorization of the refined quotient through an original quotient gives the required kernel inclusion for identity-neighborhood reindexing.
Show proof
by
refine
HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_ker_le
(Y := Y) (π := π) (π' := π') hbasis ?_
intro j
rcases hrefine j with ⟨k, τ, hτ⟩
refine ⟨k, ?_⟩
intro z hz
change π j z = 1
have hz' : τ (π' k z) = 1 := by
rw [hz]
exact map_one τ
simpa [← hτ, MonoidHom.comp_apply] using hz'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. 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. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem HasLeftQuotientKernelNeighbourhoodBasis.reindex_of_factor
(hbasis : HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) π)
(hrefine : ∀ j : J, ∃ k : K, ∃ τ : Q' k →* Q j, τ.comp (π' k) = π j) :
HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) π'A factorization of the refined quotient through an original quotient gives the required kernel inclusion for identity-neighborhood reindexing.
Show proof
by
refine
HasLeftQuotientKernelNeighbourhoodBasis.reindex_of_ker_le
(Y := Y) (π := π) (π' := π') hbasis ?_
intro j
rcases hrefine j with ⟨k, τ, hτ⟩
refine ⟨k, ?_⟩
intro z hz
change π j z = 1
have hz' : τ (π' k z) = 1 := by
rw [hz]
exact map_one τ
simpa [← hτ, MonoidHom.comp_apply] using hz'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. 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. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem subset_closure_of_identityQuotientKernel_approximation_reindex
[IsTopologicalGroup Y]
{S T : Set Y}
(hbasis : HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π)
(hcofinal : ∀ j : J, ∃ k : K, (π' k).ker ≤ (π j).ker)
(happrox :
∀ y : Y, y ∈ T → ∀ k : K,
∃ s : Y, s ∈ S ∧ π' k s = π' k y) :
T ⊆ closure SClosure approximation can be checked on any cofinal refinement of quotient kernels.
Show proof
subset_closure_of_identityQuotientKernel_approximation
(Y := Y) (S := S) (T := T) π'
(HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_ker_le
(Y := Y) (π := π) (π' := π') hbasis hcofinal)
happroxProof. 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. 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. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem subset_closure_of_identityQuotientKernel_stage_exact_reindex
[IsTopologicalGroup Y]
{S T : Set Y}
(hbasis : HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π)
(hcofinal : ∀ j : J, ∃ k : K, (π' k).ker ≤ (π j).ker)
(Sstage Tstage : ∀ k : K, Set (Q' k))
(hTstage : ∀ y : Y, y ∈ T → ∀ k : K, π' k y ∈ Tstage k)
(hstage_exact : ∀ k : K, Tstage k ⊆ Sstage k)
(hlift_stage : ∀ k : K, ∀ q : Q' k, q ∈ Sstage k →
∃ s : Y, s ∈ S ∧ π' k s = q) :
T ⊆ closure SThe finite-stage closure approximation can be checked on a cofinal refined quotient family.
Show proof
subset_closure_of_identityQuotientKernel_stage_exact
(Y := Y) (S := S) (T := T) π'
(HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_ker_le
(Y := Y) (π := π) (π' := π') hbasis hcofinal)
Sstage Tstage hTstage hstage_exact hlift_stageProof. 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. 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. 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.
□