FoxDifferential.Completed.FreeProC.QuotientKernelBasis
def HasIdentityQuotientKernelNeighbourhoodBasis : Prop :=
∀ U : Set Y, IsOpen U → (1 : Y) ∈ U →
∃ j : J, ∀ z : Y, z ∈ (π j).ker → z ∈ UQuotient kernels form a neighborhood basis at the identity. For every open neighborhood of 1, some finite-stage kernel is contained in it. In a topological group this is the natural form obtained from finite quotient separation; it implies the left-coset basis used by subset_closure_of_quotientKernel_approximation.
theorem HasIdentityQuotientKernelNeighbourhoodBasis.to_left
[IsTopologicalGroup Y]
(hbasis : HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π) :
HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) πIdentity-neighborhood quotient kernels give the left quotient-kernel basis.
Show proof
by
intro y U hU hyU
let W : Set Y := {z : Y | y * z ∈ U}
have hWopen : IsOpen W := by
have hmul : Continuous fun z : Y => y * z :=
(continuous_const : Continuous fun _ : Y => y).mul continuous_id
exact hU.preimage hmul
have hWone : (1 : Y) ∈ W := by
simp only [Set.mem_setOf_eq, mul_one, hyU, W]
rcases hbasis W hWopen hWone with ⟨j, hj⟩
refine ⟨j, ?_⟩
intro z hz
exact hj z hzProof. 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
[IsTopologicalGroup Y]
{S T : Set Y}
(hbasis : HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π)
(happrox :
∀ y : Y, y ∈ T → ∀ j : J,
∃ s : Y, s ∈ S ∧ π j s = π j y) :
T ⊆ closure SClosure criterion using identity-neighborhood quotient kernels directly.
Show proof
subset_closure_of_quotientKernel_approximation
(Y := Y) (S := S) (T := T) π
(HasIdentityQuotientKernelNeighbourhoodBasis.to_left (Y := Y) (π := π) hbasis)
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
[IsTopologicalGroup Y]
{S T : Set Y}
(hbasis : HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π)
(Sstage Tstage : ∀ j : J, Set (Q j))
(hTstage : ∀ y : Y, y ∈ T → ∀ j : J, π j y ∈ Tstage j)
(hstage_exact : ∀ j : J, Tstage j ⊆ Sstage j)
(hlift_stage : ∀ j : J, ∀ q : Q j, q ∈ Sstage j →
∃ s : Y, s ∈ S ∧ π j s = q) :
T ⊆ closure SThe closure criterion with identity-neighborhood quotient kernels can be checked at finite stages.
Show proof
subset_closure_of_quotientKernel_stage_exact
(Y := Y) (S := S) (T := T) π
(HasIdentityQuotientKernelNeighbourhoodBasis.to_left (Y := Y) (π := π) hbasis)
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.
□