ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.FiniteQuotients

25 Theorems | 7 Definitions | 1 Abbreviation

This file constructs the finite group-algebra stages obtained by quotienting both coefficients and the group. It develops their quotient maps, kernels, transition maps, basis formulas, continuity, and surjectivity.

import

ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.CanonicalMaps

Imported by

ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteQuotients

Theorem CompletedGroupAlgebra.continuous_idealQuotient_mk_openIdeal_discrete

theorem continuous_idealQuotient_mk_openIdeal_discrete
    (I : Ideal R) (hI : IsOpen (I : Set R)) :
    letI : TopologicalSpace (R ⧸ I) := ⊥
    Continuous (Ideal.Quotient.mk I)

An open coefficient ideal gives a continuous quotient map when the quotient is equipped with the discrete topology. This is the coefficient-side continuity used in Ribes--Zalesskii Section \(5.3\).

Show Lean proof

Theorem CompletedGroupAlgebra.finiteGroupAlgebra_mapRangeRingHom_continuous

omit G [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [IsTopologicalRing R] in
theorem finiteGroupAlgebra_mapRangeRingHom_continuous
    (S : Type u) [CommRing S] [TopologicalSpace S]
    (Q : Type v) [Group Q] [Finite Q]
    (f : R →+* S) (hf : Continuous f) :
    letI : TopologicalSpace (MonoidAlgebra R Q) := finiteGroupAlgebraTopology R Q
    letI : TopologicalSpace (MonoidAlgebra S Q) := finiteGroupAlgebraTopology S Q
    Continuous (MonoidAlgebra.mapRingHom Q f :
      MonoidAlgebra R Q → MonoidAlgebra S Q)

Finite-stage group algebras are functorial in the coefficient ring by continuous maps.

Show Lean proof

Theorem CompletedGroupAlgebra.finiteGroupAlgebraTopology_discrete_of_discrete_coeff

omit R G [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G] in
theorem finiteGroupAlgebraTopology_discrete_of_discrete_coeff
    (S : Type u) [CommRing S] [TopologicalSpace S] [DiscreteTopology S]
    (Q : Type v) [Finite Q] :
    letI : TopologicalSpace (MonoidAlgebra S Q) := finiteGroupAlgebraTopology S Q
    DiscreteTopology (MonoidAlgebra S Q)

If the coefficient ring is discrete, then the finite-stage group algebra has the discrete finite-product topology.

Show Lean proof

Abbreviation CompletedGroupAlgebra.CompletedGroupAlgebraCoeffQuotientStage

omit [TopologicalSpace R] [IsTopologicalRing R] in
abbrev CompletedGroupAlgebraCoeffQuotientStage
    (R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
    Type (max u v) :=
  MonoidAlgebra (R ⧸ I) (CompletedGroupAlgebraQuotient G U)

The Ribes--Zalesskii Section \(5.3\) finite quotient \((R/I)[G/U]\) applies both the coefficient quotient and the group quotient and is used in the kernel-neighborhood topology.

Definition CompletedGroupAlgebra.completedGroupAlgebraStageCoeffQuotientMap

omit [TopologicalSpace R] [IsTopologicalRing R] in
def completedGroupAlgebraStageCoeffQuotientMap
    (R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G]
    (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
    CompletedGroupAlgebraStage R G U →+*
      CompletedGroupAlgebraCoeffQuotientStage R G I U :=
  MonoidAlgebra.mapRingHom (CompletedGroupAlgebraQuotient G U)
    (Ideal.Quotient.mk I)

The coefficient quotient map \(R[G/U]\) \(\to\) \((R/I)[G/U]\).

Theorem CompletedGroupAlgebra.completedGroupAlgebraStageCoeffQuotientMap_single

omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem completedGroupAlgebraStageCoeffQuotientMap_single
    (I : Ideal R) (U : CompletedGroupAlgebraIndex G)
    (q : CompletedGroupAlgebraQuotient G U) (r : R) :
    completedGroupAlgebraStageCoeffQuotientMap R G I U (MonoidAlgebra.single q r) =
      MonoidAlgebra.single q (Ideal.Quotient.mk I r)

The coefficient-quotient map sends a singleton supported at a finite quotient class to the corresponding singleton with transformed coefficient and unchanged quotient support.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraStageCoeffQuotientMap_surjective

omit [TopologicalSpace R] [IsTopologicalRing R] in
theorem completedGroupAlgebraStageCoeffQuotientMap_surjective
    (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
    Function.Surjective (completedGroupAlgebraStageCoeffQuotientMap R G I U)

The finite-stage coefficient-quotient map is surjective; every target singleton is lifted by keeping the quotient support and lifting the coefficient.

Show Lean proof

Definition CompletedGroupAlgebra.groupAlgebraFiniteQuotientMap

omit [TopologicalSpace R] [IsTopologicalRing R] in
def groupAlgebraFiniteQuotientMap
    (R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G]
    (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
    MonoidAlgebra R G →+* CompletedGroupAlgebraCoeffQuotientStage R G I U :=
  (completedGroupAlgebraStageCoeffQuotientMap R G I U).comp
    (completedGroupAlgebraStageMap R G U)

The finite-quotient map \(R[G]\to (R/I)[G/U]\) used in Ribes--Zalesskii Section \(5.3\).

Theorem CompletedGroupAlgebra.groupAlgebraFiniteQuotientMap_single

omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem groupAlgebraFiniteQuotientMap_single
    (I : Ideal R) (U : CompletedGroupAlgebraIndex G) (g : G) (r : R) :
    groupAlgebraFiniteQuotientMap R G I U (MonoidAlgebra.single g r) =
      MonoidAlgebra.single
        (openNormalSubgroupInClassProj
          (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g)
        (Ideal.Quotient.mk I r)

The finite quotient map on a group algebra sends a singleton \(r[g]\) to the singleton \(\bar r[\bar g]\) in \((R/I)[G/U]\).

Show Lean proof

Theorem CompletedGroupAlgebra.groupAlgebraFiniteQuotientMap_of

omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem groupAlgebraFiniteQuotientMap_of
    (I : Ideal R) (U : CompletedGroupAlgebraIndex G) (g : G) :
    groupAlgebraFiniteQuotientMap R G I U (MonoidAlgebra.of R G g) =
      MonoidAlgebra.of (R ⧸ I) (CompletedGroupAlgebraQuotient G U)
        (openNormalSubgroupInClassProj
          (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g)

The finite quotient group-algebra map is computed by choosing representatives and applying the quotient map to supports.

Show Lean proof

Theorem CompletedGroupAlgebra.groupAlgebraFiniteQuotientMap_eq_mapDomain_comp_mapRange

omit [TopologicalSpace R] [IsTopologicalRing R] in
theorem groupAlgebraFiniteQuotientMap_eq_mapDomain_comp_mapRange
    (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
    groupAlgebraFiniteQuotientMap R G I U =
      (MonoidAlgebra.mapDomainRingHom (R ⧸ I)
          (openNormalSubgroupInClassProj
            (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U)).comp
        (MonoidAlgebra.mapRingHom G (Ideal.Quotient.mk I))

The quotient map \(R[G] \to (R/I)[G/U]\) factors equally as coefficient quotient followed by group quotient, or group quotient followed by coefficient quotient.

Show Lean proof

Theorem CompletedGroupAlgebra.groupAlgebraFiniteQuotientMap_surjective

omit [TopologicalSpace R] [IsTopologicalRing R] in
theorem groupAlgebraFiniteQuotientMap_surjective
    (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
    Function.Surjective (groupAlgebraFiniteQuotientMap R G I U)

The finite quotient map on group algebras is surjective, expressing functoriality after passage to finite quotient stages.

Show Lean proof

Definition CompletedGroupAlgebra.groupAlgebraFiniteQuotientKernel

omit [TopologicalSpace R] [IsTopologicalRing R] in
def groupAlgebraFiniteQuotientKernel
    (R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G]
    (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
    Ideal (MonoidAlgebra R G) :=
  RingHom.ker (groupAlgebraFiniteQuotientMap R G I U)

The kernels used in Ribes--Zalesskii's natural topology on \(R[G]\); for the kernel-neighborhood topology this family is restricted to open ideals \(I\) and open normal subgroups \(U\).

Theorem CompletedGroupAlgebra.mem_groupAlgebraFiniteQuotientKernel_iff

omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem mem_groupAlgebraFiniteQuotientKernel_iff
    {R : Type u} {G : Type v} [CommRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G]
    {I : Ideal R} {U : CompletedGroupAlgebraIndex G} {x : MonoidAlgebra R G} :
    x ∈ groupAlgebraFiniteQuotientKernel R G I U ↔
      groupAlgebraFiniteQuotientMap R G I U x = 0

An element of \(R[G]\) lies in groupAlgebraFiniteQuotientKernel exactly when its image in \((R/I)[G/U]\) is zero.

Show Lean proof

Theorem CompletedGroupAlgebra.groupAlgebraFiniteQuotientKernel_eq_comap

omit [TopologicalSpace R] [IsTopologicalRing R] in
theorem groupAlgebraFiniteQuotientKernel_eq_comap
    (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
    groupAlgebraFiniteQuotientKernel R G I U =
      Ideal.comap (completedGroupAlgebraStageMap R G U)
        (RingHom.ker (completedGroupAlgebraStageCoeffQuotientMap R G I U))

The kernel of the finite quotient group-algebra map is the comap of the corresponding quotient-kernel data.

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraCoeffQuotientTransition

omit [TopologicalSpace R] [IsTopologicalRing R] in
def completedGroupAlgebraCoeffQuotientTransition
    (R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] {I J : Ideal R} (hIJ : I ≤ J)
    (U : CompletedGroupAlgebraIndex G) :
    CompletedGroupAlgebraCoeffQuotientStage R G I U →+*
      CompletedGroupAlgebraCoeffQuotientStage R G J U :=
  MonoidAlgebra.mapRingHom (CompletedGroupAlgebraQuotient G U)
    (Ideal.Quotient.factor hIJ)

Coefficient transition \((R/I)[G/U]\) \(\to\) \((R/J)[G/U]\) induced by an inclusion \(I\le J\).

Theorem CompletedGroupAlgebra.completedGroupAlgebraCoeffQuotientTransition_single

omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem completedGroupAlgebraCoeffQuotientTransition_single
    {I J : Ideal R} (hIJ : I ≤ J) (U : CompletedGroupAlgebraIndex G)
    (q : CompletedGroupAlgebraQuotient G U) (r : R ⧸ I) :
    completedGroupAlgebraCoeffQuotientTransition R G hIJ U (MonoidAlgebra.single q r) =
      MonoidAlgebra.single q (Ideal.Quotient.factor hIJ r)

The coefficient transition from \(R/I\) to \(R/J\) fixes the support \(q\) and applies Ideal.Quotient.factor to the singleton coefficient.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraCoeffQuotientTransition_comp_stageCoeffQuotientMap

omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem completedGroupAlgebraCoeffQuotientTransition_comp_stageCoeffQuotientMap
    {I J : Ideal R} (hIJ : I ≤ J) (U : CompletedGroupAlgebraIndex G) :
    (completedGroupAlgebraCoeffQuotientTransition R G hIJ U).comp
        (completedGroupAlgebraStageCoeffQuotientMap R G I U) =
      completedGroupAlgebraStageCoeffQuotientMap R G J U

Applying the coefficient transition after reduction modulo \(I\) agrees with reducing the stage coefficients directly modulo \(J\).

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraCoeffQuotientTransition_surjective

omit [TopologicalSpace R] [IsTopologicalRing R] in
theorem completedGroupAlgebraCoeffQuotientTransition_surjective
    {I J : Ideal R} (hIJ : I ≤ J) (U : CompletedGroupAlgebraIndex G) :
    Function.Surjective (completedGroupAlgebraCoeffQuotientTransition R G hIJ U)

At a fixed quotient stage \(U\), the coefficient transition induced by \(I\leq J\) is surjective.

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraCoeffQuotientGroupTransition

omit [TopologicalSpace R] [IsTopologicalRing R] in
def completedGroupAlgebraCoeffQuotientGroupTransition
    (R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] (I : Ideal R) {U V : CompletedGroupAlgebraIndex G}
    (hUV : U ≤ V) :
    CompletedGroupAlgebraCoeffQuotientStage R G I V →+*
      CompletedGroupAlgebraCoeffQuotientStage R G I U :=
  MonoidAlgebra.mapDomainRingHom (R ⧸ I)
    (OpenNormalSubgroupInClass.map
      (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
      (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)

Group-quotient transition \((R/I)[G/V]\) \(\to\) \((R/I)[G/U]\) induced by \(U\le V\).

Theorem CompletedGroupAlgebra.completedGroupAlgebraCoeffQuotientGroupTransition_single

omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem completedGroupAlgebraCoeffQuotientGroupTransition_single
    (I : Ideal R) {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
    (q : CompletedGroupAlgebraQuotient G V) (r : R ⧸ I) :
    completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV
        (MonoidAlgebra.single q r) =
      MonoidAlgebra.single
        ((OpenNormalSubgroupInClass.map
          (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
          (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) r

The group-quotient transition from \(G/V\) to \(G/U\) sends a singleton to the singleton at the induced quotient image and leaves its \(R/I\)-coefficient unchanged.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraCoeffQuotientGroupTransition_comp_stageCoeffQuotientMap

omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem completedGroupAlgebraCoeffQuotientGroupTransition_comp_stageCoeffQuotientMap
    (I : Ideal R) {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    (completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV).comp
        (completedGroupAlgebraStageCoeffQuotientMap R G I V) =
      (completedGroupAlgebraStageCoeffQuotientMap R G I U).comp
        (completedGroupAlgebraTransition R G hUV)

Changing the group quotient after reducing coefficients modulo \(I\) agrees with first applying the group-stage transition and then reducing coefficients.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraQuotientTransition_surjective

omit [TopologicalSpace R] [IsTopologicalRing R] [IsTopologicalGroup G] in
theorem completedGroupAlgebraQuotientTransition_surjective
    {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    Function.Surjective
      (OpenNormalSubgroupInClass.map
        (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
        (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)

The canonical quotient homomorphism \(G/V\to G/U\) induced by \(U\leq V\) is surjective.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraCoeffQuotientGroupTransition_surjective

omit [TopologicalSpace R] [IsTopologicalRing R] in
theorem completedGroupAlgebraCoeffQuotientGroupTransition_surjective
    (I : Ideal R) {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    Function.Surjective (completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV)

The group-quotient transition \((R/I)[G/V]\to(R/I)[G/U]\) is surjective.

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraFiniteQuotientTransition

omit [TopologicalSpace R] [IsTopologicalRing R] in
def completedGroupAlgebraFiniteQuotientTransition
    (R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] {I J : Ideal R} (hIJ : I ≤ J)
    {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    CompletedGroupAlgebraCoeffQuotientStage R G I V →+*
      CompletedGroupAlgebraCoeffQuotientStage R G J U :=
  (completedGroupAlgebraCoeffQuotientTransition R G hIJ U).comp
    (completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV)

The combined transition (R/I)[G/V] -> (R/J)[G/U].

Theorem CompletedGroupAlgebra.completedGroupAlgebraFiniteQuotientTransition_single

omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem completedGroupAlgebraFiniteQuotientTransition_single
    {I J : Ideal R} (hIJ : I ≤ J) {U V : CompletedGroupAlgebraIndex G}
    (hUV : U ≤ V) (q : CompletedGroupAlgebraQuotient G V) (r : R ⧸ I) :
    completedGroupAlgebraFiniteQuotientTransition R G hIJ hUV
        (MonoidAlgebra.single q r) =
      MonoidAlgebra.single
        ((OpenNormalSubgroupInClass.map
          (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
          (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q)
        (Ideal.Quotient.factor hIJ r)

The combined finite-quotient transition sends a singleton by transporting its support from \(G/V\) to \(G/U\) and its coefficient from \(R/I\) to \(R/J\).

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraCoeffQuotientGroupTransition_comp_finiteQuotientMap

omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem completedGroupAlgebraCoeffQuotientGroupTransition_comp_finiteQuotientMap
    (I : Ideal R) {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    (completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV).comp
        (groupAlgebraFiniteQuotientMap R G I V) =
      groupAlgebraFiniteQuotientMap R G I U

At fixed coefficient quotient \(R/I\), applying the group-quotient transition after the abstract finite-quotient map at \(V\) gives the finite-quotient map at \(U\).

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraFiniteQuotientTransition_comp_finiteQuotientMap

omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem completedGroupAlgebraFiniteQuotientTransition_comp_finiteQuotientMap
    {I J : Ideal R} (hIJ : I ≤ J) {U V : CompletedGroupAlgebraIndex G}
    (hUV : U ≤ V) :
    (completedGroupAlgebraFiniteQuotientTransition R G hIJ hUV).comp
        (groupAlgebraFiniteQuotientMap R G I V) =
      groupAlgebraFiniteQuotientMap R G J U

The combined transition from \((R/I)[G/V]\) to \((R/J)[G/U]\), composed with the source finite-quotient map, is the target finite-quotient map.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraFiniteQuotientTransition_surjective

omit [TopologicalSpace R] [IsTopologicalRing R] in
theorem completedGroupAlgebraFiniteQuotientTransition_surjective
    {I J : Ideal R} (hIJ : I ≤ J) {U V : CompletedGroupAlgebraIndex G}
    (hUV : U ≤ V) :
    Function.Surjective (completedGroupAlgebraFiniteQuotientTransition R G hIJ hUV)

The combined coefficient-and-group transition \((R/I)[G/V]\to(R/J)[G/U]\) is surjective.

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraFiniteQuotientProjection

def completedGroupAlgebraFiniteQuotientProjection
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
    [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
    CompletedGroupAlgebraCarrier R G →+*
      CompletedGroupAlgebraCoeffQuotientStage R G I U :=
  (completedGroupAlgebraStageCoeffQuotientMap R G I U).comp
    (completedGroupAlgebraProjection R G U)

The corresponding projection from the completed group algebra to \((R/I)[G/U]\).

Theorem CompletedGroupAlgebra.completedGroupAlgebraFiniteQuotientProjection_toCompletedGroupAlgebra

@[simp]
theorem completedGroupAlgebraFiniteQuotientProjection_toCompletedGroupAlgebra
    (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
    (completedGroupAlgebraFiniteQuotientProjection R G I U).comp
        (toCompletedGroupAlgebraRingHom R G) =
      groupAlgebraFiniteQuotientMap R G I U

Composing the finite-quotient projection from the completed group algebra with its canonical dense ring homomorphism gives groupAlgebraFiniteQuotientMap.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraFiniteQuotientProjection_apply_toCompletedGroupAlgebra

@[simp]
theorem completedGroupAlgebraFiniteQuotientProjection_apply_toCompletedGroupAlgebra
    (I : Ideal R) (U : CompletedGroupAlgebraIndex G) (x : MonoidAlgebra R G) :
    completedGroupAlgebraFiniteQuotientProjection R G I U
        (toCompletedGroupAlgebra R G x) =
      groupAlgebraFiniteQuotientMap R G I U x

The finite-quotient projection of the canonical dense element is computed by the associated quotient-stage map.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraFiniteQuotientTransition_comp_projection

@[simp 900]
theorem completedGroupAlgebraFiniteQuotientTransition_comp_projection
    {I J : Ideal R} (hIJ : I ≤ J) {U V : CompletedGroupAlgebraIndex G}
    (hUV : U ≤ V) :
    (completedGroupAlgebraFiniteQuotientTransition R G hIJ hUV).comp
        (completedGroupAlgebraFiniteQuotientProjection R G I V) =
      completedGroupAlgebraFiniteQuotientProjection R G J U

Projecting to \((R/I)[G/V]\) and then applying the combined transition agrees with projecting directly to \((R/J)[G/U]\).

Show Lean proof

ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.FiniteQuotients

Declarations