Module

FiniteStageFactorization.lean

Nyll.ProCGroups.InverseSystems.FiniteStageFactorization

9 declarations indexed from sourceView source ↗

Module documentation

Factorization through finite stages

Products are presented as inverse limits of their finite subproducts. The main factorization results show that continuous maps from a compact inverse limit to a finite discrete target depend on one stage; specialized versions produce factorizations by group homomorphisms and additive monoid homomorphisms.

Imports1

Nyll.ProCGroups.InverseSystems.ProfiniteSpace

Imported by5

def

additiveMultiplicativeHomeomorph

L32 ↗

ProCGroups.InverseSystems.additiveMultiplicativeHomeomorph

Documentation

The additive-multiplicative homeomorphism is compatible with the profinite topology and is determined by finite-quotient data.

Source context 5 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
attribute [local instance] instAddCommGroupAddInverseLimit
universe u v w

Lean source · full declaration

def additiveMultiplicativeHomeomorph (A : Type*) [TopologicalSpace A] :
    A ≃ₜ Multiplicative A where
  toEquiv := Multiplicative.ofAdd
  continuous_toFun := continuous_id
  continuous_invFun := continuous_id

def

finiteSubsetProductSystem

L41 ↗

ProCGroups.InverseSystems.finiteSubsetProductSystem

Documentation

The inverse system whose stage at \(F\) is the finite subproduct over the finite subset \(F\).

Source context 5 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
attribute [local instance] instAddCommGroupAddInverseLimit
universe u v w

Lean source · full declaration

def finiteSubsetProductSystem {α : Type u} (X : α → Type v)
    [∀ a, TopologicalSpace (X a)] : InverseSystem.{u, max u v} (I := Finset α) where
  X := fun F => ∀ a : F, X a.1
  topologicalSpace := fun _ => inferInstance
  map := fun {F G} hFG x a => x ⟨a.1, hFG a.2⟩
  continuous_map := fun {F G} hFG => by
    exact continuous_pi fun a => continuous_apply (⟨a.1, hFG a.2⟩ : G)
  map_id := fun F => by
    funext x a
    rfl
  map_comp := fun {F G H} hFG hGH => by
    funext x a
    rfl

def

homeomorph_inverseLimit_finiteSubsetProductSystem

L56 ↗

ProCGroups.InverseSystems.homeomorph_inverseLimit_finiteSubsetProductSystem

Documentation

An arbitrary product is homeomorphic to the inverse limit of its finite subproducts.

Source context 5 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
attribute [local instance] instAddCommGroupAddInverseLimit
universe u v w

Lean source · statement

def homeomorph_inverseLimit_finiteSubsetProductSystem {α : Type u} (X : α → Type v)
    [∀ a, TopologicalSpace (X a)] :
    (∀ a, X a) ≃ₜ (finiteSubsetProductSystem X).inverseLimit

theorem

factors_through_projection_finite

L111 ↗

ProCGroups.InverseSystems.InverseSystem.factors_through_projection_finite

Documentation

A continuous map from a profinite inverse limit to a finite discrete space factors through one projection.

Source context 5 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
attribute [local instance] instAddCommGroupAddInverseLimit
universe u v w

Lean source · statement

theorem InverseSystem.factors_through_projection_finite
    {I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]
    [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
    [∀ i, TotallyDisconnectedSpace (S.X i)] (hdir : Directed (· ≤ ·) (id : I → I))
    {Y : Type w} [TopologicalSpace Y] [Finite Y] [Nonempty Y] [DiscreteTopology Y]
    (ρ : S.inverseLimit → Y) (hρ : Continuous ρ) :
    ∃ k : I, ∃ ρ' : S.X k → Y, Continuous ρ' ∧ ρ = ρ' ∘ S.projection k

instance

finiteSubsetProductSystem_instGroup

L273 ↗

ProCGroups.InverseSystems.finiteSubsetProductSystem_instGroup

Documentation

Finite-subset product stages inherit their product group structures.

Source context 7 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
attribute [local instance] instAddCommGroupAddInverseLimit
universe u v w
section
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))

Lean source · statement

instance finiteSubsetProductSystem_instGroup {α : Type u} (X : α → Type v)
    [∀ a, TopologicalSpace (X a)] [∀ a, Group (X a)] :
    ∀ s, Group ((finiteSubsetProductSystem X).X s)

