ProCGroups.FreeProC.Universe

6 Theorems | 5 Definitions | 1 Structure

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.

import

ProCGroups.FreeProC.Basic

Imported by

ProCGroups.FreeProC

Definition ProCGroups.FreeProC.HasFreeLiftTo

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 :=
  ProC.HasOpenNormalBasisInClassAcrossUniverses C G →
    ∀ (φ : X → G), Continuous φ →
      ∃! f : F →* G, Continuous f ∧ ∀ x, f (ι x) = φ x

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.

Definition ProCGroups.FreeProC.HasFreeLiftTo.lift

noncomputable def lift (h : HasFreeLiftTo (C := C) ι G)
    (hG : ProC.HasOpenNormalBasisInClassAcrossUniverses C G)
    (φ : X → G) (hφ : Continuous φ) : F →* G :=
  Classical.choose (ExistsUnique.exists (h hG φ hφ))

Extend a continuous generator map to the fixed target.

Theorem ProCGroups.FreeProC.HasFreeLiftTo.lift_spec

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

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

Show Lean proof

Theorem ProCGroups.FreeProC.HasFreeLiftTo.lift_unique

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φ

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

Show Lean proof

Definition ProCGroups.FreeProC.HasFreeLiftTo.liftHom

noncomputable 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

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

Structure ProCGroups.FreeProC.IsFreeProCGroupForTargetUniverse

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

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.

Definition ProCGroups.FreeProC.IsFreeProCGroupForTargetUniverse.lift

noncomputable 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 :=
  (hι.hasFreeLiftTo (G := G)).lift hG φ hφ

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

Theorem ProCGroups.FreeProC.IsFreeProCGroupForTargetUniverse.lift_spec

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

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

Show Lean proof

Theorem ProCGroups.FreeProC.IsFreeProCGroupForTargetUniverse.lift_unique

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φ

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

Show Lean proof

Definition ProCGroups.FreeProC.IsFreeProCGroupForTargetUniverse.liftHom

noncomputable 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

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

Theorem ProCGroups.FreeProC.IsFreeProCGroup.hasFreeLiftTo

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

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

Show Lean proof

Theorem ProCGroups.FreeProC.IsFreeProCGroup.toForTargetUniverse

theorem toForTargetUniverse (hι : IsFreeProCGroup (C := C) ι) :
    IsFreeProCGroupForTargetUniverse.{u, u} (C := C) ι where
  toIsFreeProCGroup

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

Show Lean proof

ProCGroups.FreeProC.Universe

Declarations