ModuleQuotientKernelBasis.lean
Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.QuotientKernelBasis
4 declarations indexed from sourceView source ↗ Module documentation
Fox differential: completed — free pro-\(C\) — quotient kernel basis
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.
Declarations
FoxDifferential.HasIdentityQuotientKernelNeighbourhoodBasis
DocumentationQuotient 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.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open scoped Topology
universe u v
section QuotientKernelIdentityBasis
variable {Y : Type u} [Group Y] [TopologicalSpace Y]
variable {J : Type v} {Q : J → Type*} [∀ j, Group (Q j)]
variable (π : ∀ j : J, Y →* Q j)
FoxDifferential.HasIdentityQuotientKernelNeighbourhoodBasis.to_left
DocumentationIdentity-neighborhood quotient kernels give the left quotient-kernel basis.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open scoped Topology
universe u v
section QuotientKernelIdentityBasis
variable {Y : Type u} [Group Y] [TopologicalSpace Y]
variable {J : Type v} {Q : J → Type*} [∀ j, Group (Q j)]
variable (π : ∀ j : J, Y →* Q j)
FoxDifferential.subset_closure_of_identityQuotientKernel_approximation
DocumentationClosure criterion using identity-neighborhood quotient kernels directly.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open scoped Topology
universe u v
section QuotientKernelIdentityBasis
variable {Y : Type u} [Group Y] [TopologicalSpace Y]
variable {J : Type v} {Q : J → Type*} [∀ j, Group (Q j)]
variable (π : ∀ j : J, Y →* Q j)
FoxDifferential.subset_closure_of_identityQuotientKernel_stage_exact
DocumentationThe closure criterion with identity-neighborhood quotient kernels can be checked at finite stages.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open scoped Topology
universe u v
section QuotientKernelIdentityBasis
variable {Y : Type u} [Group Y] [TopologicalSpace Y]
variable {J : Type v} {Q : J → Type*} [∀ j, Group (Q j)]
variable (π : ∀ j : J, Y →* Q j)