Yamaguchi Lean 4 Library
ProCGroups.CompletedGroupAlgebra.UniversalProperty.Basic
ProCGroups/CompletedGroupAlgebra/UniversalProperty/Basic

ProCGroups.CompletedGroupAlgebra.UniversalProperty.Basic

35 Theorems | 15 Definitions | 2 Structures

This module packages canonical completed-group-algebra models by their finite-stage cone and inverse-limit universal property, derives comparison equivalences, and develops the continuous group-like map and its spanning properties.

imports
Imported by

Declarations

Structure CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel 
structure CanonicalCompletedGroupAlgebraModel
    (R : ProfiniteCommRing.{u}) (G : ProfiniteGrp.{v}) (RG : ProfiniteRing.{w})
    (algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG) where
  /-- The projection from the candidate model to each finite group-algebra stage. -/
  stageProjection : ∀ U : CompletedGroupAlgebraIndex G,
    RG →+* CompletedGroupAlgebraStage R G U
  /-- Each stage projection agrees with the canonical stage map on the algebraic source. -/
  stageProjection_comp_algebraicMap : ∀ U : CompletedGroupAlgebraIndex G,
    (stageProjection U).comp algebraicMap = completedGroupAlgebraNaturalSourceStageMap R G U
  /-- The stage projections exhibit the candidate carrier as the inverse limit. -/
  isInverseLimit :
    (completedGroupAlgebraSystem R G).IsInverseLimit
      (fun U x => stageProjection U x)

Certificate that a profinite ring realizes the inverse limit of the finite group algebras R[G/U] for bundled profinite coefficients and group.

The data are the bundled finite-stage ring homomorphisms, their compatibility with the specified algebraic map, and the inverse-limit universal property. Continuity and transition compatibility of the projections are contained in isInverseLimit. In particular, no comparison with the canonical carrier is assumed: the comparison homeomorphism and ring equivalence below are derived from the universal property. Profiniteness is inherited from the three bundled objects rather than repeated as certificate fields.

Theorem CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.stageProjection_continuous 
theorem stageProjection_continuous
    (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap)
    (U : CompletedGroupAlgebraIndex G) :
    letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
      (completedGroupAlgebraSystem R G).topologicalSpace U
    Continuous (h.stageProjection U)

Each model projection is continuous, as a consequence of the inverse-limit witness.

