ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.Maps

12 Theorems | 2 Definitions

This module lifts hereditary \(C\)-indexed finite-stage maps to the named completed carrier and proves their algebraic, topological, and dense-subalgebra characterizations.

import

ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.StageMaps

Imported by

Definition CompletedGroupAlgebra.completedGroupAlgebraMapInClass

def completedGroupAlgebraMapInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    (φ : G →* H) (hφ : Continuous φ) :
    CompletedGroupAlgebraInClass C R G →+* CompletedGroupAlgebraInClass C R H where
  toFun x :=
    (completedGroupAlgebraInClassCompatibleFamilyEquiv
      (R := R) (G := H) C).symm
      ((completedGroupAlgebraSystemInClass C R H).inverseLimitLift
        (fun V x =>
          completedGroupAlgebraFunctorialStageMapInClass
            (G := G) (H := H) C hHer (R := R) φ hφ V
            (completedGroupAlgebraProjectionInClass C R G
              (completedGroupAlgebraComapIndexInClass
                (G := G) (H := H) C hHer φ hφ V) x))
        (by
          intro V W hVW
          funext x
          have hcomp := congrFun
            (congrArg DFunLike.coe
              (completedGroupAlgebraFunctorialStageMapInClass_transition
                (R := R) (G := G) (H := H) C hHer φ hφ hVW))
            (completedGroupAlgebraProjectionInClass C R G
              (completedGroupAlgebraComapIndexInClass
                (G := G) (H := H) C hHer φ hφ W) x)
          rw [RingHom.comp_apply, RingHom.comp_apply] at hcomp
          simp only [Function.comp_apply]
          rw [← completedGroupAlgebraProjectionInClass_compatible
            (R := R) (G := G) C
            (completedGroupAlgebraComapIndexInClass_mono
              (G := G) (H := H) C hHer φ hφ hVW) x]
          exact hcomp) x)
  map_zero' := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := H) C
    intro V
    exact map_zero (completedGroupAlgebraFunctorialStageMapInClass
      (G := G) (H := H) C hHer (R := R) φ hφ V)
  map_one' := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := H) C
    intro V
    exact map_one (completedGroupAlgebraFunctorialStageMapInClass
      (G := G) (H := H) C hHer (R := R) φ hφ V)
  map_add' x y := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := H) C
    intro V
    exact map_add (completedGroupAlgebraFunctorialStageMapInClass
      (G := G) (H := H) C hHer (R := R) φ hφ V)
      (completedGroupAlgebraProjectionInClass C R G
        (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x)
      (completedGroupAlgebraProjectionInClass C R G
        (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) y)
  map_mul' x y := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := H) C
    intro V
    exact map_mul (completedGroupAlgebraFunctorialStageMapInClass
      (G := G) (H := H) C hHer (R := R) φ hφ V)
      (completedGroupAlgebraProjectionInClass C R G
        (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x)
      (completedGroupAlgebraProjectionInClass C R G
        (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) y)

A continuous homomorphism of groups induces a ring homomorphism on \(C\)-indexed completed group algebras, when \(C\) is hereditary.

Theorem CompletedGroupAlgebra.completedGroupAlgebraProjectionInClass_map

@[simp 900]
theorem completedGroupAlgebraProjectionInClass_map
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ)
    (V : CompletedGroupAlgebraIndexInClass H C) (x : CompletedGroupAlgebraInClass C R G) :
    completedGroupAlgebraProjectionInClass C R H V
        (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ x) =
      completedGroupAlgebraFunctorialStageMapInClass
        (G := G) (H := H) C hHer (R := R) φ hφ V
        (completedGroupAlgebraProjectionInClass C R G
          (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x)

The in-class completed group-algebra map is characterized by its finite-stage projections.

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraMapAlgHomInClass

def completedGroupAlgebraMapAlgHomInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    (φ : G →* H) (hφ : Continuous φ) :
    CompletedGroupAlgebraInClass C R G →ₐ[R] CompletedGroupAlgebraInClass C R H where
  toRingHom := completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ
  commutes' := by
    intro r
    apply completedGroupAlgebraInClass_ext (R := R) (G := H) C
    intro V
    change completedGroupAlgebraFunctorialStageMapInClass
        (G := G) (H := H) C hHer (R := R) φ hφ V
        (algebraMap R
          (CompletedGroupAlgebraStageInClass C R G
            (completedGroupAlgebraComapIndexInClass
              (G := G) (H := H) C hHer φ hφ V)) r) =
      algebraMap R (CompletedGroupAlgebraStageInClass C R H V) r
    exact completedGroupAlgebraFunctorialStageMapInClass_algebraMap
      (R := R) (G := G) (H := H) C hHer φ hφ V r

A continuous group homomorphism \(\varphi:G\to H\) induces an \(R\)-algebra homomorphism between the corresponding \(C\)-indexed completed group algebras.

Theorem CompletedGroupAlgebra.completedGroupAlgebraMapAlgHomInClass_apply

@[simp]
theorem completedGroupAlgebraMapAlgHomInClass_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (x : CompletedGroupAlgebraInClass C R G) :
    completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hHer R φ hφ x =
      completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ x

Evaluating the algebra homomorphism induced by \(\varphi\) at \(x\) gives completedGroupAlgebraMapInClass applied to \(x\).

Show Lean proof

Theorem CompletedGroupAlgebra.continuous_completedGroupAlgebraMapInClass

theorem continuous_completedGroupAlgebraMapInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) :
    Continuous (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ)

The induced \(C\)-indexed completed-group-algebra map is continuous.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraMapInClass_comp_toCompletedGroupAlgebraInClass

theorem completedGroupAlgebraMapInClass_comp_toCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) :
    (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ).comp
        (toCompletedGroupAlgebraInClassRingHom C R G) =
      (toCompletedGroupAlgebraInClassRingHom C R H).comp
        (MonoidAlgebra.mapDomainRingHom R φ)

