Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.FreeProC.QuotientKernelBasis
ProCGroups/FoxDifferential/Completed/FreeProC/QuotientKernelBasis

ProCGroups.FoxDifferential.Completed.FreeProC.QuotientKernelBasis

3 Theorems | 1 Definition

The principal declarations in this module are:

  • HasIdentityQuotientKernelNeighbourhoodBasis Quotient 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. - HasIdentityQuotientKernelNeighbourhoodBasis.to_left Identity-neighborhood quotient kernels give the left quotient-kernel basis. - subset_closure_of_identityQuotientKernel_approximation Closure criterion using identity-neighborhood quotient kernels directly. - subset_closure_of_identityQuotientKernel_stage_exact The closure criterion with identity-neighborhood quotient kernels can be checked at finite stages.
import
Imported by

Declarations

Definition FoxDifferential.HasIdentityQuotientKernelNeighbourhoodBasis 
def HasIdentityQuotientKernelNeighbourhoodBasis : Prop :=
  ∀ U : Set Y, IsOpen U → (1 : Y) ∈ U →
    ∃ j : J, ∀ z : Y, z ∈ (π j).ker → z ∈ U

Quotient 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 FoxDifferential.HasIdentityQuotientKernelNeighbourhoodBasis.to_left 
theorem HasIdentityQuotientKernelNeighbourhoodBasis.to_left
    [IsTopologicalGroup Y]
    (hbasis : HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π) :
    HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) π

Identity-neighborhood quotient kernels give the left quotient-kernel basis.

Show Lean proof
Theorem FoxDifferential.subset_closure_of_identityQuotientKernel_approximation 
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 S

Closure criterion using identity-neighborhood quotient kernels directly.

Show Lean proof
Theorem FoxDifferential.subset_closure_of_identityQuotientKernel_stage_exact 
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 S

The closure criterion with identity-neighborhood quotient kernels can be checked at finite stages.

Show Lean proof