NYLL
Module

Universe.lean

Nyll.ProCGroups.FreeProC.Universe
12 declarations indexed from sourceView source ↗

Module documentation

Universe-polymorphic targets for free pro-\(C\) groups

The original IsFreeProCGroup API keeps the source, free group, finite-group class, and target in one universe. This module factors the universal property for one fixed target into HasFreeLiftTo, then supplies an explicit extension whose target lives in an independent universe. Cross-universe membership is expressed by FiniteGroupClass.MemAcrossUniverses, so no ULift appears in the public universal property.

An ordinary IsFreeProCGroup yields this extension only in its native target universe. There is deliberately no theorem promoting it to every target universe: such a promotion is not a consequence of the same-universe universal property.

Imports1
Imported by1

Declarations

def

HasFreeLiftTo

L39 ↗
ProCGroups.FreeProC.HasFreeLiftTo
Documentation

The universal extension property from F to one fixed pro-\(C\) target G.

Keeping this target-specific property separate lets constructions prove exactly the cross-universe lifting statement they support, without claiming a nonexistent automatic promotion from the native universal property.

Source context 6 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v
open ProCGroups
variable {C : FiniteGroupClass.{u}}
Lean source · statement
def HasFreeLiftTo
    {X : Type u} [TopologicalSpace X]
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    (ι : X → F)
    (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] : Prop
def

lift

L58 ↗
ProCGroups.FreeProC.HasFreeLiftTo.lift
Documentation

Extend a continuous generator map to the fixed target.