Show Lean proof
Theorem CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.stageProjection_compatible 
theorem stageProjection_compatible
    (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap)
    {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    (completedGroupAlgebraTransition R G hUV).comp (h.stageProjection V) =
      h.stageProjection U

Model projections commute with finite-stage transition ring homomorphisms.

Show Lean proof
Definition CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.comparisonHomeomorph 
noncomputable def comparisonHomeomorph
    (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap) :
    RG ≃ₜ CompletedGroupAlgebraCarrier R G :=
  h.isInverseLimit.homeomorphToInverseLimit

The comparison homeomorphism with the concrete inverse-limit carrier, derived solely from the two inverse-limit universal properties.

Theorem CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.completedGroupAlgebraProjection_comparisonHomeomorph 
@[simp]
theorem completedGroupAlgebraProjection_comparisonHomeomorph
    (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap)
    (U : CompletedGroupAlgebraIndex G) (x : RG) :
    completedGroupAlgebraProjection R G U (h.comparisonHomeomorph x) =
      h.stageProjection U x

The derived comparison is characterized by every finite-stage projection.

Show Lean proof
Definition CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.comparisonRingEquiv 
noncomputable def comparisonRingEquiv
    (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap) :
    RG ≃+* CompletedGroupAlgebraCarrier R G where
  toEquiv := h.comparisonHomeomorph.toEquiv
  map_add' x y := by
    apply completedGroupAlgebra_ext (R := R) (G := G)
    intro U
    change completedGroupAlgebraProjection R G U (h.comparisonHomeomorph (x + y)) =
      completedGroupAlgebraProjection R G U
        (h.comparisonHomeomorph x + h.comparisonHomeomorph y)
    calc
      completedGroupAlgebraProjection R G U (h.comparisonHomeomorph (x + y)) =
          h.stageProjection U (x + y) :=
        h.completedGroupAlgebraProjection_comparisonHomeomorph U (x + y)
      _ = h.stageProjection U x + h.stageProjection U y := map_add _ x y
      _ = completedGroupAlgebraProjection R G U (h.comparisonHomeomorph x) +
          completedGroupAlgebraProjection R G U (h.comparisonHomeomorph y) :=
        congrArg₂ (· + ·)
          (h.completedGroupAlgebraProjection_comparisonHomeomorph U x).symm
          (h.completedGroupAlgebraProjection_comparisonHomeomorph U y).symm
      _ = completedGroupAlgebraProjection R G U
          (h.comparisonHomeomorph x + h.comparisonHomeomorph y) :=
        (map_add (completedGroupAlgebraProjection R G U) _ _).symm
  map_mul' x y := by
    apply completedGroupAlgebra_ext (R := R) (G := G)
    intro U
    change completedGroupAlgebraProjection R G U (h.comparisonHomeomorph (x * y)) =
      completedGroupAlgebraProjection R G U
        (h.comparisonHomeomorph x * h.comparisonHomeomorph y)
    calc
      completedGroupAlgebraProjection R G U (h.comparisonHomeomorph (x * y)) =
          h.stageProjection U (x * y) :=
        h.completedGroupAlgebraProjection_comparisonHomeomorph U (x * y)
      _ = h.stageProjection U x * h.stageProjection U y := map_mul _ x y
      _ = completedGroupAlgebraProjection R G U (h.comparisonHomeomorph x) *
          completedGroupAlgebraProjection R G U (h.comparisonHomeomorph y) :=
        congrArg₂ (· * ·)
          (h.completedGroupAlgebraProjection_comparisonHomeomorph U x).symm
          (h.completedGroupAlgebraProjection_comparisonHomeomorph U y).symm
      _ = completedGroupAlgebraProjection R G U
          (h.comparisonHomeomorph x * h.comparisonHomeomorph y) :=
        (map_mul (completedGroupAlgebraProjection R G U) _ _).symm

The comparison homeomorphism preserves the ring operations because all model projections are ring homomorphisms.

Theorem CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.completedGroupAlgebraProjection_comparisonRingEquiv 
@[simp]
theorem completedGroupAlgebraProjection_comparisonRingEquiv
    (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap)
    (U : CompletedGroupAlgebraIndex G) (x : RG) :
    completedGroupAlgebraProjection R G U (h.comparisonRingEquiv x) =
      h.stageProjection U x

Ring-equivalence form of the finite-stage characterization.

Show Lean proof
Theorem CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.comparisonRingEquiv_continuous 
theorem comparisonRingEquiv_continuous
    (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap) :
    Continuous h.comparisonRingEquiv

The derived comparison ring equivalence is continuous.

Show Lean proof
Theorem CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.comparisonRingEquiv_symm_continuous 
theorem comparisonRingEquiv_symm_continuous
    (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap) :
    Continuous h.comparisonRingEquiv.symm

The inverse of the derived comparison ring equivalence is continuous.

Show Lean proof
Theorem CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.comparisonRingEquiv_algebraicMap 
@[simp]
theorem comparisonRingEquiv_algebraicMap
    (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap)
    (x : CompletedGroupAlgebraNaturalSource R G) :
    h.comparisonRingEquiv (algebraicMap x) =
      toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G) x

The derived comparison extends the specified algebraic map.

Show Lean proof
Theorem CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.comparisonRingEquiv_comp_algebraicMap 
theorem comparisonRingEquiv_comp_algebraicMap
    (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap) :
    h.comparisonRingEquiv.toRingHom.comp algebraicMap =
      toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G)

Bundled ring-homomorphism form of algebraic-map compatibility.

Show Lean proof
Theorem CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.algebraicMap_eq_comparisonRingEquiv_symm_comp 
theorem algebraicMap_eq_comparisonRingEquiv_symm_comp
    (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap) :
    algebraicMap = h.comparisonRingEquiv.symm.toRingHom.comp
      (toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G))

The specified algebraic map is forced by the finite-stage cone: it is the canonical map followed by the inverse comparison equivalence.

Show Lean proof
Theorem CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.algebraicMap_continuous 
theorem algebraicMap_continuous
    (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap) :
    Continuous algebraicMap

Continuity of the specified algebraic map is derived from the inverse-limit comparison.

