ProCGroups.CompletedGroupAlgebra.Basic.ClassComparison

21 Theorems | 10 Definitions

This module compares the all-finite and \(C\)-indexed named completed carriers through their canonical projections, and bundles the resulting inverse maps as ring, algebra, and topological equivalences for pro-\(C\) groups.

imports

Imported by

Definition CompletedGroupAlgebra.completedGroupAlgebraProjectionToStageInClass

def completedGroupAlgebraProjectionToStageInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    CompletedGroupAlgebraCarrier R G →+* CompletedGroupAlgebraStageInClass C R G U :=
  completedGroupAlgebraProjection R G
    (completedGroupAlgebraIndexInClassToAllFinite G C U)

The projection from the all-finite completion to a stage indexed by a finite quotient class \(C\), bundled as a ring homomorphism.

Theorem CompletedGroupAlgebra.completedGroupAlgebraProjectionToStageInClass_compatible

theorem completedGroupAlgebraProjectionToStageInClass_compatible
    (C : ProCGroups.FiniteGroupClass.{v})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
    (x : CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraTransitionInClass C R G hUV
        (completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C V x) =
      completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C U x

The all-finite projection to a \(C\)-indexed stage is compatible with the transition maps of the \(C\)-indexed tower.

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraToInClass

def completedGroupAlgebraToInClass
    (C : ProCGroups.FiniteGroupClass.{v}) :
    CompletedGroupAlgebraCarrier R G → CompletedGroupAlgebraInClass C R G :=
  fun x =>
    (completedGroupAlgebraInClassCompatibleFamilyEquiv
      (R := R) (G := G) C).symm
      ((completedGroupAlgebraSystemInClass C R G).inverseLimitLift
        (fun U =>
          completedGroupAlgebraProjectionToStageInClass
            (R := R) (G := G) C U)
        (by
          intro U V hUV
          funext x
          exact completedGroupAlgebraProjectionToStageInClass_compatible
            (R := R) (G := G) C hUV x) x)

The comparison map from the ordinary all-finite completed group algebra to the inverse limit over any finite-quotient class.

Theorem CompletedGroupAlgebra.completedGroupAlgebraToInClass_projection

@[simp]
theorem completedGroupAlgebraToInClass_projection
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) (x : CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraProjectionInClass C R G U
        (completedGroupAlgebraToInClass (R := R) (G := G) C x) =
      completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C U x

Projecting the comparison map \(\widehat{R[G]}\to\widehat{R[G]}_{C}\) to a \(C\)-indexed finite stage recovers the corresponding all-finite projection.

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraToInClassRingHom

def completedGroupAlgebraToInClassRingHom
    (C : ProCGroups.FiniteGroupClass.{v}) :
    CompletedGroupAlgebraCarrier R G →+* CompletedGroupAlgebraInClass C R G where
  toFun := completedGroupAlgebraToInClass (R := R) (G := G) C
  map_zero' := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    rfl
  map_one' := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    rfl
  map_add' x y := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    rfl
  map_mul' x y := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    rfl

The comparison from the all-finite completed group algebra to the \(C\)-indexed inverse limit is bundled as a ring homomorphism.

Theorem CompletedGroupAlgebra.completedGroupAlgebraToInClassRingHom_apply

@[simp]
theorem completedGroupAlgebraToInClassRingHom_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (x : CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraToInClassRingHom (R := R) (G := G) C x =
      completedGroupAlgebraToInClass (R := R) (G := G) C x

The comparison map from the all-finite completed group algebra to the \(C\)-indexed model is evaluated by reading the corresponding finite-stage coordinate.

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraToInClassAlgHom

def completedGroupAlgebraToInClassAlgHom
    (C : ProCGroups.FiniteGroupClass.{v}) :
    CompletedGroupAlgebraCarrier R G →ₐ[R] CompletedGroupAlgebraInClass C R G where
  toRingHom := completedGroupAlgebraToInClassRingHom (R := R) (G := G) C
  commutes' := by
    intro r
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    rfl

The comparison from the all-finite completed group algebra to the \(C\)-indexed inverse limit, as an \(R\)-algebra homomorphism.

Theorem CompletedGroupAlgebra.completedGroupAlgebraToInClassAlgHom_apply

@[simp]
theorem completedGroupAlgebraToInClassAlgHom_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (x : CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraToInClassAlgHom (R := R) (G := G) C x =
      completedGroupAlgebraToInClass (R := R) (G := G) C x

The comparison map from the all-finite completed group algebra to the \(C\)-indexed model is evaluated by reading the corresponding finite-stage coordinate.

Show Lean proof

Theorem CompletedGroupAlgebra.continuous_completedGroupAlgebraToInClass

theorem continuous_completedGroupAlgebraToInClass
    (C : ProCGroups.FiniteGroupClass.{v}) :
    Continuous (completedGroupAlgebraToInClass (R := R) (G := G) C )

The comparison map from the all-finite completed group algebra to the \(C\)-indexed completed group algebra is continuous for the inverse-limit topology.

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraFromInClass

def completedGroupAlgebraFromInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    CompletedGroupAlgebraInClass C R G → CompletedGroupAlgebraCarrier R G :=
  fun x =>
    (completedGroupAlgebraCompatibleFamilyEquiv (R := R) (G := G)).symm
      ((completedGroupAlgebraSystem R G).inverseLimitLift
        (fun U : CompletedGroupAlgebraIndex G =>
          completedGroupAlgebraProjectionInClass C R G
            (completedGroupAlgebraIndexToInClass G C hForm hG U))
        (by
          intro U V hUV
          funext x
          change completedGroupAlgebraTransitionInClass C R G
              (completedGroupAlgebraIndexToInClass_le
                (G := G) C hForm hG hUV)
              (completedGroupAlgebraProjectionInClass C R G
                (completedGroupAlgebraIndexToInClass G C hForm hG V) x) =
            completedGroupAlgebraProjectionInClass C R G
              (completedGroupAlgebraIndexToInClass G C hForm hG U) x
          exact completedGroupAlgebraProjectionInClass_compatible
            (R := R) (G := G) C
            (completedGroupAlgebraIndexToInClass_le
              (G := G) C hForm hG hUV) x) x)

For a pro-\(C\) group, the \(C\)-indexed inverse limit maps back to the ordinary all-finite completed group algebra by reading the same open-normal quotient stages.

Theorem CompletedGroupAlgebra.completedGroupAlgebraFromInClass_projection

@[simp]
theorem completedGroupAlgebraFromInClass_projection
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (U :
        CompletedGroupAlgebraIndex G)
    (x : CompletedGroupAlgebraInClass C R G) :
    completedGroupAlgebraProjection R G U
        (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x) =
      completedGroupAlgebraProjectionInClass C R G
        (completedGroupAlgebraIndexToInClass G C hForm hG U) x

Projecting the comparison map \(\widehat{R[G]}_{C}\to\widehat{R[G]}\) to an all-finite stage recovers the matching \(C\)-indexed projection.

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraFromInClassRingHom

def completedGroupAlgebraFromInClassRingHom
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    CompletedGroupAlgebraInClass C R G →+* CompletedGroupAlgebraCarrier R G where
  toFun := completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG
  map_zero' := by
    apply completedGroupAlgebra_ext (R := R) (G := G)
    intro U
    change completedGroupAlgebraProjection R G U
        (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG 0) =
      completedGroupAlgebraProjection R G U (0 : CompletedGroupAlgebraCarrier R G)
    rw [completedGroupAlgebraFromInClass_projection]
    exact map_zero (completedGroupAlgebraProjectionInClass C R G
      (completedGroupAlgebraIndexToInClass G C hForm hG U))
  map_one' := by
    apply completedGroupAlgebra_ext (R := R) (G := G)
    intro U
    change completedGroupAlgebraProjection R G U
        (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG 1) =
      completedGroupAlgebraProjection R G U (1 : CompletedGroupAlgebraCarrier R G)
    rw [completedGroupAlgebraFromInClass_projection]
    exact map_one (completedGroupAlgebraProjectionInClass C R G
      (completedGroupAlgebraIndexToInClass G C hForm hG U))
  map_add' x y := by
    apply completedGroupAlgebra_ext (R := R) (G := G)
    intro U
    change completedGroupAlgebraProjection R G U
        (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG (x + y)) =
      completedGroupAlgebraProjection R G U
        (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x +
          completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG y)
    rw [completedGroupAlgebraFromInClass_projection]
    exact map_add (completedGroupAlgebraProjectionInClass C R G
      (completedGroupAlgebraIndexToInClass G C hForm hG U)) x y
  map_mul' x y := by
    apply completedGroupAlgebra_ext (R := R) (G := G)
    intro U
    change completedGroupAlgebraProjection R G U
        (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG (x * y)) =
      completedGroupAlgebraProjection R G U
        (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x *
          completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG y)
    rw [completedGroupAlgebraFromInClass_projection]
    exact map_mul (completedGroupAlgebraProjectionInClass C R G
      (completedGroupAlgebraIndexToInClass G C hForm hG U)) x y

The ring-homomorphism form of the comparison map is the bundled ring map determined by the underlying coordinate formula for the completed group algebra.

Theorem CompletedGroupAlgebra.completedGroupAlgebraFromInClassRingHom_apply

@[simp]
theorem completedGroupAlgebraFromInClassRingHom_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :
        CompletedGroupAlgebraInClass C R G) :
    completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG x =
      completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x

The comparison map from the \(C\)-indexed completed group algebra to the all-finite model is evaluated by reading the corresponding finite-stage coordinate.

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraFromInClassAlgHom

def completedGroupAlgebraFromInClassAlgHom
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    CompletedGroupAlgebraInClass C R G →ₐ[R] CompletedGroupAlgebraCarrier R G where
  toRingHom := completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG
  commutes' := by
    intro r
    apply completedGroupAlgebra_ext (R := R) (G := G)
    intro U
    change completedGroupAlgebraProjection R G U
        (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG
          (algebraMap R (CompletedGroupAlgebraInClass C R G) r)) =
      completedGroupAlgebraProjection R G U (algebraMap R (CompletedGroupAlgebraCarrier R G) r)
    rw [completedGroupAlgebraFromInClass_projection]
    change completedGroupAlgebraProjectionInClass C R G
        (completedGroupAlgebraIndexToInClass G C hForm hG U)
        (algebraMap R (CompletedGroupAlgebraInClass C R G) r) =
      algebraMap R (CompletedGroupAlgebraStage R G U) r
    exact completedGroupAlgebraProjectionInClass_algebraMap (R := R) (G := G) C
      (completedGroupAlgebraIndexToInClass G C hForm hG U) r

The algebra homomorphism form of the comparison map is the bundled algebra map determined by the underlying coordinate formula for the completed group algebra.

Theorem CompletedGroupAlgebra.completedGroupAlgebraFromInClassAlgHom_apply

@[simp]
theorem completedGroupAlgebraFromInClassAlgHom_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :
        CompletedGroupAlgebraInClass C R G) :
    completedGroupAlgebraFromInClassAlgHom (R := R) (G := G) C hForm hG x =
      completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x

The comparison map from the \(C\)-indexed completed group algebra to the all-finite model is evaluated by reading the corresponding finite-stage coordinate.

Show Lean proof

Theorem CompletedGroupAlgebra.continuous_completedGroupAlgebraFromInClass

theorem continuous_completedGroupAlgebraFromInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    Continuous (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG)

The comparison map from the \(C\)-indexed completed group algebra to the all-finite completed group algebra is continuous for the inverse-limit topology.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraFromInClass_toInClass

@[simp]
theorem completedGroupAlgebraFromInClass_toInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :
        CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG
        (completedGroupAlgebraToInClass (R := R) (G := G) C x) = x

The composite from a \(C\)-indexed completion to the all-finite completion and back is the identity on the \(C\)-indexed completion.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraToInClass_fromInClass

@[simp]
theorem completedGroupAlgebraToInClass_fromInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :
        CompletedGroupAlgebraInClass C R G) :
    completedGroupAlgebraToInClass (R := R) (G := G) C
        (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x) = x

