NYLL
Module

Basic.lean

Nyll.ProCGroups.CompletedGroupAlgebra.UniversalProperty.Basic
52 declarations indexed from sourceView source ↗

Module documentation

Completed Group Algebra / Universal Property / Basic

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.

Imports3
Imported by4

Declarations

structure

CanonicalCompletedGroupAlgebraModel

L44 ↗
CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel
Documentation

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.

Source context 10 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
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)
theorem

stageProjection_continuous

L65 ↗
CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.stageProjection_continuous
Documentation

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

Source context 14 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CanonicalCompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
variable {RG : ProfiniteRing.{w}}
variable {algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG}
Lean source · full declaration
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) := by
  let : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
    (completedGroupAlgebraSystem R G).topologicalSpace U
  exact h.isInverseLimit.continuous_proj U
theorem

stageProjection_compatible

L76 ↗
CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.stageProjection_compatible
Documentation

Model projections commute with finite-stage transition ring homomorphisms.

Source context 14 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CanonicalCompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
variable {RG : ProfiniteRing.{w}}
variable {algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG}
Lean source · statement
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
def

comparisonHomeomorph

L90 ↗
CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.comparisonHomeomorph
Documentation

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

Source context 14 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CanonicalCompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
variable {RG : ProfiniteRing.{w}}
variable {algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG}
Lean source · statement
def comparisonHomeomorph
    (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap) :
    RG ≃ₜ CompletedGroupAlgebraCarrier R G
theorem

completedGroupAlgebraProjection_comparisonHomeomorph

L97 ↗
CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.completedGroupAlgebraProjection_comparisonHomeomorph
Documentation

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

Source context 14 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CanonicalCompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
variable {RG : ProfiniteRing.{w}}
variable {algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG}
Lean source · statement
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
def

comparisonRingEquiv

L106 ↗
CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.comparisonRingEquiv
Documentation

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

Source context 14 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CanonicalCompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
variable {RG : ProfiniteRing.{w}}
variable {algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG}
Lean source · full declaration
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
theorem

completedGroupAlgebraProjection_comparisonRingEquiv

L151 ↗
CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.completedGroupAlgebraProjection_comparisonRingEquiv
Documentation

Ring-equivalence form of the finite-stage characterization.

Source context 14 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CanonicalCompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
variable {RG : ProfiniteRing.{w}}
variable {algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG}
Lean source · statement
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
theorem

comparisonRingEquiv_continuous

L159 ↗
CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.comparisonRingEquiv_continuous
Documentation

The derived comparison ring equivalence is continuous.

Source context 14 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CanonicalCompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
variable {RG : ProfiniteRing.{w}}
variable {algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG}
Lean source · statement
theorem comparisonRingEquiv_continuous
    (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap) :
    Continuous h.comparisonRingEquiv
theorem

comparisonRingEquiv_symm_continuous

L166 ↗
CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.comparisonRingEquiv_symm_continuous
Documentation

The inverse of the derived comparison ring equivalence is continuous.

Source context 14 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CanonicalCompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
variable {RG : ProfiniteRing.{w}}
variable {algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG}
Lean source · statement
theorem comparisonRingEquiv_symm_continuous
    (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap) :
    Continuous h.comparisonRingEquiv.symm
theorem

comparisonRingEquiv_algebraicMap

L174 ↗
CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.comparisonRingEquiv_algebraicMap
Documentation

The derived comparison extends the specified algebraic map.

Source context 14 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CanonicalCompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
variable {RG : ProfiniteRing.{w}}
variable {algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG}
Lean source · statement
theorem comparisonRingEquiv_algebraicMap
    (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap)
    (x : CompletedGroupAlgebraNaturalSource R G) :
    h.comparisonRingEquiv (algebraicMap x) =
      toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G) x
theorem

comparisonRingEquiv_comp_algebraicMap

L199 ↗
CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.comparisonRingEquiv_comp_algebraicMap
Documentation