Show Lean proof
Theorem CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.algebraicMap_dense 
theorem algebraicMap_dense
    (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap) :
    DenseRange algebraicMap

Density of the specified algebraic map is likewise forced by the canonical inverse-limit model; it is not independent structure data.

Show Lean proof
Definition CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.modelToModelHomeomorph 
noncomputable def modelToModelHomeomorph
    (h₁ : CanonicalCompletedGroupAlgebraModel R G RG₁ algebraicMap₁)
    (h₂ : CanonicalCompletedGroupAlgebraModel R G RG₂ algebraicMap₂) :
    RG₁ ≃ₜ RG₂ :=
  h₁.comparisonHomeomorph.trans h₂.comparisonHomeomorph.symm

The canonical homeomorphism between two finite-stage inverse-limit models.

Definition CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.modelToModelRingEquiv 
noncomputable def modelToModelRingEquiv
    (h₁ : CanonicalCompletedGroupAlgebraModel R G RG₁ algebraicMap₁)
    (h₂ : CanonicalCompletedGroupAlgebraModel R G RG₂ algebraicMap₂) :
    RG₁ ≃+* RG₂ :=
  h₁.comparisonRingEquiv.trans h₂.comparisonRingEquiv.symm

The canonical ring equivalence between two finite-stage inverse-limit models.

Theorem CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.stageProjection_modelToModelRingEquiv 
@[simp]
theorem stageProjection_modelToModelRingEquiv
    (h₁ : CanonicalCompletedGroupAlgebraModel R G RG₁ algebraicMap₁)
    (h₂ : CanonicalCompletedGroupAlgebraModel R G RG₂ algebraicMap₂)
    (U : CompletedGroupAlgebraIndex G) (x : RG₁) :
    h₂.stageProjection U (h₁.modelToModelRingEquiv h₂ x) =
      h₁.stageProjection U x

The model-to-model equivalence commutes with every finite-stage projection.

Show Lean proof
Theorem CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.modelToModelRingEquiv_continuous 
theorem modelToModelRingEquiv_continuous
    (h₁ : CanonicalCompletedGroupAlgebraModel R G RG₁ algebraicMap₁)
    (h₂ : CanonicalCompletedGroupAlgebraModel R G RG₂ algebraicMap₂) :
    Continuous (h₁.modelToModelRingEquiv h₂)

The canonical model-to-model ring equivalence is continuous.

Show Lean proof
Theorem CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.modelToModelRingEquiv_symm_continuous 
theorem modelToModelRingEquiv_symm_continuous
    (h₁ : CanonicalCompletedGroupAlgebraModel R G RG₁ algebraicMap₁)
    (h₂ : CanonicalCompletedGroupAlgebraModel R G RG₂ algebraicMap₂) :
    Continuous (h₁.modelToModelRingEquiv h₂).symm

The inverse of the canonical model-to-model ring equivalence is continuous.

Show Lean proof
Theorem CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.modelToModelRingEquiv_algebraicMap 
@[simp]
theorem modelToModelRingEquiv_algebraicMap
    (h₁ : CanonicalCompletedGroupAlgebraModel R G RG₁ algebraicMap₁)
    (h₂ : CanonicalCompletedGroupAlgebraModel R G RG₂ algebraicMap₂)
    (x : CompletedGroupAlgebraNaturalSource R G) :
    h₁.modelToModelRingEquiv h₂ (algebraicMap₁ x) = algebraicMap₂ x

The canonical model-to-model equivalence carries one specified algebraic map to the other.

Show Lean proof
Theorem CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.modelToModelRingEquiv_comp_algebraicMap 
theorem modelToModelRingEquiv_comp_algebraicMap
    (h₁ : CanonicalCompletedGroupAlgebraModel R G RG₁ algebraicMap₁)
    (h₂ : CanonicalCompletedGroupAlgebraModel R G RG₂ algebraicMap₂) :
    (h₁.modelToModelRingEquiv h₂).toRingHom.comp algebraicMap₁ = algebraicMap₂

Bundled ring-homomorphism form of model-to-model algebraic-map compatibility.