Source context 12 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v
open ProCGroups
variable {C : FiniteGroupClass.{u}}
namespace HasFreeLiftTo
variable {X : Type u} [TopologicalSpace X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {ι : X → F}
variable {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
def lift (h : HasFreeLiftTo (C := C) ι G)
    (hG : ProC.HasOpenNormalBasisInClassAcrossUniverses C G)
    (φ : X → G) (hφ : Continuous φ) : F →* G
theorem

lift_spec

L64 ↗
ProCGroups.FreeProC.HasFreeLiftTo.lift_spec
Documentation

The fixed-target lift is continuous and has the prescribed generator values.

Source context 12 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v
open ProCGroups
variable {C : FiniteGroupClass.{u}}
namespace HasFreeLiftTo
variable {X : Type u} [TopologicalSpace X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {ι : X → F}
variable {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
theorem lift_spec (h : HasFreeLiftTo (C := C) ι G)
    (hG : ProC.HasOpenNormalBasisInClassAcrossUniverses C G)
    (φ : X → G) (hφ : Continuous φ) :
    Continuous (h.lift hG φ hφ) ∧ ∀ x, h.lift hG φ hφ (ι x) = φ x
theorem

lift_unique

L71 ↗
ProCGroups.FreeProC.HasFreeLiftTo.lift_unique
Documentation

The fixed-target lift is unique among continuous homomorphisms with the prescribed values.

Source context 12 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v
open ProCGroups
variable {C : FiniteGroupClass.{u}}
namespace HasFreeLiftTo
variable {X : Type u} [TopologicalSpace X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {ι : X → F}
variable {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
theorem lift_unique (h : HasFreeLiftTo (C := C) ι G)
    (hG : ProC.HasOpenNormalBasisInClassAcrossUniverses C G)
    (φ : X → G) (hφ : Continuous φ)
    {f : F →* G} (hf : Continuous f) (hfac : ∀ x, f (ι x) = φ x) :
    f = h.lift hG φ hφ
def

liftHom

L79 ↗
ProCGroups.FreeProC.HasFreeLiftTo.liftHom
Documentation

Bundle the fixed-target lift as a continuous monoid homomorphism.

Source context 12 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v
open ProCGroups
variable {C : FiniteGroupClass.{u}}
namespace HasFreeLiftTo
variable {X : Type u} [TopologicalSpace X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {ι : X → F}
variable {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · full declaration
def liftHom (h : HasFreeLiftTo (C := C) ι G)
    (hG : ProC.HasOpenNormalBasisInClassAcrossUniverses C G)
    (φ : X → G) (hφ : Continuous φ) : F →ₜ* G where
  toMonoidHom := h.lift hG φ hφ
  continuous_toFun := (h.lift_spec hG φ hφ).1
structure

IsFreeProCGroupForTargetUniverse

L92 ↗
ProCGroups.FreeProC.IsFreeProCGroupForTargetUniverse
Documentation

The free pro-\(C\) universal property for targets in an explicitly independent universe.

Lean cannot quantify over universe levels inside a proposition, so the target universe v is a universe parameter of this structure. The native universal property is retained as a parent, so this stronger witness is directly usable anywhere an IsFreeProCGroup is expected.

Source context 6 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v
open ProCGroups
variable {C : FiniteGroupClass.{u}}
Lean source · full declaration
structure IsFreeProCGroupForTargetUniverse
    {X : Type u} [TopologicalSpace X]
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    (ι : X → F) : Prop extends IsFreeProCGroup (C := C) ι where
  /--
  For every pro-`C` target in universe `v`, continuous maps from `X` extend uniquely to
  continuous homomorphisms from `F`.
  -/
  hasFreeLiftTo :
    ∀ {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
      [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G],
      HasFreeLiftTo (C := C) ι G
def

lift

L115 ↗
ProCGroups.FreeProC.IsFreeProCGroupForTargetUniverse.lift
Documentation

Extend a continuous generator map to a homomorphism into a target in the chosen target universe.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v
open ProCGroups
variable {C : FiniteGroupClass.{u}}
namespace IsFreeProCGroupForTargetUniverse
variable {X : Type u} [TopologicalSpace X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}
Lean source · statement
def lift (hι : IsFreeProCGroupForTargetUniverse.{u, v} (C := C) ι)
    {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : ProC.HasOpenNormalBasisInClassAcrossUniverses C G)
    (φ : X → G) (hφ : Continuous φ) : F →* G
theorem

lift_spec

L123 ↗
ProCGroups.FreeProC.IsFreeProCGroupForTargetUniverse.lift_spec
Documentation

The cross-universe lift is continuous and has the prescribed generator values.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v
open ProCGroups
variable {C : FiniteGroupClass.{u}}
namespace IsFreeProCGroupForTargetUniverse
variable {X : Type u} [TopologicalSpace X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}
Lean source · statement
theorem lift_spec (hι : IsFreeProCGroupForTargetUniverse.{u, v} (C := C) ι)
    {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : ProC.HasOpenNormalBasisInClassAcrossUniverses C G)
    (φ : X → G) (hφ : Continuous φ) :
    Continuous (hι.lift hG φ hφ) ∧
      ∀ x, hι.lift hG φ hφ (ι x) = φ x
theorem

lift_unique

L133 ↗
ProCGroups.FreeProC.IsFreeProCGroupForTargetUniverse.lift_unique
Documentation

The cross-universe lift is unique among continuous homomorphisms with the prescribed values.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v
open ProCGroups
variable {C : FiniteGroupClass.{u}}
namespace IsFreeProCGroupForTargetUniverse
variable {X : Type u} [TopologicalSpace X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}
Lean source · statement
theorem lift_unique (hι : IsFreeProCGroupForTargetUniverse.{u, v} (C := C) ι)
    {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : ProC.HasOpenNormalBasisInClassAcrossUniverses C G)
    (φ : X → G) (hφ : Continuous φ)
    {f : F →* G} (hf : Continuous f) (hfac : ∀ x, f (ι x) = φ x) :
    f = hι.lift hG φ hφ
def

liftHom

L143 ↗
ProCGroups.FreeProC.IsFreeProCGroupForTargetUniverse.liftHom
Documentation

Bundle the cross-universe lift as a continuous monoid homomorphism.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v
open ProCGroups
variable {C : FiniteGroupClass.{u}}
namespace IsFreeProCGroupForTargetUniverse
variable {X : Type u} [TopologicalSpace X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}
Lean source · full declaration
def liftHom (hι : IsFreeProCGroupForTargetUniverse.{u, v} (C := C) ι)
    {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : ProC.HasOpenNormalBasisInClassAcrossUniverses C G)
    (φ : X → G) (hφ : Continuous φ) : F →ₜ* G where
  toMonoidHom := hι.lift hG φ hφ
  continuous_toFun := (hι.lift_spec hG φ hφ).1
theorem

hasFreeLiftTo

L161 ↗
ProCGroups.FreeProC.IsFreeProCGroup.hasFreeLiftTo
Documentation

The ordinary universal property, viewed as a fixed-target property in its native universe.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v
open ProCGroups
variable {C : FiniteGroupClass.{u}}
namespace IsFreeProCGroup
variable {X : Type u} [TopologicalSpace X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}
Lean source · statement
theorem hasFreeLiftTo (hι : IsFreeProCGroup (C := C) ι)
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] :
    HasFreeLiftTo (C := C) ι G
theorem

toForTargetUniverse

L171 ↗
ProCGroups.FreeProC.IsFreeProCGroup.toForTargetUniverse
Documentation

In the native target universe, the original property yields the explicit target-universe property.

Source context 11 commands

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

open Set
open scoped Topology
namespace ProCGroups.FreeProC
universe u v
open ProCGroups
variable {C : FiniteGroupClass.{u}}
namespace IsFreeProCGroup
variable {X : Type u} [TopologicalSpace X]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F}
Lean source · full declaration
theorem toForTargetUniverse (hι : IsFreeProCGroup (C := C) ι) :
    IsFreeProCGroupForTargetUniverse.{u, u} (C := C) ι where
  toIsFreeProCGroup := hι
  hasFreeLiftTo := hι.hasFreeLiftTo

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