Bundled ring-homomorphism form of algebraic-map compatibility.

Source context 14 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CanonicalCompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
variable {RG : ProfiniteRing.{w}}
variable {algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG}
Lean source · statement
theorem comparisonRingEquiv_comp_algebraicMap
    (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap) :
    h.comparisonRingEquiv.toRingHom.comp algebraicMap =
      toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G)
theorem

algebraicMap_eq_comparisonRingEquiv_symm_comp

L209 ↗
CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.algebraicMap_eq_comparisonRingEquiv_symm_comp
Documentation

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

Source context 14 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CanonicalCompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
variable {RG : ProfiniteRing.{w}}
variable {algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG}
Lean source · statement
theorem algebraicMap_eq_comparisonRingEquiv_symm_comp
    (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap) :
    algebraicMap = h.comparisonRingEquiv.symm.toRingHom.comp
      (toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G))
theorem

algebraicMap_continuous

L230 ↗
CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.algebraicMap_continuous
Documentation

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

Source context 14 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CanonicalCompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
variable {RG : ProfiniteRing.{w}}
variable {algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG}
Lean source · statement
theorem algebraicMap_continuous
    (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap) :
    Continuous algebraicMap
theorem

algebraicMap_dense

L239 ↗
CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.algebraicMap_dense
Documentation

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

Source context 14 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CanonicalCompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
variable {RG : ProfiniteRing.{w}}
variable {algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG}
Lean source · statement
theorem algebraicMap_dense
    (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap) :
    DenseRange algebraicMap
def

modelToModelHomeomorph

L253 ↗
CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.modelToModelHomeomorph
Documentation

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

Source context 17 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CanonicalCompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
variable {RG : ProfiniteRing.{w}}
variable {algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG}
variable {RG₁ : ProfiniteRing.{w}} {RG₂ : ProfiniteRing.{z}}
variable {algebraicMap₁ : CompletedGroupAlgebraNaturalSource R G →+* RG₁}
variable {algebraicMap₂ : CompletedGroupAlgebraNaturalSource R G →+* RG₂}
Lean source · statement
def modelToModelHomeomorph
    (h₁ : CanonicalCompletedGroupAlgebraModel R G RG₁ algebraicMap₁)
    (h₂ : CanonicalCompletedGroupAlgebraModel R G RG₂ algebraicMap₂) :
    RG₁ ≃ₜ RG₂
def

modelToModelRingEquiv

L260 ↗
CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.modelToModelRingEquiv
Documentation

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

Source context 17 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CanonicalCompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
variable {RG : ProfiniteRing.{w}}
variable {algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG}
variable {RG₁ : ProfiniteRing.{w}} {RG₂ : ProfiniteRing.{z}}
variable {algebraicMap₁ : CompletedGroupAlgebraNaturalSource R G →+* RG₁}
variable {algebraicMap₂ : CompletedGroupAlgebraNaturalSource R G →+* RG₂}
Lean source · statement
def modelToModelRingEquiv
    (h₁ : CanonicalCompletedGroupAlgebraModel R G RG₁ algebraicMap₁)
    (h₂ : CanonicalCompletedGroupAlgebraModel R G RG₂ algebraicMap₂) :
    RG₁ ≃+* RG₂
theorem

stageProjection_modelToModelRingEquiv

L268 ↗
CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.stageProjection_modelToModelRingEquiv
Documentation

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

Source context 17 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CanonicalCompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
variable {RG : ProfiniteRing.{w}}
variable {algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG}
variable {RG₁ : ProfiniteRing.{w}} {RG₂ : ProfiniteRing.{z}}
variable {algebraicMap₁ : CompletedGroupAlgebraNaturalSource R G →+* RG₁}
variable {algebraicMap₂ : CompletedGroupAlgebraNaturalSource R G →+* RG₂}
Lean source · statement
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
theorem

modelToModelRingEquiv_continuous

