Yamaguchi Lean 4 Library
ProCGroups.FreeProC.Characterization.Quasifree
ProCGroups/FreeProC/Characterization/Quasifree

ProCGroups.FreeProC.Characterization.Quasifree

5 Definition

This module proves the universal-property part of the construction. It packages finite-stage data into completed maps and shows the required extension and uniqueness statements.

Open this file on GitHub
import
Imported by

Declarations

Definition ProCGroups.FreeProC.Characterization.HasGeneratingSetOfCardinality GitHub 
def HasGeneratingSetOfCardinality (G : Type u) [Group G] (κ : Cardinal) : Prop :=
  ∃ S : Set G, Subgroup.closure S = ⊤ ∧ Cardinal.mk S = κ

An abstract group has a generating set of cardinality \(\kappa\). This is not the right rank condition for quasifree profinite groups; use HasTopologicalGeneratingSetOfCardinality there.

Definition ProCGroups.FreeProC.Characterization.HasTopologicalGeneratingSetOfCardinality GitHub 
def HasTopologicalGeneratingSetOfCardinality
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (κ : Cardinal) : Prop :=
  ∃ S : Set G, Generation.TopologicallyGenerates (G := G) S ∧ Cardinal.mk S = κ

A topological group has a topological generating set of cardinality \(\kappa\).

Definition ProCGroups.FreeProC.Characterization.IsProjectiveProCGroup GitHub 
def IsProjectiveProCGroup (C : ProCGroups.FiniteGroupClass.{u})
    (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
  ProCGroups.ProC.IsProCGroup C G ∧
    ∀ {A B : Type u} [Group A] [Group B]
      [TopologicalSpace A] [TopologicalSpace B]
      [IsTopologicalGroup A] [IsTopologicalGroup B],
      ProCGroups.ProC.IsProCGroup C A → ProCGroups.ProC.IsProCGroup C B →
        (φ : G →ₜ* B) → (π : A →ₜ* B) → Function.Surjective π →
          ∃ lift : G →ₜ* A, π.comp lift = φ

A pro-\(C\) group is projective for finite \(C\)-embedding problems, expressed as the concrete lifting property used by the quasifree formulation.

Definition ProCGroups.FreeProC.Characterization.HasQuasifreeProperSolutionProperty GitHub 
def HasQuasifreeProperSolutionProperty
    (C : ProCGroups.FiniteGroupClass.{u})
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (κ : Cardinal) : Prop :=
  ∀ P : TopologicalEmbeddingProblem G,
    IsFiniteSplitCEmbeddingProblem C P → P.HasAtLeastProperSolutions κ

A group has the quasifree proper-solution property at rank \(\kappa\) for finite split \(C\)-embedding problems.

Definition ProCGroups.FreeProC.Characterization.IsQuasifreeOfRank GitHub 
def IsQuasifreeOfRank (C : ProCGroups.FiniteGroupClass.{u})
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (κ : Cardinal) : Prop :=
  ProCGroups.ProC.IsProCGroup C G ∧
    HasTopologicalGeneratingSetOfCardinality G κ ∧
      Cardinal.aleph0 ≤ κ ∧
        HasQuasifreeProperSolutionProperty C G κ

Quasifreeness at infinite rank \(\kappa\). The rank field is deliberately topological: in profinite contexts an abstract generating set is too weak and does not control the closed subgroup generated by the chosen family. The lifting field records the standard proper-solution condition for finite split embedding problems.