Show Lean proof
Theorem CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.modelToModelRingEquiv_unique 
theorem modelToModelRingEquiv_unique
    (h₁ : CanonicalCompletedGroupAlgebraModel R G RG₁ algebraicMap₁)
    (h₂ : CanonicalCompletedGroupAlgebraModel R G RG₂ algebraicMap₂)
    (e : RG₁ ≃+* RG₂)
    (hstage : ∀ U : CompletedGroupAlgebraIndex G,
      (h₂.stageProjection U).comp e.toRingHom = h₁.stageProjection U) :
    e = h₁.modelToModelRingEquiv h₂

A ring equivalence commuting with all finite-stage projections is the canonical model-to-model equivalence. Joint injectivity of the canonical stage projections makes a separate continuity hypothesis unnecessary.

Show Lean proof
Structure CompletedGroupAlgebra.CompletedGroupAlgebraModel 
structure CompletedGroupAlgebraModel
    (R : ProfiniteCommRing.{u}) (G : ProfiniteGrp.{v}) where
  /-- The profinite ring underlying the completed group-algebra model. -/
  carrier : ProfiniteRing.{w}
  /-- The canonical map from the algebraic group algebra into the model. -/
  algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* carrier
  /-- The projection from the model to each finite group-algebra stage. -/
  stageProjection : ∀ U : CompletedGroupAlgebraIndex G,
    carrier →+* CompletedGroupAlgebraStage R G U
  /-- Each stage projection agrees with the canonical stage map on the algebraic source. -/
  stageProjection_comp_algebraicMap : ∀ U : CompletedGroupAlgebraIndex G,
    (stageProjection U).comp algebraicMap = completedGroupAlgebraNaturalSourceStageMap R G U
  /-- The stage projections exhibit the model carrier as the inverse limit. -/
  isInverseLimit :
    (completedGroupAlgebraSystem R G).IsInverseLimit
      (fun U x => stageProjection U x)

A completed group algebra model whose coefficient ring, profinite carrier, and group are genuine bundled objects.

The data fields contain the algebraic map and the finite-stage cone with its universal property. Continuity, density, and carrier profiniteness are theorems forced by comparison with the concrete inverse limit; they are not stored as independent witnesses. Likewise, all input profiniteness structure is inherited from the objects. CompletedGroupAlgebraModel.certificate reconstructs the finite-stage certificate when needed.

Definition CompletedGroupAlgebra.CompletedGroupAlgebraModel.certificate 
def certificate (M : CompletedGroupAlgebraModel R G) :
    CanonicalCompletedGroupAlgebraModel R G M.carrier M.algebraicMap where
  stageProjection := M.stageProjection
  stageProjection_comp_algebraicMap := M.stageProjection_comp_algebraicMap
  isInverseLimit := M.isInverseLimit

Expose the bundled model's finite-stage inverse-limit certificate.

Definition CompletedGroupAlgebra.CompletedGroupAlgebraModel.ofCertificate 
def ofCertificate (carrier : ProfiniteRing.{w})
    (algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* carrier)
    (h : CanonicalCompletedGroupAlgebraModel R G carrier algebraicMap) :
    CompletedGroupAlgebraModel R G where
  carrier := carrier
  algebraicMap := algebraicMap
  stageProjection := h.stageProjection
  stageProjection_comp_algebraicMap := h.stageProjection_comp_algebraicMap
  isInverseLimit := h.isInverseLimit

Package a finite-stage certificate as a completed-group-algebra model.

Theorem CompletedGroupAlgebra.CompletedGroupAlgebraModel.algebraicMap_continuous 
theorem algebraicMap_continuous (M : CompletedGroupAlgebraModel R G) :
    Continuous M.algebraicMap

The bundled model's specified algebraic map is continuous; this is derived, not stored.

Show Lean proof
Theorem CompletedGroupAlgebra.CompletedGroupAlgebraModel.algebraicMap_dense 
theorem algebraicMap_dense (M : CompletedGroupAlgebraModel R G) :
    DenseRange M.algebraicMap

The bundled model's specified algebraic map has dense range; this is derived, not stored.

Show Lean proof
Definition CompletedGroupAlgebra.CompletedGroupAlgebraModel.coefficientMap 
def coefficientMap (M : CompletedGroupAlgebraModel R G) : R →+* M.carrier :=
  M.algebraicMap.comp
    (completedGroupAlgebraNaturalSourceCoefficientRingHom (R := R) (G := G))

Restriction of the algebraic map to the coefficient ring.