L291 ↗
CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.modelToModelRingEquiv_continuous
Documentation

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

Source context 17 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CanonicalCompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
variable {RG : ProfiniteRing.{w}}
variable {algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG}
variable {RG₁ : ProfiniteRing.{w}} {RG₂ : ProfiniteRing.{z}}
variable {algebraicMap₁ : CompletedGroupAlgebraNaturalSource R G →+* RG₁}
variable {algebraicMap₂ : CompletedGroupAlgebraNaturalSource R G →+* RG₂}
Lean source · statement
theorem modelToModelRingEquiv_continuous
    (h₁ : CanonicalCompletedGroupAlgebraModel R G RG₁ algebraicMap₁)
    (h₂ : CanonicalCompletedGroupAlgebraModel R G RG₂ algebraicMap₂) :
    Continuous (h₁.modelToModelRingEquiv h₂)
theorem

modelToModelRingEquiv_symm_continuous

L299 ↗
CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.modelToModelRingEquiv_symm_continuous
Documentation

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

Source context 17 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CanonicalCompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
variable {RG : ProfiniteRing.{w}}
variable {algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG}
variable {RG₁ : ProfiniteRing.{w}} {RG₂ : ProfiniteRing.{z}}
variable {algebraicMap₁ : CompletedGroupAlgebraNaturalSource R G →+* RG₁}
variable {algebraicMap₂ : CompletedGroupAlgebraNaturalSource R G →+* RG₂}
Lean source · statement
theorem modelToModelRingEquiv_symm_continuous
    (h₁ : CanonicalCompletedGroupAlgebraModel R G RG₁ algebraicMap₁)
    (h₂ : CanonicalCompletedGroupAlgebraModel R G RG₂ algebraicMap₂) :
    Continuous (h₁.modelToModelRingEquiv h₂).symm
theorem

modelToModelRingEquiv_algebraicMap

L308 ↗
CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.modelToModelRingEquiv_algebraicMap
Documentation

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

Source context 17 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CanonicalCompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
variable {RG : ProfiniteRing.{w}}
variable {algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG}
variable {RG₁ : ProfiniteRing.{w}} {RG₂ : ProfiniteRing.{z}}
variable {algebraicMap₁ : CompletedGroupAlgebraNaturalSource R G →+* RG₁}
variable {algebraicMap₂ : CompletedGroupAlgebraNaturalSource R G →+* RG₂}
Lean source · statement
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
theorem

modelToModelRingEquiv_comp_algebraicMap

L322 ↗
CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.modelToModelRingEquiv_comp_algebraicMap
Documentation

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

Source context 17 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CanonicalCompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
variable {RG : ProfiniteRing.{w}}
variable {algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG}
variable {RG₁ : ProfiniteRing.{w}} {RG₂ : ProfiniteRing.{z}}
variable {algebraicMap₁ : CompletedGroupAlgebraNaturalSource R G →+* RG₁}
variable {algebraicMap₂ : CompletedGroupAlgebraNaturalSource R G →+* RG₂}
Lean source · statement
theorem modelToModelRingEquiv_comp_algebraicMap
    (h₁ : CanonicalCompletedGroupAlgebraModel R G RG₁ algebraicMap₁)
    (h₂ : CanonicalCompletedGroupAlgebraModel R G RG₂ algebraicMap₂) :
    (h₁.modelToModelRingEquiv h₂).toRingHom.comp algebraicMap₁ = algebraicMap₂
theorem

modelToModelRingEquiv_unique

L333 ↗
CompletedGroupAlgebra.CanonicalCompletedGroupAlgebraModel.modelToModelRingEquiv_unique
Documentation

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.

Source context 17 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CanonicalCompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
variable {RG : ProfiniteRing.{w}}
variable {algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG}
variable {RG₁ : ProfiniteRing.{w}} {RG₂ : ProfiniteRing.{z}}
variable {algebraicMap₁ : CompletedGroupAlgebraNaturalSource R G →+* RG₁}
variable {algebraicMap₂ : CompletedGroupAlgebraNaturalSource R G →+* RG₂}
Lean source · statement
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₂
structure

