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

ProCGroups.FoxDifferential.Completed.FreeProC.CofinalQuotientKernelBasis

6 Theorems

The principal declarations in this module are:

  • HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_ker_le 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. - HasLeftQuotientKernelNeighbourhoodBasis.reindex_of_ker_le Reindex a left-neighborhood quotient-kernel basis along a cofinal refinement of kernels. Every kernel in the original family is required to contain a kernel from the refined family. - HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_factor A factorization of the refined quotient through an original quotient gives the required kernel inclusion for identity-neighborhood reindexing. - HasLeftQuotientKernelNeighbourhoodBasis.reindex_of_factor A factorization of each refined quotient through an original quotient gives the kernel inclusion needed to reindex a left-neighborhood quotient-kernel basis.
import
Imported by

Declarations

Theorem FoxDifferential.HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_ker_le 
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 Lean proof
Theorem FoxDifferential.HasLeftQuotientKernelNeighbourhoodBasis.reindex_of_ker_le 
theorem HasLeftQuotientKernelNeighbourhoodBasis.reindex_of_ker_le
    (hbasis : HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) π)
    (hcofinal : ∀ j : J, ∃ k : K, (π' k).ker ≤ (π j).ker) :
    HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) π'

Reindex a left-neighborhood quotient-kernel basis along a cofinal refinement of kernels. Every kernel in the original family is required to contain a kernel from the refined family.

Show Lean proof
Theorem FoxDifferential.HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_factor 
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 Lean proof
Theorem FoxDifferential.HasLeftQuotientKernelNeighbourhoodBasis.reindex_of_factor 
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 each refined quotient through an original quotient gives the kernel inclusion needed to reindex a left-neighborhood quotient-kernel basis.

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

Closure approximation can be checked on any cofinal refinement of quotient kernels.

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

The finite-stage closure approximation can be checked on a cofinal refined quotient family.

Show Lean proof