Definition CompletedGroupAlgebra.CompletedGroupAlgebraModel.groupMap 
def groupMap (M : CompletedGroupAlgebraModel R G) : G →* M.carrier :=
  M.algebraicMap.toMonoidHom.comp
    (completedGroupAlgebraNaturalSourceGroupMonoidHom (R := R) (G := G))

Restriction of the algebraic map to group-like elements.

Definition CompletedGroupAlgebra.CompletedGroupAlgebraModel.groupUnitsMap 
def groupUnitsMap (M : CompletedGroupAlgebraModel R G) : G →* M.carrierˣ :=
  M.groupMap.toHomUnits

Group-like elements land in units; this is the object-level unit representation of a model.

Theorem CompletedGroupAlgebra.CompletedGroupAlgebraModel.groupUnitsMap_coe 
@[simp]
theorem groupUnitsMap_coe (M : CompletedGroupAlgebraModel R G) (g : G) :
    ((M.groupUnitsMap g : M.carrierˣ) : M.carrier) = M.groupMap g

Forgetting the unit structure from a model's group map recovers its underlying group-like element.

Show Lean proof
Definition CompletedGroupAlgebra.CompletedGroupAlgebraModel.comparisonRingEquiv 
noncomputable def comparisonRingEquiv (M : CompletedGroupAlgebraModel R G) :
    M.carrier ≃+* CompletedGroupAlgebraCarrier R G :=
  M.certificate.comparisonRingEquiv

The derived comparison with the concrete compatible-family model.

Definition CompletedGroupAlgebra.CompletedGroupAlgebraModel.comparisonHomeomorph 
noncomputable def comparisonHomeomorph (M : CompletedGroupAlgebraModel R G) :
    M.carrier ≃ₜ CompletedGroupAlgebraCarrier R G :=
  M.certificate.comparisonHomeomorph

The derived comparison is a homeomorphism.

Theorem CompletedGroupAlgebra.CompletedGroupAlgebraModel.completedGroupAlgebraProjection_comparisonRingEquiv 
@[simp]
theorem completedGroupAlgebraProjection_comparisonRingEquiv
    (M : CompletedGroupAlgebraModel R G) (U : CompletedGroupAlgebraIndex G) (x : M.carrier) :
    completedGroupAlgebraProjection R G U (M.comparisonRingEquiv x) =
      M.stageProjection U x

The bundled comparison is characterized by every finite-stage projection.

Show Lean proof
Theorem CompletedGroupAlgebra.CompletedGroupAlgebraModel.comparisonRingEquiv_algebraicMap 
@[simp]
theorem comparisonRingEquiv_algebraicMap (M : CompletedGroupAlgebraModel R G)
    (x : CompletedGroupAlgebraNaturalSource R G) :
    M.comparisonRingEquiv (M.algebraicMap x) =
      toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G) x

The bundled comparison extends the model's full algebraic map.

Show Lean proof
Theorem CompletedGroupAlgebra.CompletedGroupAlgebraModel.comparisonRingEquiv_coefficientMap 
@[simp]
theorem comparisonRingEquiv_coefficientMap (M : CompletedGroupAlgebraModel R G) (r : R) :
    M.comparisonRingEquiv (M.coefficientMap r) =
      algebraMap R (CompletedGroupAlgebraCarrier R G) r

The comparison therefore respects the coefficient-ring embedding.

Show Lean proof
Theorem CompletedGroupAlgebra.CompletedGroupAlgebraModel.comparisonRingEquiv_groupMap_source 
@[simp]
theorem comparisonRingEquiv_groupMap_source (M : CompletedGroupAlgebraModel R G) (g : G) :
    M.comparisonRingEquiv (M.groupMap g) =
      toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G)
        (completedGroupAlgebraNaturalSourceGroupMonoidHom (R := R) (G := G) g)

Source-wrapper form of compatibility with the group-like map. The normalized completedGroupAlgebraOf form is stated after that canonical map is introduced below.

Show Lean proof
Definition CompletedGroupAlgebra.CompletedGroupAlgebraModel.modelEquiv 
noncomputable def modelEquiv (M : CompletedGroupAlgebraModel.{u, v, w} R G)
    (N : CompletedGroupAlgebraModel.{u, v, z} R G) :
    M.carrier ≃+* N.carrier :=
  M.certificate.modelToModelRingEquiv N.certificate

Canonical equivalence between any two bundled models.