The composite from the all-finite completion to the \(C\)-indexed completion and back is the identity on the all-finite completion.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraFromInClassRingHom_comp_toInClassRingHom

@[simp]
theorem completedGroupAlgebraFromInClassRingHom_comp_toInClassRingHom
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG).comp
        (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C ) =
      RingHom.id (CompletedGroupAlgebraCarrier R G)

The two comparison ring homomorphisms are inverse to one another after composition.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraToInClassRingHom_comp_fromInClassRingHom

@[simp]
theorem completedGroupAlgebraToInClassRingHom_comp_fromInClassRingHom
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C ).comp
        (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG) =
      RingHom.id (CompletedGroupAlgebraInClass C R G)

The two comparison ring homomorphisms are inverse to one another after composition.

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraInClassRingEquiv

def completedGroupAlgebraInClassRingEquiv
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    CompletedGroupAlgebraCarrier R G ≃+* CompletedGroupAlgebraInClass C R G where
  toFun := completedGroupAlgebraToInClass (R := R) (G := G) C
  invFun := completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG
  left_inv := by
    intro x
    exact completedGroupAlgebraFromInClass_toInClass (R := R) (G := G) C hForm hG x
  right_inv := by
    intro x
    exact completedGroupAlgebraToInClass_fromInClass (R := R) (G := G) C hForm hG x
  map_mul' := by
    intro x y
    exact map_mul (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C ) x y
  map_add' := by
    intro x y
    exact map_add (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C ) x y