instance

finiteSubsetProductSystem_instIsTopologicalGroup

L282 ↗

ProCGroups.InverseSystems.finiteSubsetProductSystem_instIsTopologicalGroup

Documentation

Finite-subset product stages inherit their product topological group structures.

Source context 7 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
attribute [local instance] instAddCommGroupAddInverseLimit
universe u v w
section
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))

Lean source · statement

instance finiteSubsetProductSystem_instIsTopologicalGroup {α : Type u} (X : α → Type v)
    [∀ a, TopologicalSpace (X a)] [∀ a, Group (X a)] [∀ a, IsTopologicalGroup (X a)] :
    ∀ s, IsTopologicalGroup ((finiteSubsetProductSystem X).X s)

instance

finiteSubsetProductSystem_instIsGroupSystem

L291 ↗

ProCGroups.InverseSystems.finiteSubsetProductSystem_instIsGroupSystem

Documentation

The finite-subset product system is a group-valued inverse system.

Source context 7 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
attribute [local instance] instAddCommGroupAddInverseLimit
universe u v w
section
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))

Lean source · full declaration

instance finiteSubsetProductSystem_instIsGroupSystem {α : Type u} (X : α → Type v)
    [∀ a, TopologicalSpace (X a)] [∀ a, Group (X a)] :
    IsGroupSystem (finiteSubsetProductSystem X) where
  map_one := by
    intro i j hij
    funext a
    change (1 : X a.1) = 1
    rfl
  map_mul := by
    intro i j hij x y
    funext a
    change
      x ⟨a.1, hij a.2⟩ * y ⟨a.1, hij a.2⟩ =
        x ⟨a.1, hij a.2⟩ * y ⟨a.1, hij a.2⟩
    rfl
  map_inv := by
    intro i j hij x
    funext a
    change (x ⟨a.1, hij a.2⟩)⁻¹ = (x ⟨a.1, hij a.2⟩)⁻¹
    rfl

theorem

factors_through_projection_finite_group_hom

L316 ↗

ProCGroups.InverseSystems.InverseSystem.factors_through_projection_finite_group_hom

Documentation

A continuous homomorphism from an inverse limit of profinite groups to a finite discrete group factors through one of the projections.

Source context 7 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
attribute [local instance] instAddCommGroupAddInverseLimit
universe u v w
section
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))

Lean source · statement

theorem InverseSystem.factors_through_projection_finite_group_hom [Nonempty I]
    [∀ i, Group (S.X i)] [IsGroupSystem S] [∀ i, IsTopologicalGroup (S.X i)]
    [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
    [∀ i, TotallyDisconnectedSpace (S.X i)]
    (hdir : Directed (· ≤ ·) (id : I → I))
    {H : Type w} [Group H] [TopologicalSpace H] [Finite H] [DiscreteTopology H]
    (β : S.inverseLimit →* H) (_hβ : Continuous β) :
    ∃ k : I, ∃ βk : S.X k →* H, Continuous βk ∧ β = βk ∘ S.projection k

theorem

factors_through_projection_finite_addMonoidHom

L604 ↗

ProCGroups.InverseSystems.InverseSystem.factors_through_projection_finite_addMonoidHom

Documentation

A continuous additive homomorphism from an inverse limit of profinite additive groups to a finite discrete additive group factors through one finite stage.

Source context 7 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
attribute [local instance] instAddCommGroupAddInverseLimit
universe u v w
section
variable {I : Type u} [Preorder I] (S : InverseSystem (I := I))

Lean source · statement

theorem InverseSystem.factors_through_projection_finite_addMonoidHom [Nonempty I]
    [∀ i, AddCommGroup (S.X i)] [IsAddGroupSystem S] [∀ i, IsTopologicalAddGroup (S.X i)]
    [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
    [∀ i, TotallyDisconnectedSpace (S.X i)]
    (hdir : Directed (· ≤ ·) (id : I → I))
    {H : Type w} [AddCommGroup H] [TopologicalSpace H] [Finite H] [DiscreteTopology H]
    (β : S.inverseLimit →+ H) (hβ : Continuous β) :
    ∃ k : I, ∃ βk : S.X k →+ H, Continuous βk ∧ β = βk ∘ S.projection k

Module documentation

Factorization through finite stages

Declarations