CompletedGroupAlgebraModel

L368 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel
Documentation

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.

Source context 10 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
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)
def

certificate

L390 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.certificate
Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · full declaration
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
def

ofCertificate

L397 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.ofCertificate
Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · full declaration
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
theorem

algebraicMap_continuous

L408 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.algebraicMap_continuous
Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · statement
theorem algebraicMap_continuous (M : CompletedGroupAlgebraModel R G) :
    Continuous M.algebraicMap
theorem

algebraicMap_dense

L413 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.algebraicMap_dense
Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · statement
theorem algebraicMap_dense (M : CompletedGroupAlgebraModel R G) :
    DenseRange M.algebraicMap
def

coefficientMap

L418 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.coefficientMap
Documentation

Restriction of the algebraic map to the coefficient ring.

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · statement
def coefficientMap (M : CompletedGroupAlgebraModel R G) : R →+* M.carrier
def

groupMap

L423 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.groupMap
Documentation

Restriction of the algebraic map to group-like elements.

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · statement
def groupMap (M : CompletedGroupAlgebraModel R G) : G →* M.carrier
def

groupUnitsMap

L428 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.groupUnitsMap
Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · statement
def groupUnitsMap (M : CompletedGroupAlgebraModel R G) : G →* M.carrierˣ
theorem

groupUnitsMap_coe

L434 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.groupUnitsMap_coe
Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · statement
theorem groupUnitsMap_coe (M : CompletedGroupAlgebraModel R G) (g : G) :
    ((M.groupUnitsMap g : M.carrierˣ) : M.carrier) = M.groupMap g
def

comparisonRingEquiv

L439 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.comparisonRingEquiv
Documentation

The derived comparison with the concrete compatible-family model.

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · statement
def comparisonRingEquiv (M : CompletedGroupAlgebraModel R G) :
    M.carrier ≃+* CompletedGroupAlgebraCarrier R G
def

comparisonHomeomorph

L444 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.comparisonHomeomorph
Documentation

The derived comparison is a homeomorphism.

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · statement
def comparisonHomeomorph (M : CompletedGroupAlgebraModel R G) :
    M.carrier ≃ₜ CompletedGroupAlgebraCarrier R G
theorem

completedGroupAlgebraProjection_comparisonRingEquiv

L450 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.completedGroupAlgebraProjection_comparisonRingEquiv
Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · statement
theorem completedGroupAlgebraProjection_comparisonRingEquiv
    (M : CompletedGroupAlgebraModel R G) (U : CompletedGroupAlgebraIndex G) (x : M.carrier) :
    completedGroupAlgebraProjection R G U (M.comparisonRingEquiv x) =
      M.stageProjection U x
theorem

comparisonRingEquiv_algebraicMap

L458 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.comparisonRingEquiv_algebraicMap
Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · statement
theorem comparisonRingEquiv_algebraicMap (M : CompletedGroupAlgebraModel R G)
    (x : CompletedGroupAlgebraNaturalSource R G) :
    M.comparisonRingEquiv (M.algebraicMap x) =
      toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G) x
theorem

comparisonRingEquiv_coefficientMap

L466 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.comparisonRingEquiv_coefficientMap
Documentation

The comparison therefore respects the coefficient-ring embedding.

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · statement
theorem comparisonRingEquiv_coefficientMap (M : CompletedGroupAlgebraModel R G) (r : R) :
    M.comparisonRingEquiv (M.coefficientMap r) =
      algebraMap R (CompletedGroupAlgebraCarrier R G) r
theorem

comparisonRingEquiv_groupMap_source

L481 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.comparisonRingEquiv_groupMap_source
Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · statement
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)
def

modelEquiv

L489 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.modelEquiv
Documentation

