Module

CofinalQuotientKernelBasis.lean

Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.CofinalQuotientKernelBasis

6 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — free pro-\(C\) — cofinal quotient kernel basis

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.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.QuotientKernelBasis

Imported by2

theorem

reindex_of_ker_le

L53 ↗

FoxDifferential.HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_ker_le

Documentation

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
universe u v w
section CofinalReindexing
variable {Y : Type u} [Group Y] [TopologicalSpace Y]
variable {J : Type v} {K : Type w}
variable {Q : J → Type*} [∀ j, Group (Q j)]
variable {Q' : K → Type*} [∀ k, Group (Q' k)]
variable (π : ∀ j : J, Y →* Q j)
variable (π' : ∀ k : K, Y →* Q' k)

Lean source · statement

theorem HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_ker_le
    (hbasis : HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π)
    (hcofinal : ∀ j : J, ∃ k : K, (π' k).ker ≤ (π j).ker) :
    HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π'

theorem

reindex_of_ker_le

L68 ↗

FoxDifferential.HasLeftQuotientKernelNeighbourhoodBasis.reindex_of_ker_le

Documentation

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.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
universe u v w
section CofinalReindexing
variable {Y : Type u} [Group Y] [TopologicalSpace Y]
variable {J : Type v} {K : Type w}
variable {Q : J → Type*} [∀ j, Group (Q j)]
variable {Q' : K → Type*} [∀ k, Group (Q' k)]
variable (π : ∀ j : J, Y →* Q j)
variable (π' : ∀ k : K, Y →* Q' k)

Lean source · statement

theorem HasLeftQuotientKernelNeighbourhoodBasis.reindex_of_ker_le
    (hbasis : HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) π)
    (hcofinal : ∀ j : J, ∃ k : K, (π' k).ker ≤ (π j).ker) :
    HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) π'

theorem

reindex_of_factor

L83 ↗

FoxDifferential.HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_factor

Documentation

A factorization of the refined quotient through an original quotient gives the required kernel inclusion for identity-neighborhood reindexing.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
universe u v w
section CofinalReindexing
variable {Y : Type u} [Group Y] [TopologicalSpace Y]
variable {J : Type v} {K : Type w}
variable {Q : J → Type*} [∀ j, Group (Q j)]
variable {Q' : K → Type*} [∀ k, Group (Q' k)]
variable (π : ∀ j : J, Y →* Q j)
variable (π' : ∀ k : K, Y →* Q' k)

Lean source · statement

theorem HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_factor
    (hbasis : HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π)
    (hrefine : ∀ j : J, ∃ k : K, ∃ τ : Q' k →* Q j, τ.comp (π' k) = π j) :
    HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π'

theorem

reindex_of_factor

L104 ↗

FoxDifferential.HasLeftQuotientKernelNeighbourhoodBasis.reindex_of_factor

Documentation

A factorization of each refined quotient through an original quotient gives the kernel inclusion needed to reindex a left-neighborhood quotient-kernel basis.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
universe u v w
section CofinalReindexing
variable {Y : Type u} [Group Y] [TopologicalSpace Y]
variable {J : Type v} {K : Type w}
variable {Q : J → Type*} [∀ j, Group (Q j)]
variable {Q' : K → Type*} [∀ k, Group (Q' k)]
variable (π : ∀ j : J, Y →* Q j)
variable (π' : ∀ k : K, Y →* Q' k)

Lean source · statement

theorem HasLeftQuotientKernelNeighbourhoodBasis.reindex_of_factor
    (hbasis : HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) π)
    (hrefine : ∀ j : J, ∃ k : K, ∃ τ : Q' k →* Q j, τ.comp (π' k) = π j) :
    HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) π'

theorem

subset_closure_of_identityQuotientKernel_approximation_reindex

L122 ↗

FoxDifferential.subset_closure_of_identityQuotientKernel_approximation_reindex

Documentation

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

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
universe u v w
section CofinalReindexing
variable {Y : Type u} [Group Y] [TopologicalSpace Y]
variable {J : Type v} {K : Type w}
variable {Q : J → Type*} [∀ j, Group (Q j)]
variable {Q' : K → Type*} [∀ k, Group (Q' k)]
variable (π : ∀ j : J, Y →* Q j)
variable (π' : ∀ k : K, Y →* Q' k)

Lean source · statement

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

theorem

subset_closure_of_identityQuotientKernel_stage_exact_reindex

L138 ↗

FoxDifferential.subset_closure_of_identityQuotientKernel_stage_exact_reindex

Documentation

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

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
universe u v w
section CofinalReindexing
variable {Y : Type u} [Group Y] [TopologicalSpace Y]
variable {J : Type v} {K : Type w}
variable {Q : J → Type*} [∀ j, Group (Q j)]
variable {Q' : K → Type*} [∀ k, Group (Q' k)]
variable (π : ∀ j : J, Y →* Q j)
variable (π' : ∀ k : K, Y →* Q' k)

Lean source · statement

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

Module documentation

Fox differential: completed — free pro-\(C\) — cofinal quotient kernel basis

Declarations

reindex_of_ker_le

reindex_of_ker_le

reindex_of_factor

reindex_of_factor

subset_closure_of_identityQuotientKernel_approximation_reindex

subset_closure_of_identityQuotientKernel_stage_exact_reindex