Theorem CompletedGroupAlgebra.CompletedGroupAlgebraModel.modelEquiv_algebraicMap 
@[simp]
theorem modelEquiv_algebraicMap (M : CompletedGroupAlgebraModel.{u, v, w} R G)
    (N : CompletedGroupAlgebraModel.{u, v, z} R G)
    (x : CompletedGroupAlgebraNaturalSource R G) :
    M.modelEquiv N (M.algebraicMap x) = N.algebraicMap x

The model equivalence carries the specified algebraic map to the specified algebraic map.

Show Lean proof
Theorem CompletedGroupAlgebra.CompletedGroupAlgebraModel.stageProjection_modelEquiv 
@[simp]
theorem stageProjection_modelEquiv (M : CompletedGroupAlgebraModel.{u, v, w} R G)
    (N : CompletedGroupAlgebraModel.{u, v, z} R G)
    (U : CompletedGroupAlgebraIndex G) (x : M.carrier) :
    N.stageProjection U (M.modelEquiv N x) = M.stageProjection U x

The canonical equivalence commutes with every finite-stage projection.

Show Lean proof
Theorem CompletedGroupAlgebra.CompletedGroupAlgebraModel.modelEquiv_coefficientMap 
@[simp]
theorem modelEquiv_coefficientMap (M : CompletedGroupAlgebraModel.{u, v, w} R G)
    (N : CompletedGroupAlgebraModel.{u, v, z} R G) (r : R) :
    M.modelEquiv N (M.coefficientMap r) = N.coefficientMap r

The canonical equivalence restricts to the identity on coefficient-ring data.

Show Lean proof
Theorem CompletedGroupAlgebra.CompletedGroupAlgebraModel.modelEquiv_groupMap 
@[simp]
theorem modelEquiv_groupMap (M : CompletedGroupAlgebraModel.{u, v, w} R G)
    (N : CompletedGroupAlgebraModel.{u, v, z} R G) (g : G) :
    M.modelEquiv N (M.groupMap g) = N.groupMap g

The canonical equivalence restricts to the identity on group-like data.

Show Lean proof
Theorem CompletedGroupAlgebra.CompletedGroupAlgebraModel.modelEquiv_continuous 
theorem modelEquiv_continuous (M : CompletedGroupAlgebraModel.{u, v, w} R G)
    (N : CompletedGroupAlgebraModel.{u, v, z} R G) :
    Continuous (M.modelEquiv N)

The canonical equivalence between bundled models is continuous.

Show Lean proof
Theorem CompletedGroupAlgebra.CompletedGroupAlgebraModel.modelEquiv_symm_continuous 
theorem modelEquiv_symm_continuous (M : CompletedGroupAlgebraModel.{u, v, w} R G)
    (N : CompletedGroupAlgebraModel.{u, v, z} R G) :
    Continuous (M.modelEquiv N).symm

Its inverse is continuous as well.

Show Lean proof
Theorem CompletedGroupAlgebra.CompletedGroupAlgebraModel.modelEquiv_unique 
theorem modelEquiv_unique (M : CompletedGroupAlgebraModel.{u, v, w} R G)
    (N : CompletedGroupAlgebraModel.{u, v, z} R G)
    (e : M.carrier ≃+* N.carrier)
    (hstage : ∀ U : CompletedGroupAlgebraIndex G,
      (N.stageProjection U).comp e.toRingHom = M.stageProjection U) :
    e = M.modelEquiv N

Public bundled uniqueness theorem: a ring equivalence commuting with all stage projections is the canonical model equivalence.

Show Lean proof
Definition CompletedGroupAlgebra.completedGroupAlgebraProfiniteRing 
noncomputable def completedGroupAlgebraProfiniteRing
    (R : ProfiniteCommRing.{u}) (G : ProfiniteGrp.{v}) : ProfiniteRing := by
  letI : CompactSpace (CompletedGroupAlgebraCarrier R G) :=
    completedGroupAlgebra_compactSpace (R := R) (G := G)
  letI : T2Space (CompletedGroupAlgebraCarrier R G) :=
    completedGroupAlgebra_t2Space (R := R) (G := G)
  letI : TotallyDisconnectedSpace (CompletedGroupAlgebraCarrier R G) :=
    completedGroupAlgebra_totallyDisconnectedSpace (R := R) (G := G)
  exact
    { toProfinite := Profinite.of (CompletedGroupAlgebraCarrier R G)
      ring := inferInstance
      isTopologicalRing := inferInstance }

