Yamaguchi Lean 4 Library
ProCGroups.Completion.ProCGroupAlgebra
ProCGroups/Completion/ProCGroupAlgebra

ProCGroups.Completion.ProCGroupAlgebra

22 Theorem | 11 Definition | 5 Abbreviation | 1 Structure | 23 Instance

This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.

Open this file on GitHub
import
Imported by

Declarations

Abbreviation ProCGroups.Completion.ProCCompletedGroupAlgebraQuotientIndex GitHub 
abbrev ProCCompletedGroupAlgebraQuotientIndex :=
  OrderDual (ProC.OpenNormalSubgroupInClass C G)

The completed group-algebra indexing set records the open-normal quotient coordinate.

Abbreviation ProCGroups.Completion.ProCCompletedGroupAlgebraIndex GitHub 
abbrev ProCCompletedGroupAlgebraIndex :=
  ProCIntegerIndex C × ProCCompletedGroupAlgebraQuotientIndex C G

The full indexing set: a coefficient modulus and a group quotient.

Abbreviation ProCGroups.Completion.ProCCompletedGroupAlgebraQuotient GitHub 
abbrev ProCCompletedGroupAlgebraQuotient
    (U : ProCCompletedGroupAlgebraQuotientIndex C G) :=
  (ProC.openNormalSubgroupInClassSystem C G).X U

The quotient group \(G/U\) at one group-coordinate.

Abbreviation ProCGroups.Completion.ProCCompletedGroupAlgebraStage GitHub 
abbrev ProCCompletedGroupAlgebraStage
    (i : ProCCompletedGroupAlgebraIndex C G) :=
  MonoidAlgebra (ProCIntegerStage C i.1)
    (ProCCompletedGroupAlgebraQuotient C G i.2)

A finite stage of the pro-\(C\) completed group algebra, represented by compatible finite-stage coordinates.

Instance ProCGroups.Completion.instTopologicalSpaceProCCompletedGroupAlgebraStage GitHub 
instance instTopologicalSpaceProCCompletedGroupAlgebraStage
    (i : ProCCompletedGroupAlgebraIndex C G) :
    TopologicalSpace (ProCCompletedGroupAlgebraStage C G i) :=
  ⊥

The finite-stage pro-\(C\) completed group algebra carries its finite-stage topology.

Instance ProCGroups.Completion.instDiscreteTopologyProCCompletedGroupAlgebraStage GitHub 
instance instDiscreteTopologyProCCompletedGroupAlgebraStage
    (i : ProCCompletedGroupAlgebraIndex C G) :
    DiscreteTopology (ProCCompletedGroupAlgebraStage C G i) :=
  ⟨rfl⟩

The finite-stage pro-\(C\) completed group algebra carries the discrete topology.

Instance ProCGroups.Completion.instFiniteProCCompletedGroupAlgebraQuotient GitHub 
instance instFiniteProCCompletedGroupAlgebraQuotient
    (U : ProCCompletedGroupAlgebraQuotientIndex C G) :
    Finite (ProCCompletedGroupAlgebraQuotient C G U) := by
  dsimp [ProCCompletedGroupAlgebraQuotient, ProC.openNormalSubgroupInClassSystem]
  exact FiniteGroupClass.finite (C := C) (OrderDual.ofDual U).2

The group quotient in each completed group-algebra coordinate is finite.

Instance ProCGroups.Completion.instFiniteProCCompletedGroupAlgebraStage GitHub 
instance instFiniteProCCompletedGroupAlgebraStage
    (i : ProCCompletedGroupAlgebraIndex C G) :
    Finite (ProCCompletedGroupAlgebraStage C G i) := by
  classical
  letI : NeZero i.1.modulus := ⟨Nat.ne_of_gt i.1.positive⟩
  letI : Fintype (ProCIntegerStage C i.1) := ZMod.fintype i.1.modulus
  letI : Fintype (ProCCompletedGroupAlgebraQuotient C G i.2) := Fintype.ofFinite _
  letI : DecidableEq (ProCCompletedGroupAlgebraQuotient C G i.2) := Classical.decEq _
  dsimp [ProCCompletedGroupAlgebraStage, ProCIntegerStage]
  change Finite (ProCCompletedGroupAlgebraQuotient C G i.2 →₀ ZMod i.1.modulus)
  exact Finite.of_fintype _

Each completed group-algebra stage is finite.

