NYLL
Module

CofinalityAndDensity.lean

Nyll.ProCGroups.InverseSystems.CofinalityAndDensity
10 declarations indexed from sourceView source ↗

Module documentation

Cofinal reindexing, density, and projection neighborhoods

For inverse systems over directed preorders, this module controls neighborhoods by finitely many coordinates and studies the map induced by a morphism on limits. It proves density and surjectivity criteria, invariance of the limit under cofinal reindexing or restriction, and the projection-preimage basis for compact Hausdorff systems.

Imports1
Imported by8

Declarations

theorem

exists_projection_preimage_subset

L39 ↗
ProCGroups.InverseSystems.InverseSystem.exists_projection_preimage_subset
Documentation

Every open neighborhood in the inverse limit contains the inverse image of an open set along one projection.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))
Lean source · statement
theorem exists_projection_preimage_subset [Nonempty I]
    (hdir : Directed (· ≤ ·) (id : I → I)) {x : S.inverseLimit} {U : Set S.inverseLimit}
    (hU : IsOpen U) (hx : x ∈ U) :
    ∃ i, ∃ V : Set (S.X i), IsOpen V ∧ S.projection i x ∈ V ∧ S.projection i ⁻¹' V ⊆ U
theorem

denseRange_lift

L100 ↗
ProCGroups.InverseSystems.InverseSystem.denseRange_lift
Documentation

A compatible family of surjections over a nonempty directed index preorder induces a dense map to the inverse limit.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))
Lean source · statement
theorem denseRange_lift {X : Type w} [Nonempty I]
    (ρ : ∀ i, X → S.X i) (hρ : S.CompatibleMaps ρ)
    (hsurj : ∀ i, Function.Surjective (ρ i)) (hdir : Directed (· ≤ ·) (id : I → I)) :
    DenseRange (S.inverseLimitLift ρ hρ)
def

reindex

L115 ↗
ProCGroups.InverseSystems.InverseSystem.reindex
Documentation

Reindexing an inverse system along a monotone map.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))
Lean source · full declaration
def reindex {K : Type w} [Preorder K] (σ : K → I) (hσ : Monotone σ) :
    InverseSystem (I := K) where
  X := fun k => S.X (σ k)
  topologicalSpace := fun k => inferInstance
  map := fun {i j} hij => S.map (hσ hij)
  continuous_map := fun {i j} hij => S.continuous_map (hσ hij)
  map_id := fun k => by
    simpa using S.map_id (σ k)
  map_comp := fun {i j k} hij hjk => by
    simpa using S.map_comp (hσ hij) (hσ hjk)
def

restrict

L127 ↗
ProCGroups.InverseSystems.InverseSystem.restrict
Documentation

The inverse system obtained by restricting the index preorder to a subset.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))
Lean source · statement
def restrict (J : Set I) : InverseSystem (I := J)
def

homeomorph_reindex_cofinal

L131 ↗
ProCGroups.InverseSystems.InverseSystem.homeomorph_reindex_cofinal
Documentation

The inverse limit is unchanged after reindexing along a monotone cofinal map.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))
Lean source · statement
def homeomorph_reindex_cofinal {K : Type w} [Preorder K]
    (σ : K → I) (hσ : Monotone σ) (hdirK : Directed (· ≤ ·) (id : K → K))
    (hcofinal : ∀ i : I, ∃ k : K, i ≤ σ k) :
    S.inverseLimit ≃ₜ (S.reindex σ hσ).inverseLimit
theorem

π_comp_homeomorph_reindex_cofinal

L213 ↗
ProCGroups.InverseSystems.InverseSystem.π_comp_homeomorph_reindex_cofinal
Documentation

After cofinal reindexing, the projection to \(k\) composed with the reindexing homeomorphism is the original projection to \(\sigma k\).

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))
Lean source · statement
theorem π_comp_homeomorph_reindex_cofinal {K : Type w} [Preorder K]
    (σ : K → I) (hσ : Monotone σ) (hdirK : Directed (· ≤ ·) (id : K → K))
    (hcofinal : ∀ i : I, ∃ k : K, i ≤ σ k) (k : K) :
    (S.reindex σ hσ).projection k ∘ S.homeomorph_reindex_cofinal σ hσ hdirK hcofinal =
        S.projection (σ k)
def

homeomorph_restrict_cofinal

L234 ↗
ProCGroups.InverseSystems.InverseSystem.homeomorph_restrict_cofinal
Documentation

The cofinal reindexing homeomorphism is characterized by its projections.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))
Lean source · statement
def homeomorph_restrict_cofinal (J : Set I)
    (hdirJ : Directed (· ≤ ·) (id : J → J)) (hcofinal : ∀ i, ∃ j : J, i ≤ j.1) :
    S.inverseLimit ≃ₜ (S.restrict J).inverseLimit
theorem

π_comp_homeomorph_restrict_cofinal

L243 ↗
ProCGroups.InverseSystems.InverseSystem.π_comp_homeomorph_restrict_cofinal
Documentation

For a cofinal restriction, projecting to \(j\) after the restriction homeomorphism is the same as the original projection to the underlying index of \(j\).

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))
Lean source · statement
theorem π_comp_homeomorph_restrict_cofinal (J : Set I)
    (hdirJ : Directed (· ≤ ·) (id : J → J)) (hcofinal : ∀ i, ∃ j : J, i ≤ j.1) (j : J) :
    (S.restrict J).projection j ∘ S.homeomorph_restrict_cofinal J hdirJ hcofinal = S.projection
        j.1
theorem

surjective_π

L255 ↗
ProCGroups.InverseSystems.InverseSystem.surjective_π
Documentation

In a surjective inverse system of compact Hausdorff nonempty spaces, each projection from the inverse limit is surjective.

Source context 9 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
section
variable {I : Type u} [Preorder I]
attribute [instance] InverseSystem.topologicalSpace
namespace InverseSystem
variable (S : InverseSystem (I := I))
Lean source · statement
theorem surjective_π [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
    (hdir : Directed (· ≤ ·) (id : I → I))
    (hsurj : ∀ {i j : I} (hij : i ≤ j), Function.Surjective (S.map hij)) (j : I) :
    Function.Surjective (S.projection j)
theorem

isTopologicalBasis_projection_preimages

L335 ↗
ProCGroups.InverseSystems.InverseSystem.isTopologicalBasis_projection_preimages
Documentation

If each component has a chosen basis, then the inverse images of basis elements under the projection maps form a basis of the inverse limit.

Source context 4 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u v w
Lean source · statement
theorem InverseSystem.isTopologicalBasis_projection_preimages {I : Type u} [Preorder I]
    (S : InverseSystem (I := I)) [Nonempty I] (hdir : Directed (· ≤ ·) (id : I → I))
    (B : ∀ i, Set (Set (S.X i))) (hB : ∀ i, TopologicalSpace.IsTopologicalBasis (B i)) :
    TopologicalSpace.IsTopologicalBasis
      {W : Set S.inverseLimit | ∃ i, ∃ V ∈ B i, W = S.projection i ⁻¹' V}

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.