For a pro-\(C\) group, the all-finite and \(C\)-indexed completed group algebras are the same ring, via the comparison maps.

Theorem CompletedGroupAlgebra.completedGroupAlgebraInClassRingEquiv_apply

@[simp]
theorem completedGroupAlgebraInClassRingEquiv_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :
        CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hForm hG x =
      completedGroupAlgebraToInClass (R := R) (G := G) C x

The comparison equivalence is evaluated by the underlying all-finite or \(C\)-indexed comparison map.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraInClassRingEquiv_symm_apply

@[simp]
theorem completedGroupAlgebraInClassRingEquiv_symm_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :
        CompletedGroupAlgebraInClass C R G) :
    (completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hForm hG).symm x =
      completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x

The comparison equivalence is evaluated by the underlying all-finite or \(C\)-indexed comparison map.

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraInClassAlgEquiv

def completedGroupAlgebraInClassAlgEquiv
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    CompletedGroupAlgebraCarrier R G ≃ₐ[R] CompletedGroupAlgebraInClass C R G :=
  AlgEquiv.ofRingEquiv (f := completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hForm hG)
    (by
      intro r
      rfl)

For a pro-\(C\) group, the all-finite and \(C\)-indexed completed group algebras are the same \(R\)-algebra.

Theorem CompletedGroupAlgebra.completedGroupAlgebraInClassAlgEquiv_apply