Definition ProCGroups.Completion.proCCompletedGroupAlgebraQuotientTransition GitHub 
def proCCompletedGroupAlgebraQuotientTransition
    {U V : ProCCompletedGroupAlgebraQuotientIndex C G} (hUV : U ≤ V) :
    ProCCompletedGroupAlgebraQuotient C G V →*
      ProCCompletedGroupAlgebraQuotient C G U :=
  ProC.OpenNormalSubgroupInClass.map (C := C) (G := G)
    (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV

The transition map between group-coordinate quotients is induced by refinement of the modulus or finite quotient index.

Definition ProCGroups.Completion.proCCompletedGroupAlgebraTransition GitHub 
def proCCompletedGroupAlgebraTransition
    {i j : ProCCompletedGroupAlgebraIndex C G} (hij : i ≤ j) :
    ProCCompletedGroupAlgebraStage C G j →+*
      ProCCompletedGroupAlgebraStage C G i :=
  (MonoidAlgebra.mapDomainRingHom (ProCIntegerStage C i.1)
      (proCCompletedGroupAlgebraQuotientTransition (C := C) (G := G) hij.2)).comp
    (MonoidAlgebra.mapRangeRingHom
      (ProCCompletedGroupAlgebraQuotient C G j.2)
      (proCIntegerTransition (C := C) hij.1))

The transition map \((\mathbb{Z}/m\mathbb{Z})[G/V] \to (\mathbb{Z}/n\mathbb{Z})[G/U]\) for a refinement of coordinates.

Definition ProCGroups.Completion.ProCCompletedGroupAlgebraCompatible GitHub 
def ProCCompletedGroupAlgebraCompatible
    (x : ∀ i : ProCCompletedGroupAlgebraIndex C G,
      ProCCompletedGroupAlgebraStage C G i) : Prop :=
  ∀ i j, ∀ hij : i ≤ j,
    proCCompletedGroupAlgebraTransition (C := C) (G := G) hij (x j) = x i

The compatibility condition for a point of the inverse limit defining the completed group algebra.

Abbreviation ProCGroups.Completion.ProCCompletedGroupAlgebraLimitCarrier GitHub 
abbrev ProCCompletedGroupAlgebraLimitCarrier : Type _ :=
  {x : ∀ i : ProCCompletedGroupAlgebraIndex C G,
      ProCCompletedGroupAlgebraStage C G i //
    ProCCompletedGroupAlgebraCompatible C G x}

Carrier-level name for the pro-\(C\) inverse-limit implementation of the completed group algebra. Use this name when no Chapter 5 universal property is needed.

Structure ProCGroups.Completion.ProCCompletedGroupAlgebraModel GitHub 
structure ProCCompletedGroupAlgebraModel where
  carrier : Type v
  [ring : Ring carrier]
  [topology : TopologicalSpace carrier]
  [topologicalRing : IsTopologicalRing carrier]
  compact : CompactSpace carrier
  t2 : T2Space carrier
  coeff : ProCIntegerLimitCarrier C →+* carrier
  groupMap : G →* carrierˣ

The pro-\(C\) inverse-limit model of the completed group algebra, bundled with its topological ring structure and canonical coefficient and group maps. This bundle records only the constructed data; density and universal-property claims are provided by separate theorems.

Definition ProCGroups.Completion.proCCompletedGroupAlgebraProj GitHub 
def proCCompletedGroupAlgebraProj (i : ProCCompletedGroupAlgebraIndex C G) :
    ProCCompletedGroupAlgebraLimitCarrier C G → ProCCompletedGroupAlgebraStage C G i :=
  fun x => x.1 i

The projection from the pro-\(C\) completed group-algebra carrier to a finite group-algebra stage.

Theorem ProCGroups.Completion.ProCCompletedGroupAlgebraLimitCarrier.ext GitHub 
theorem ProCCompletedGroupAlgebraLimitCarrier.ext {x y : ProCCompletedGroupAlgebraLimitCarrier C G}
    (h : ∀ i : ProCCompletedGroupAlgebraIndex C G,
      proCCompletedGroupAlgebraProj (C := C) (G := G) i x =
        proCCompletedGroupAlgebraProj (C := C) (G := G) i y) :
    x = y

The pro-\(C\) completed group algebra is extensional: equality follows from equality of all finite-stage coordinates.

Show proof
Instance ProCGroups.Completion.instZeroProCCompletedGroupAlgebra GitHub 
instance instZeroProCCompletedGroupAlgebra :
    Zero (ProCCompletedGroupAlgebraLimitCarrier C G) where
  zero := ⟨fun _ => 0, by
    intro i j hij
    exact map_zero (proCCompletedGroupAlgebraTransition (C := C) (G := G) hij)⟩

The zero element is defined coordinatewise as the compatible family of zero elements at all finite stages.

Instance ProCGroups.Completion.instAddProCCompletedGroupAlgebra GitHub 
instance instAddProCCompletedGroupAlgebra :
    Add (ProCCompletedGroupAlgebraLimitCarrier C G) where
  add x y := ⟨fun i => x.1 i + y.1 i, by
    intro i j hij
    rw [map_add]
    exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩

The additive structure of the pro-\(C\) completed group algebra is inherited coordinatewise from finite group-algebra stages.

Instance ProCGroups.Completion.instNegProCCompletedGroupAlgebra GitHub 
instance instNegProCCompletedGroupAlgebra :
    Neg (ProCCompletedGroupAlgebraLimitCarrier C G) where
  neg x := ⟨fun i => -x.1 i, by
    intro i j hij
    rw [map_neg]
    exact congrArg Neg.neg (x.2 i j hij)⟩

Negation on the pro-\(C\) completed group algebra is defined coordinatewise through the finite-stage group-algebra negations.

Instance ProCGroups.Completion.instSubProCCompletedGroupAlgebra GitHub 
instance instSubProCCompletedGroupAlgebra :
    Sub (ProCCompletedGroupAlgebraLimitCarrier C G) where
  sub x y := ⟨fun i => x.1 i - y.1 i, by
    intro i j hij
    rw [map_sub]
    exact congrArg₂ HSub.hSub (x.2 i j hij) (y.2 i j hij)⟩

Subtraction on the completed group algebra is defined coordinatewise through the finite-stage group-algebra subtractions.

Instance ProCGroups.Completion.instSMulNatProCCompletedGroupAlgebra GitHub 
instance instSMulNatProCCompletedGroupAlgebra :
    SMul ℕ (ProCCompletedGroupAlgebraLimitCarrier C G) where
  smul n x := ⟨fun i => n • x.1 i, by
    intro i j hij
    rw [map_nsmul]
    exact congrArg (n • ·) (x.2 i j hij)⟩

The pro-\(C\) completed group algebra carries natural-number scalar multiplication coordinatewise.

Instance ProCGroups.Completion.instSMulIntProCCompletedGroupAlgebra GitHub 
instance instSMulIntProCCompletedGroupAlgebra :
    SMul ℤ (ProCCompletedGroupAlgebraLimitCarrier C G) where
  smul n x := ⟨fun i => n • x.1 i, by
    intro i j hij
    rw [map_zsmul]
    exact congrArg (n • ·) (x.2 i j hij)⟩

The completed group algebra carries integer scalar multiplication by applying the scalar action at every finite quotient stage.

Instance ProCGroups.Completion.instOneProCCompletedGroupAlgebra GitHub 
instance instOneProCCompletedGroupAlgebra :
    One (ProCCompletedGroupAlgebraLimitCarrier C G) where
  one := ⟨fun _ => 1, by
    intro i j hij
    exact map_one (proCCompletedGroupAlgebraTransition (C := C) (G := G) hij)⟩

The unit of the pro-\(C\) completed group algebra is defined coordinatewise.

Instance ProCGroups.Completion.instMulProCCompletedGroupAlgebra GitHub 
instance instMulProCCompletedGroupAlgebra :
    Mul (ProCCompletedGroupAlgebraLimitCarrier C G) where
  mul x y := ⟨fun i => x.1 i * y.1 i, by
    intro i j hij
    rw [map_mul]
    exact congrArg₂ HMul.hMul (x.2 i j hij) (y.2 i j hij)⟩

Multiplication on the completed group algebra is defined coordinatewise through the finite-stage group-algebra products.

Instance ProCGroups.Completion.instNatCastProCCompletedGroupAlgebra GitHub 
instance instNatCastProCCompletedGroupAlgebra :
    NatCast (ProCCompletedGroupAlgebraLimitCarrier C G) where
  natCast n := ⟨fun _ => n, by
    intro i j hij
    exact map_natCast (proCCompletedGroupAlgebraTransition (C := C) (G := G) hij) n⟩

Natural number casts in the pro-\(C\) completed group algebra are computed coordinatewise from finite-stage natural number casts.

Instance ProCGroups.Completion.instIntCastProCCompletedGroupAlgebra GitHub 
instance instIntCastProCCompletedGroupAlgebra :
    IntCast (ProCCompletedGroupAlgebraLimitCarrier C G) where
  intCast n := ⟨fun _ => n, by
    intro i j hij
    exact map_intCast (proCCompletedGroupAlgebraTransition (C := C) (G := G) hij) n⟩

Integer casts in the pro-\(C\) completed group algebra are computed coordinatewise from finite-stage integer casts.

Instance ProCGroups.Completion.instPowProCCompletedGroupAlgebra GitHub 
instance instPowProCCompletedGroupAlgebra :
    Pow (ProCCompletedGroupAlgebraLimitCarrier C G) ℕ where
  pow x n := ⟨fun i => x.1 i ^ n, by
    intro i j hij
    rw [map_pow]
    exact congrArg (fun t => t ^ n) (x.2 i j hij)⟩

The completed group algebra has powers computed at every finite-stage coordinate.

Theorem ProCGroups.Completion.coe_zero_proCCompletedGroupAlgebra GitHub 
theorem coe_zero_proCCompletedGroupAlgebra :
    ((0 : ProCCompletedGroupAlgebraLimitCarrier C G) :
      ∀ i : ProCCompletedGroupAlgebraIndex C G,
        ProCCompletedGroupAlgebraStage C G i) = 0

The underlying compatible family of the completed group algebra computes zero coordinatewise.

Show proof
Theorem ProCGroups.Completion.coe_one_proCCompletedGroupAlgebra GitHub 
theorem coe_one_proCCompletedGroupAlgebra :
    ((1 : ProCCompletedGroupAlgebraLimitCarrier C G) :
      ∀ i : ProCCompletedGroupAlgebraIndex C G,
        ProCCompletedGroupAlgebraStage C G i) = 1

The underlying compatible family of the completed group algebra computes \(1\) coordinatewise.

Show proof
Theorem ProCGroups.Completion.coe_add_proCCompletedGroupAlgebra GitHub 
theorem coe_add_proCCompletedGroupAlgebra (x y : ProCCompletedGroupAlgebraLimitCarrier C G) :
    ((x + y : ProCCompletedGroupAlgebraLimitCarrier C G) :
      ∀ i : ProCCompletedGroupAlgebraIndex C G,
        ProCCompletedGroupAlgebraStage C G i) = x + y

The underlying compatible family of the completed group algebra computes addition coordinatewise.

Show proof
Theorem ProCGroups.Completion.coe_mul_proCCompletedGroupAlgebra GitHub 
theorem coe_mul_proCCompletedGroupAlgebra (x y : ProCCompletedGroupAlgebraLimitCarrier C G) :
    ((x * y : ProCCompletedGroupAlgebraLimitCarrier C G) :
      ∀ i : ProCCompletedGroupAlgebraIndex C G,
        ProCCompletedGroupAlgebraStage C G i) = x * y

The underlying compatible family of the completed group algebra computes multiplication coordinatewise.

Show proof
Theorem ProCGroups.Completion.coe_neg_proCCompletedGroupAlgebra GitHub 
theorem coe_neg_proCCompletedGroupAlgebra (x : ProCCompletedGroupAlgebraLimitCarrier C G) :
    ((-x : ProCCompletedGroupAlgebraLimitCarrier C G) :
      ∀ i : ProCCompletedGroupAlgebraIndex C G,
        ProCCompletedGroupAlgebraStage C G i) = -x

The underlying compatible family of the completed group algebra computes negation coordinatewise.

Show proof
Theorem ProCGroups.Completion.coe_sub_proCCompletedGroupAlgebra GitHub 
theorem coe_sub_proCCompletedGroupAlgebra (x y : ProCCompletedGroupAlgebraLimitCarrier C G) :
    ((x - y : ProCCompletedGroupAlgebraLimitCarrier C G) :
      ∀ i : ProCCompletedGroupAlgebraIndex C G,
        ProCCompletedGroupAlgebraStage C G i) = x - y

The underlying compatible family of the completed group algebra computes subtraction coordinatewise.

Show proof
Theorem ProCGroups.Completion.coe_natCast_proCCompletedGroupAlgebra GitHub 
theorem coe_natCast_proCCompletedGroupAlgebra (n : ℕ) :
    ((n : ProCCompletedGroupAlgebraLimitCarrier C G) :
      ∀ i : ProCCompletedGroupAlgebraIndex C G,
        ProCCompletedGroupAlgebraStage C G i) = n

The underlying compatible family of the completed group algebra computes natural number casts coordinatewise.

Show proof
Theorem ProCGroups.Completion.coe_intCast_proCCompletedGroupAlgebra GitHub 
theorem coe_intCast_proCCompletedGroupAlgebra (n : ℤ) :
    ((n : ProCCompletedGroupAlgebraLimitCarrier C G) :
      ∀ i : ProCCompletedGroupAlgebraIndex C G,
        ProCCompletedGroupAlgebraStage C G i) =
      fun i => (n : ProCCompletedGroupAlgebraStage C G i)

The underlying compatible family of the completed group algebra computes integer casts coordinatewise.

Show proof
Theorem ProCGroups.Completion.coe_pow_proCCompletedGroupAlgebra GitHub 
theorem coe_pow_proCCompletedGroupAlgebra (x : ProCCompletedGroupAlgebraLimitCarrier C G) (n : ℕ) :
    ((x ^ n : ProCCompletedGroupAlgebraLimitCarrier C G) :
      ∀ i : ProCCompletedGroupAlgebraIndex C G,
        ProCCompletedGroupAlgebraStage C G i) = x ^ n

The underlying compatible family of the completed group algebra computes powers coordinatewise.

Show proof
Instance ProCGroups.Completion.instRingProCCompletedGroupAlgebra GitHub 
instance instRingProCCompletedGroupAlgebra : Ring (ProCCompletedGroupAlgebraLimitCarrier C G) :=
  Function.Injective.ring
    (fun x : ProCCompletedGroupAlgebraLimitCarrier C G =>
      (x : ∀ i : ProCCompletedGroupAlgebraIndex C G,
        ProCCompletedGroupAlgebraStage C G i))
    Subtype.val_injective
    (coe_zero_proCCompletedGroupAlgebra (C := C) (G := G))
    (coe_one_proCCompletedGroupAlgebra (C := C) (G := G))
    (coe_add_proCCompletedGroupAlgebra (C := C) (G := G))
    (coe_mul_proCCompletedGroupAlgebra (C := C) (G := G))
    (coe_neg_proCCompletedGroupAlgebra (C := C) (G := G))
    (coe_sub_proCCompletedGroupAlgebra (C := C) (G := G))
    (by intro n x; funext i; change (n • x).1 i = n • x.1 i; rfl)
    (by intro n x; funext i; change (n • x).1 i = n • x.1 i; rfl)
    (coe_pow_proCCompletedGroupAlgebra (C := C) (G := G))
    (coe_natCast_proCCompletedGroupAlgebra (C := C) (G := G))
    (coe_intCast_proCCompletedGroupAlgebra (C := C) (G := G))

The completed group algebra is a ring because all ring operations and ring axioms are inherited coordinatewise from the finite-stage group algebras.

Theorem ProCGroups.Completion.proCCompletedGroupAlgebraProj_zero GitHub 
theorem proCCompletedGroupAlgebraProj_zero
    (i : ProCCompletedGroupAlgebraIndex C G) :
    proCCompletedGroupAlgebraProj (C := C) (G := G) i
      (0 : ProCCompletedGroupAlgebraLimitCarrier C G) = 0

The finite-stage projection from the pro-\(C\) completed group algebra sends \(0\) to \(0\).

Show proof
Theorem ProCGroups.Completion.proCCompletedGroupAlgebraProj_one GitHub 
theorem proCCompletedGroupAlgebraProj_one
    (i : ProCCompletedGroupAlgebraIndex C G) :
    proCCompletedGroupAlgebraProj (C := C) (G := G) i
      (1 : ProCCompletedGroupAlgebraLimitCarrier C G) = 1

The finite-stage projection from the pro-\(C\) completed group algebra sends \(1\) to \(1\).

Show proof
Theorem ProCGroups.Completion.proCCompletedGroupAlgebraProj_add GitHub 
theorem proCCompletedGroupAlgebraProj_add
    (i : ProCCompletedGroupAlgebraIndex C G) (x y : ProCCompletedGroupAlgebraLimitCarrier C G) :
    proCCompletedGroupAlgebraProj (C := C) (G := G) i (x + y) =
      proCCompletedGroupAlgebraProj (C := C) (G := G) i x +
        proCCompletedGroupAlgebraProj (C := C) (G := G) i y

The finite-stage projection from the pro-\(C\) completed group algebra preserves addition.

Show proof
Theorem ProCGroups.Completion.proCCompletedGroupAlgebraProj_mul GitHub 
theorem proCCompletedGroupAlgebraProj_mul
    (i : ProCCompletedGroupAlgebraIndex C G) (x y : ProCCompletedGroupAlgebraLimitCarrier C G) :
    proCCompletedGroupAlgebraProj (C := C) (G := G) i (x * y) =
      proCCompletedGroupAlgebraProj (C := C) (G := G) i x *
        proCCompletedGroupAlgebraProj (C := C) (G := G) i y

The finite-stage projection from the pro-\(C\) completed group algebra preserves multiplication.

Show proof
Theorem ProCGroups.Completion.proCCompletedGroupAlgebraProj_neg GitHub 
theorem proCCompletedGroupAlgebraProj_neg
    (i : ProCCompletedGroupAlgebraIndex C G) (x : ProCCompletedGroupAlgebraLimitCarrier C G) :
    proCCompletedGroupAlgebraProj (C := C) (G := G) i (-x) =
      -proCCompletedGroupAlgebraProj (C := C) (G := G) i x

The finite-stage projection from the pro-\(C\) completed group algebra preserves negation.

Show proof
Theorem ProCGroups.Completion.proCCompletedGroupAlgebraProj_sub GitHub 
theorem proCCompletedGroupAlgebraProj_sub
    (i : ProCCompletedGroupAlgebraIndex C G) (x y : ProCCompletedGroupAlgebraLimitCarrier C G) :
    proCCompletedGroupAlgebraProj (C := C) (G := G) i (x - y) =
      proCCompletedGroupAlgebraProj (C := C) (G := G) i x -
        proCCompletedGroupAlgebraProj (C := C) (G := G) i y

The finite-stage projection from the pro-\(C\) completed group algebra preserves subtraction.

Show proof
Definition ProCGroups.Completion.proCCompletedGroupAlgebraProjRingHom GitHub 
def proCCompletedGroupAlgebraProjRingHom
    (i : ProCCompletedGroupAlgebraIndex C G) :
    ProCCompletedGroupAlgebraLimitCarrier C G →+* ProCCompletedGroupAlgebraStage C G i where
  toFun := proCCompletedGroupAlgebraProj (C := C) (G := G) i
  map_zero' := by simp only [proCCompletedGroupAlgebraProj_zero]
  map_one' := by simp only [proCCompletedGroupAlgebraProj_one]
  map_add' := by intro x y; simp only [proCCompletedGroupAlgebraProj_add]
  map_mul' := by intro x y; simp only [proCCompletedGroupAlgebraProj_mul]

The projection from the completed group algebra to a finite group-algebra stage is bundled as a ring homomorphism.

Theorem ProCGroups.Completion.proCCompletedGroupAlgebraProjRingHom_apply GitHub 
theorem proCCompletedGroupAlgebraProjRingHom_apply
    (i : ProCCompletedGroupAlgebraIndex C G) (x : ProCCompletedGroupAlgebraLimitCarrier C G) :
    proCCompletedGroupAlgebraProjRingHom (C := C) (G := G) i x =
      proCCompletedGroupAlgebraProj (C := C) (G := G) i x

The bundled ring homomorphism has the same underlying function as the coordinatewise construction.

Show proof
Theorem ProCGroups.Completion.continuous_proCCompletedGroupAlgebraProj GitHub 
theorem continuous_proCCompletedGroupAlgebraProj
    (i : ProCCompletedGroupAlgebraIndex C G) :
    Continuous (proCCompletedGroupAlgebraProj (C := C) (G := G) i)

Each finite projection from the completed group algebra is continuous.

Show proof
Theorem ProCGroups.Completion.proCCompletedGroupAlgebraProj_transition GitHub 
theorem proCCompletedGroupAlgebraProj_transition
    {i j : ProCCompletedGroupAlgebraIndex C G} (hij : i ≤ j)
    (x : ProCCompletedGroupAlgebraLimitCarrier C G) :
    proCCompletedGroupAlgebraTransition (C := C) (G := G) hij
        (proCCompletedGroupAlgebraProj (C := C) (G := G) j x) =
      proCCompletedGroupAlgebraProj (C := C) (G := G) i x

Compatibility of the finite projections with completed group-algebra transition maps.

Show proof
Theorem ProCGroups.Completion.isClosed_setOf_completedGroupAlgebraCompatible GitHub 
theorem isClosed_setOf_completedGroupAlgebraCompatible :
    IsClosed {x : ∀ i : ProCCompletedGroupAlgebraIndex C G,
        ProCCompletedGroupAlgebraStage C G i |
      ProCCompletedGroupAlgebraCompatible C G x}

The compatibility condition defining the completed group algebra is closed in the product of finite stages.

Show proof
Instance ProCGroups.Completion.instCompactSpaceProCCompletedGroupAlgebraLimitCarrier GitHub 
instance instCompactSpaceProCCompletedGroupAlgebraLimitCarrier :
    CompactSpace (ProCCompletedGroupAlgebraLimitCarrier C G) := by
  letI : ∀ i : ProCCompletedGroupAlgebraIndex C G,
      CompactSpace (ProCCompletedGroupAlgebraStage C G i) := fun _ => inferInstance
  let hs : IsClosed {x : ∀ i : ProCCompletedGroupAlgebraIndex C G,
      ProCCompletedGroupAlgebraStage C G i |
      ProCCompletedGroupAlgebraCompatible C G x} :=
    isClosed_setOf_completedGroupAlgebraCompatible (C := C) (G := G)
  simpa [ProCCompletedGroupAlgebraLimitCarrier] using hs.isClosedEmbedding_subtypeVal.compactSpace

The pro-\(C\) completed group-algebra limit carrier is compact.

Instance ProCGroups.Completion.instT2SpaceProCCompletedGroupAlgebraLimitCarrier GitHub 
instance instT2SpaceProCCompletedGroupAlgebraLimitCarrier :
    T2Space (ProCCompletedGroupAlgebraLimitCarrier C G) := by
  change T2Space {x : ∀ i : ProCCompletedGroupAlgebraIndex C G,
      ProCCompletedGroupAlgebraStage C G i //
      ProCCompletedGroupAlgebraCompatible C G x}
  infer_instance

The pro-\(C\) completed group-algebra limit carrier is a \(T_2\) space.

Instance ProCGroups.Completion.instContinuousAddProCCompletedGroupAlgebraLimitCarrier GitHub 
instance instContinuousAddProCCompletedGroupAlgebraLimitCarrier :
    ContinuousAdd (ProCCompletedGroupAlgebraLimitCarrier C G) where
  continuous_add := by
    refine Continuous.subtype_mk (continuous_pi fun i => ?_) (fun p => (p.1 + p.2).2)
    change Continuous fun p : ProCCompletedGroupAlgebraLimitCarrier C G ×
        ProCCompletedGroupAlgebraLimitCarrier C G =>
      proCCompletedGroupAlgebraProj (C := C) (G := G) i p.1 +
        proCCompletedGroupAlgebraProj (C := C) (G := G) i p.2
    exact ((continuous_proCCompletedGroupAlgebraProj (C := C) (G := G) i).comp
        continuous_fst).add
      ((continuous_proCCompletedGroupAlgebraProj (C := C) (G := G) i).comp continuous_snd)

Addition on the pro-\(C\) completed group algebra is continuous for the inverse-limit topology.

Instance ProCGroups.Completion.instContinuousMulProCCompletedGroupAlgebraLimitCarrier GitHub 
instance instContinuousMulProCCompletedGroupAlgebraLimitCarrier :
    ContinuousMul (ProCCompletedGroupAlgebraLimitCarrier C G) where
  continuous_mul := by
    refine Continuous.subtype_mk (continuous_pi fun i => ?_) (fun p => (p.1 * p.2).2)
    change Continuous fun p : ProCCompletedGroupAlgebraLimitCarrier C G ×
        ProCCompletedGroupAlgebraLimitCarrier C G =>
      proCCompletedGroupAlgebraProj (C := C) (G := G) i p.1 *
        proCCompletedGroupAlgebraProj (C := C) (G := G) i p.2
    exact ((continuous_proCCompletedGroupAlgebraProj (C := C) (G := G) i).comp
        continuous_fst).mul
      ((continuous_proCCompletedGroupAlgebraProj (C := C) (G := G) i).comp continuous_snd)

Multiplication on the completed group algebra is continuous for the inverse-limit topology.

Instance ProCGroups.Completion.instContinuousNegProCCompletedGroupAlgebraLimitCarrier GitHub 
instance instContinuousNegProCCompletedGroupAlgebraLimitCarrier :
    ContinuousNeg (ProCCompletedGroupAlgebraLimitCarrier C G) where
  continuous_neg := by
    refine Continuous.subtype_mk (continuous_pi fun i => ?_) (fun x => (-x).2)
    change Continuous fun x : ProCCompletedGroupAlgebraLimitCarrier C G =>
      -proCCompletedGroupAlgebraProj (C := C) (G := G) i x
    exact (continuous_proCCompletedGroupAlgebraProj (C := C) (G := G) i).neg

Negation on the completed group algebra is continuous for the inverse-limit topology.

Instance ProCGroups.Completion.ProCCompletedGroupAlgebraLimitCarrier.instIsTopologicalRing GitHub 
instance ProCCompletedGroupAlgebraLimitCarrier.instIsTopologicalRing :
    IsTopologicalRing (ProCCompletedGroupAlgebraLimitCarrier C G) := by
  letI : ContinuousAdd (ProCCompletedGroupAlgebraLimitCarrier C G) :=
    instContinuousAddProCCompletedGroupAlgebraLimitCarrier (C := C) (G := G)
  letI : ContinuousMul (ProCCompletedGroupAlgebraLimitCarrier C G) :=
    instContinuousMulProCCompletedGroupAlgebraLimitCarrier (C := C) (G := G)
  letI : ContinuousNeg (ProCCompletedGroupAlgebraLimitCarrier C G) :=
    instContinuousNegProCCompletedGroupAlgebraLimitCarrier (C := C) (G := G)
  letI : IsTopologicalSemiring (ProCCompletedGroupAlgebraLimitCarrier C G) :=
    IsTopologicalSemiring.mk
  exact IsTopologicalRing.mk

The pro-\(C\) completed group-algebra carrier inherits a ring structure from the compatible finite-stage rings.

Definition ProCGroups.Completion.proCIntegerToProCCompletedGroupAlgebra GitHub 
def proCIntegerToProCCompletedGroupAlgebra :
    ProCIntegerLimitCarrier C →+* ProCCompletedGroupAlgebraLimitCarrier C G where
  toFun z := ⟨fun i =>
      algebraMap (ProCIntegerStage C i.1) (ProCCompletedGroupAlgebraStage C G i)
        (proCIntegerProj (C := C) i.1 z), by
    intro i j hij
    simp only [proCCompletedGroupAlgebraTransition, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self,
  RingHom.coe_id, Function.comp_apply, id_eq, RingHom.coe_comp, MonoidAlgebra.mapRangeRingHom_single,
  proCIntegerProj_transition (C := C) hij.1 z, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single,
  map_one]⟩
  map_zero' := by
    apply ProCCompletedGroupAlgebraLimitCarrier.ext
    intro i
    exact map_zero (algebraMap (ProCIntegerStage C i.1)
      (ProCCompletedGroupAlgebraStage C G i))
  map_one' := by
    apply ProCCompletedGroupAlgebraLimitCarrier.ext
    intro i
    exact map_one (algebraMap (ProCIntegerStage C i.1)
      (ProCCompletedGroupAlgebraStage C G i))
  map_add' := by
    intro x y
    apply ProCCompletedGroupAlgebraLimitCarrier.ext
    intro i
    exact map_add (algebraMap (ProCIntegerStage C i.1)
      (ProCCompletedGroupAlgebraStage C G i))
      (proCIntegerProj (C := C) i.1 x) (proCIntegerProj (C := C) i.1 y)
  map_mul' := by
    intro x y
    apply ProCCompletedGroupAlgebraLimitCarrier.ext
    intro i
    exact map_mul (algebraMap (ProCIntegerStage C i.1)
      (ProCCompletedGroupAlgebraStage C G i))
      (proCIntegerProj (C := C) i.1 x) (proCIntegerProj (C := C) i.1 y)

The coefficient embedding into the completed group algebra.

Theorem ProCGroups.Completion.proCCompletedGroupAlgebraProj_proCIntegerToProCCompletedGroupAlgebra GitHub 
theorem proCCompletedGroupAlgebraProj_proCIntegerToProCCompletedGroupAlgebra
    (i : ProCCompletedGroupAlgebraIndex C G) (z : ProCIntegerLimitCarrier C) :
    proCCompletedGroupAlgebraProj (C := C) (G := G) i
        (proCIntegerToProCCompletedGroupAlgebra (C := C) (G := G) z) =
      algebraMap (ProCIntegerStage C i.1) (ProCCompletedGroupAlgebraStage C G i)
        (proCIntegerProj (C := C) i.1 z)

Projecting the coefficient embedding into the completed group algebra applies the stage algebra map.

Show proof
Instance ProCGroups.Completion.instAlgebraProCIntegerLimitCarrierProCCompletedGroupAlgebraLimitCarrier GitHub 
instance instAlgebraProCIntegerLimitCarrierProCCompletedGroupAlgebraLimitCarrier :
    Algebra (ProCIntegerLimitCarrier C) (ProCCompletedGroupAlgebraLimitCarrier C G) :=
  RingHom.toAlgebra'
    (proCIntegerToProCCompletedGroupAlgebra (C := C) (G := G))
    (by
      intro z x
      apply ProCCompletedGroupAlgebraLimitCarrier.ext
      intro i
      change
        algebraMap (ProCIntegerStage C i.1) (ProCCompletedGroupAlgebraStage C G i)
            (proCIntegerProj (C := C) i.1 z) *
          proCCompletedGroupAlgebraProj (C := C) (G := G) i x =
        proCCompletedGroupAlgebraProj (C := C) (G := G) i x *
          algebraMap (ProCIntegerStage C i.1) (ProCCompletedGroupAlgebraStage C G i)
            (proCIntegerProj (C := C) i.1 z)
      exact Algebra.commutes _ _)

The completed group algebra is an algebra over the coefficient ring via the coordinatewise finite-stage algebra maps.

Definition ProCGroups.Completion.proCCompletedGroupAlgebraOf GitHub 
def proCCompletedGroupAlgebraOf : G →* ProCCompletedGroupAlgebraLimitCarrier C G where
  toFun g := ⟨fun i =>
      MonoidAlgebra.of (ProCIntegerStage C i.1)
        (ProCCompletedGroupAlgebraQuotient C G i.2)
        (ProC.openNormalSubgroupInClassProj (C := C) (G := G) i.2 g), by
    intro i j hij
    have hq :=
      congrFun (ProC.openNormalSubgroupInClassProj_compatible
        (C := C) (G := G) i.2 j.2 hij.2) g
    simpa [proCCompletedGroupAlgebraTransition,
      proCCompletedGroupAlgebraQuotientTransition] using
      congrArg (fun q =>
        MonoidAlgebra.of (ProCIntegerStage C i.1)
          (ProCCompletedGroupAlgebraQuotient C G i.2) q) hq⟩
  map_one' := by
    apply ProCCompletedGroupAlgebraLimitCarrier.ext
    intro i
    change
      MonoidAlgebra.of (ProCIntegerStage C i.1)
          (ProCCompletedGroupAlgebraQuotient C G i.2)
          (ProC.openNormalSubgroupInClassProj (C := C) (G := G) i.2 1) =
        1
    rfl
  map_mul' g h := by
    apply ProCCompletedGroupAlgebraLimitCarrier.ext
    intro i
    change
      MonoidAlgebra.of (ProCIntegerStage C i.1)
          (ProCCompletedGroupAlgebraQuotient C G i.2)
          (ProC.openNormalSubgroupInClassProj (C := C) (G := G) i.2 (g * h)) =
        MonoidAlgebra.of (ProCIntegerStage C i.1)
            (ProCCompletedGroupAlgebraQuotient C G i.2)
            (ProC.openNormalSubgroupInClassProj (C := C) (G := G) i.2 g) *
          MonoidAlgebra.of (ProCIntegerStage C i.1)
            (ProCCompletedGroupAlgebraQuotient C G i.2)
            (ProC.openNormalSubgroupInClassProj (C := C) (G := G) i.2 h)
    simp only [ProC.openNormalSubgroupInClassProj, QuotientGroup.mk'_apply, QuotientGroup.mk_mul,
  MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single, mul_one]

The canonical group map into the pro-\(C\) completed group algebra sends \(g\) to its compatible system of group-like basis elements.

Theorem ProCGroups.Completion.proCCompletedGroupAlgebraProj_of GitHub 
theorem proCCompletedGroupAlgebraProj_of
    (i : ProCCompletedGroupAlgebraIndex C G) (g : G) :
    proCCompletedGroupAlgebraProj (C := C) (G := G) i
        (proCCompletedGroupAlgebraOf (C := C) (G := G) g) =
      MonoidAlgebra.of (ProCIntegerStage C i.1)
        (ProCCompletedGroupAlgebraQuotient C G i.2)
        (ProC.openNormalSubgroupInClassProj (C := C) (G := G) i.2 g)

Projecting a group element into the completed group algebra gives the corresponding finite basis element.

Show proof
Definition ProCGroups.Completion.groupBasisUnit GitHub 
def groupBasisUnit (g : G) : (ProCCompletedGroupAlgebraLimitCarrier C G)ˣ where
  val := proCCompletedGroupAlgebraOf (C := C) (G := G) g
  inv := proCCompletedGroupAlgebraOf (C := C) (G := G) g⁻¹
  val_inv := by
    rw [← map_mul]
    simp only [mul_inv_cancel, map_one]
  inv_val := by
    rw [← map_mul]
    simp only [inv_mul_cancel, map_one]

A group element gives a unit in the completed group-algebra limit carrier.

Definition ProCGroups.Completion.ProCCompletedGroupAlgebraModel.groupToUnits GitHub 
def ProCCompletedGroupAlgebraModel.groupToUnits : G →* (ProCCompletedGroupAlgebraLimitCarrier C G)ˣ where
  toFun := groupBasisUnit (C := C) (G := G)
  map_one' := by
    ext
    simp only [groupBasisUnit, map_one, inv_one, proCCompletedGroupAlgebraProj_one, Units.val_one]
  map_mul' g h := by
    ext
    simp only [groupBasisUnit, map_mul, mul_inv_rev, proCCompletedGroupAlgebraProj_mul,
  proCCompletedGroupAlgebraProj_of, MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single, mul_one, Units.val_mul]

The canonical map from \(G\) to units in the completed group-algebra limit carrier.

Definition ProCGroups.Completion.ProCCompletedGroupAlgebraModel.lift GitHub 
def lift
    {R : Type v} [Ring R] [TopologicalSpace R] [IsTopologicalRing R]
    (f : ∀ i : ProCCompletedGroupAlgebraIndex C G,
      R →+* ProCCompletedGroupAlgebraStage C G i)
    (hf_compat : ∀ i j (hij : i ≤ j),
      (proCCompletedGroupAlgebraTransition (C := C) (G := G) hij).comp (f j) = f i) :
    R →+* ProCCompletedGroupAlgebraLimitCarrier C G where
  toFun r := ⟨fun i => f i r, by
    intro i j hij
    exact congrArg (fun φ : R →+* ProCCompletedGroupAlgebraStage C G i => φ r)
      (hf_compat i j hij)⟩
  map_zero' := by
    apply ProCCompletedGroupAlgebraLimitCarrier.ext
    intro i
    exact map_zero (f i)
  map_one' := by
    apply ProCCompletedGroupAlgebraLimitCarrier.ext
    intro i
    exact map_one (f i)
  map_add' := by
    intro x y
    apply ProCCompletedGroupAlgebraLimitCarrier.ext
    intro i
    exact map_add (f i) x y
  map_mul' := by
    intro x y
    apply ProCCompletedGroupAlgebraLimitCarrier.ext
    intro i
    exact map_mul (f i) x y

Compatible maps into the finite stages lift to the completed group-algebra limit carrier.

Definition ProCGroups.Completion.proCCompletedGroupAlgebraModel GitHub 
def proCCompletedGroupAlgebraModel :
    ProCCompletedGroupAlgebraModel C G where
  carrier := ProCCompletedGroupAlgebraLimitCarrier C G
  ring := inferInstance
  topology := inferInstance
  topologicalRing := inferInstance
  compact := inferInstance
  t2 := inferInstance
  coeff := proCIntegerToProCCompletedGroupAlgebra (C := C) (G := G)
  groupMap := ProCCompletedGroupAlgebraModel.groupToUnits (C := C) (G := G)

The inverse-limit carrier is bundled as a completed group-algebra object.