The concrete inverse-limit carrier as a profinite ring object.

Definition CompletedGroupAlgebra.completedGroupAlgebraCanonicalModel 
noncomputable def completedGroupAlgebraCanonicalModel
    (R : ProfiniteCommRing.{u}) (G : ProfiniteGrp.{v}) :
    CanonicalCompletedGroupAlgebraModel R G (completedGroupAlgebraProfiniteRing R G)
      (toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G)) where
  stageProjection := completedGroupAlgebraProjection R G
  stageProjection_comp_algebraicMap := by
    intro U
    apply RingHom.ext
    intro x
    change completedGroupAlgebraProjection R G U
        (toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G) x) =
      completedGroupAlgebraNaturalSourceStageMap R G U x
    rw [completedGroupAlgebraNaturalSourceStageMap_apply]
    change completedGroupAlgebraProjection R G U
        (toCompletedGroupAlgebra R G x.toMonoidAlgebra) =
      completedGroupAlgebraStageMap R G U x.toMonoidAlgebra
    exact completedGroupAlgebraProjection_toCompletedGroupAlgebra
      (R := R) (G := G) U x.toMonoidAlgebra
  isInverseLimit := by
    change
      (completedGroupAlgebraSystem R G).IsInverseLimit
        (fun U x => (completedGroupAlgebraSystem R G).projection U x)
    exact (completedGroupAlgebraSystem R G).isInverseLimit_projection

The inverse-limit carrier with its canonical dense map is the canonical model.

Definition CompletedGroupAlgebra.completedGroupAlgebraModel 
noncomputable def completedGroupAlgebraModel
    (Λ : ProfiniteCommRing.{u}) (P : ProfiniteGrp.{v}) :
    CompletedGroupAlgebraModel Λ P :=
  CompletedGroupAlgebraModel.ofCertificate
    (completedGroupAlgebraProfiniteRing Λ P)
    (toCompletedGroupAlgebraNaturalSourceRingHom (R := Λ) (G := P))
    (completedGroupAlgebraCanonicalModel Λ P)

The concrete inverse limit packaged as the canonical bundled completed-group-algebra model.

This is the object-level source of truth: the coefficient ring and group enter as standard profinite bundles, so their compactness and separation witnesses are not repeated in the API.

Theorem CompletedGroupAlgebra.CompletedGroupAlgebraModel.comparisonRingEquiv_groupMap 
@[simp]
theorem comparisonRingEquiv_groupMap (M : CompletedGroupAlgebraModel R G) (g : G) :
    M.comparisonRingEquiv (M.groupMap g) = completedGroupAlgebraOf R G g

The model comparison sends its group-like map to the canonical completed group element.

Show Lean proof
Theorem CompletedGroupAlgebra.toCompletedGroupAlgebraRingHom_mem_span_completedGroupAlgebraOf 
theorem toCompletedGroupAlgebraRingHom_mem_span_completedGroupAlgebraOf
    (x : MonoidAlgebra R G) :
    toCompletedGroupAlgebraRingHom R G x ∈
      Submodule.span R (Set.range (completedGroupAlgebraOf R G))

The dense abstract group-algebra map lands in the span of the completed group-like elements.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraOf_dense_span 
theorem completedGroupAlgebraOf_dense_span :
    closure (Submodule.span R (Set.range (completedGroupAlgebraOf R G)) :
      Set (CompletedGroupAlgebraCarrier R G)) = Set.univ

The completed group-like elements have dense linear span in the completed group algebra.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraContinuousLinearMap_ext_of_basis 
theorem completedGroupAlgebraContinuousLinearMap_ext_of_basis
    {N : Type w} [AddCommGroup N] [TopologicalSpace N] [Module R N] [T2Space N]
    {F K : CompletedGroupAlgebraCarrier R G →L[R] N}
    (hbasis : ∀ g : G, F (completedGroupAlgebraOf R G g) =
      K (completedGroupAlgebraOf R G g)) :
    F = K

The uniqueness half of the universal property in Lemma 5.3.5(d): a continuous linear map out of \(\widehat{R[G]}\) is determined by its values on the completed group-like elements.

Show Lean proof