Canonical equivalence between any two bundled models.

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · statement
def modelEquiv (M : CompletedGroupAlgebraModel.{u, v, w} R G)
    (N : CompletedGroupAlgebraModel.{u, v, z} R G) :
    M.carrier ≃+* N.carrier
theorem

modelEquiv_algebraicMap

L496 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.modelEquiv_algebraicMap
Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · statement
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
theorem

stageProjection_modelEquiv

L504 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.stageProjection_modelEquiv
Documentation

The canonical equivalence commutes with every finite-stage projection.

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · statement
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
theorem

modelEquiv_coefficientMap

L512 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.modelEquiv_coefficientMap
Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · statement
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
theorem

modelEquiv_groupMap

L520 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.modelEquiv_groupMap
Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · statement
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
theorem

modelEquiv_continuous

L527 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.modelEquiv_continuous
Documentation

The canonical equivalence between bundled models is continuous.

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · statement
theorem modelEquiv_continuous (M : CompletedGroupAlgebraModel.{u, v, w} R G)
    (N : CompletedGroupAlgebraModel.{u, v, z} R G) :
    Continuous (M.modelEquiv N)
theorem

modelEquiv_symm_continuous

L533 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.modelEquiv_symm_continuous
Documentation

Its inverse is continuous as well.

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · statement
theorem modelEquiv_symm_continuous (M : CompletedGroupAlgebraModel.{u, v, w} R G)
    (N : CompletedGroupAlgebraModel.{u, v, z} R G) :
    Continuous (M.modelEquiv N).symm
theorem

modelEquiv_unique

L540 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.modelEquiv_unique
Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · statement
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
def

completedGroupAlgebraProfiniteRing

L551 ↗
CompletedGroupAlgebra.completedGroupAlgebraProfiniteRing
Documentation

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

Source context 10 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def completedGroupAlgebraProfiniteRing
    (R : ProfiniteCommRing.{u}) (G : ProfiniteGrp.{v}) : ProfiniteRing
def

completedGroupAlgebraCanonicalModel

L565 ↗
CompletedGroupAlgebra.completedGroupAlgebraCanonicalModel
Documentation

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

Source context 10 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
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
def

completedGroupAlgebraModel

L593 ↗
CompletedGroupAlgebra.completedGroupAlgebraModel
Documentation

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.

Source context 10 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def completedGroupAlgebraModel
    (Λ : ProfiniteCommRing.{u}) (P : ProfiniteGrp.{v}) :
    CompletedGroupAlgebraModel Λ P
theorem

comparisonRingEquiv_groupMap

L607 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.comparisonRingEquiv_groupMap
Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · statement
theorem comparisonRingEquiv_groupMap (M : CompletedGroupAlgebraModel R G) (g : G) :
    M.comparisonRingEquiv (M.groupMap g) = completedGroupAlgebraOf R G g
theorem

toCompletedGroupAlgebraRingHom_mem_span_completedGroupAlgebraOf

L617 ↗
CompletedGroupAlgebra.toCompletedGroupAlgebraRingHom_mem_span_completedGroupAlgebraOf
Documentation

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

Source context 10 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem toCompletedGroupAlgebraRingHom_mem_span_completedGroupAlgebraOf
    (x : MonoidAlgebra R G) :
    toCompletedGroupAlgebraRingHom R G x ∈
      Submodule.span R (Set.range (completedGroupAlgebraOf R G))
theorem

completedGroupAlgebraOf_dense_span

L644 ↗
CompletedGroupAlgebra.completedGroupAlgebraOf_dense_span
Documentation

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

Source context 10 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem completedGroupAlgebraOf_dense_span :
    closure (Submodule.span R (Set.range (completedGroupAlgebraOf R G)) :
      Set (CompletedGroupAlgebraCarrier R G)) = Set.univ
theorem

completedGroupAlgebraContinuousLinearMap_ext_of_basis

L663 ↗
CompletedGroupAlgebra.completedGroupAlgebraContinuousLinearMap_ext_of_basis
Documentation

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.

Source context 10 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w z
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
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

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