The in-class completed group-algebra map composes with the dense abstract map as expected.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraMapInClass_surjective_of_surjective

theorem completedGroupAlgebraMapInClass_surjective_of_surjective
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (hH : HasOpenNormalBasisInClass C H)
    (φ : G →* H) (hφ : Continuous φ) (hφsurj : Function.Surjective φ) :
    Function.Surjective
      (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ)

A surjective continuous homomorphism onto a pro-\(C\) group induces a surjective map on \(C\)-indexed completed group algebras.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraInClassRingHom_ext_of_comp_toCompleted

theorem completedGroupAlgebraInClassRingHom_ext_of_comp_toCompleted
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (hG : HasOpenNormalBasisInClass C G)
    {f g : CompletedGroupAlgebraInClass C R G →+*
      CompletedGroupAlgebraInClass C R H}
    (hf : Continuous f) (hg : Continuous g)
    (hfg : f.comp (toCompletedGroupAlgebraInClassRingHom C R G) =
      g.comp (toCompletedGroupAlgebraInClassRingHom C R G)) :
    f = g

Continuous ring homomorphisms out of \(\widehat{R[G]}_C\) are determined by their values on the dense abstract group algebra.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraMapInClass_id

theorem completedGroupAlgebraMapInClass_id
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (hG : HasOpenNormalBasisInClass C G) :
    completedGroupAlgebraMapInClass (G := G) (H := G) C hHer R
        (MonoidHom.id G) continuous_id =
      RingHom.id (CompletedGroupAlgebraInClass C R G)

Identity law for the \(C\)-indexed completed-group-algebra functor.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraMapAlgHomInClass_id

theorem completedGroupAlgebraMapAlgHomInClass_id
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (hG : HasOpenNormalBasisInClass C G) :
    completedGroupAlgebraMapAlgHomInClass (G := G) (H := G) C hHer R
        (MonoidHom.id G) continuous_id =
      AlgHom.id R (CompletedGroupAlgebraInClass C R G)

Identity law for the \(C\)-indexed completed-group-algebra functor, as an \(R\)-algebra homomorphism.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraMapInClass_comp

theorem completedGroupAlgebraMapInClass_comp
    {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (hG : HasOpenNormalBasisInClass C G)
    (φ : G →* H) (hφ : Continuous φ) (ψ : H →* K) (hψ : Continuous ψ) :
    (completedGroupAlgebraMapInClass (G := H) (H := K) C hHer R ψ hψ).comp
        (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ) =
      completedGroupAlgebraMapInClass (G := G) (H := K) C hHer R
        (ψ.comp φ) (hψ.comp hφ)

Composition law for the \(C\)-indexed completed-group-algebra functor.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraMapAlgHomInClass_comp

theorem completedGroupAlgebraMapAlgHomInClass_comp
    {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (hG : HasOpenNormalBasisInClass C G)
    (φ : G →* H) (hφ : Continuous φ) (ψ : H →* K) (hψ : Continuous ψ) :
    (completedGroupAlgebraMapAlgHomInClass (G := H) (H := K) C hHer R ψ hψ).comp
        (completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hHer R φ hφ) =
      completedGroupAlgebraMapAlgHomInClass (G := G) (H := K) C hHer R
        (ψ.comp φ) (hψ.comp hφ)

Composition law for the \(C\)-indexed completed-group-algebra functor, as an \(R\)-algebra homomorphism.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraMapInClass_toCompletedGroupAlgebraInClass_of

@[simp]
theorem completedGroupAlgebraMapInClass_toCompletedGroupAlgebraInClass_of
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (g : G) :
    completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ
        (toCompletedGroupAlgebraInClass C R G (MonoidAlgebra.of R G g)) =
      toCompletedGroupAlgebraInClass C R H (MonoidAlgebra.of R H (φ g))

The in-class completed group-algebra map sends group-like elements to group-like elements.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraMapInClass_toCompletedGroupAlgebraInClass_sub_one_of

@[simp]
theorem completedGroupAlgebraMapInClass_toCompletedGroupAlgebraInClass_sub_one_of
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (g : G) :
    completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ
        (toCompletedGroupAlgebraInClass C R G (MonoidAlgebra.of R G g) - 1) =
      toCompletedGroupAlgebraInClass C R H (MonoidAlgebra.of R H (φ g)) - 1

The in-class completed group-algebra map sends group-like augmentation generators to their images.

Show Lean proof

ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.Maps

Declarations