@[simp]
theorem completedGroupAlgebraInClassAlgEquiv_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :
        CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraInClassAlgEquiv (R := R) (G := G) C hForm hG x =
      completedGroupAlgebraToInClass (R := R) (G := G) C x

The comparison equivalence is evaluated by the underlying all-finite or \(C\)-indexed comparison map.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraInClassAlgEquiv_symm_apply

@[simp]
theorem completedGroupAlgebraInClassAlgEquiv_symm_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :
        CompletedGroupAlgebraInClass C R G) :
    (completedGroupAlgebraInClassAlgEquiv (R := R) (G := G) C hForm hG).symm x =
      completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x

The comparison equivalence is evaluated by the underlying all-finite or \(C\)-indexed comparison map.

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraInClassHomeomorph

def completedGroupAlgebraInClassHomeomorph
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    CompletedGroupAlgebraCarrier R G ≃ₜ CompletedGroupAlgebraInClass C R G where
  toEquiv := (completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hForm hG).toEquiv
  continuous_toFun := continuous_completedGroupAlgebraToInClass (R := R) (G := G) C
  continuous_invFun := continuous_completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG

The comparison equivalence is an equivalence of topological spaces.

Theorem CompletedGroupAlgebra.completedGroupAlgebraInClassHomeomorph_apply

@[simp]
theorem completedGroupAlgebraInClassHomeomorph_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :
        CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraInClassHomeomorph (R := R) (G := G) C hForm hG x =
      completedGroupAlgebraToInClass (R := R) (G := G) C x

The comparison homeomorphism is evaluated by the underlying all-finite or \(C\)-indexed comparison map.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraInClassHomeomorph_symm_apply

@[simp]
theorem completedGroupAlgebraInClassHomeomorph_symm_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :
        CompletedGroupAlgebraInClass C R G) :
    (completedGroupAlgebraInClassHomeomorph (R := R) (G := G) C hForm hG).symm x =
      completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x

The comparison homeomorphism is evaluated by the underlying all-finite or \(C\)-indexed comparison map.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraToInClass_surjective

theorem completedGroupAlgebraToInClass_surjective
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    Function.Surjective (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C )

Surjectivity of the induced map is obtained from surjectivity on the underlying quotient or dense algebraic model, together with closedness of the image in the completed target.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraFromInClass_surjective

theorem completedGroupAlgebraFromInClass_surjective
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    Function.Surjective (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG)

Surjectivity of the induced map is obtained from surjectivity on the underlying quotient or dense algebraic model, together with closedness of the image in the completed target.

Show Lean proof

ProCGroups.CompletedGroupAlgebra.Basic.ClassComparison

Declarations