Module

FiniteQuotients.lean

Nyll.ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.FiniteQuotients

33 declarations indexed from sourceView source ↗

Module documentation

Finite coefficient-and-group quotients

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.

Imports1

Nyll.ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.CanonicalMaps

Imported by2

theorem

continuous_idealQuotient_mk_openIdeal_discrete

L39 ↗

CompletedGroupAlgebra.continuous_idealQuotient_mk_openIdeal_discrete

Documentation

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\).

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · full declaration

theorem continuous_idealQuotient_mk_openIdeal_discrete
    (I : Ideal R) (hI : IsOpen (I : Set R)) :
    letI : TopologicalSpace (R ⧸ I) := ⊥
    Continuous (Ideal.Quotient.mk I) := by
  let : TopologicalSpace (R ⧸ I) := ⊥
  have : DiscreteTopology (R ⧸ I) := ⟨rfl⟩
  rw [continuous_discrete_rng]
  intro b
  rcases Ideal.Quotient.mk_surjective (I := I) b with ⟨a, rfl⟩
  have hpre :
      (Ideal.Quotient.mk I) ⁻¹' ({Ideal.Quotient.mk I a} : Set (R ⧸ I)) =
        (fun x : R => x - a) ⁻¹' (I : Set R) := by
    ext x
    simp only [Set.mem_preimage, Set.mem_singleton_iff, Ideal.Quotient.eq, SetLike.mem_coe]
  rw [hpre]
  exact hI.preimage (continuous_id.sub continuous_const)

theorem

finiteGroupAlgebra_mapRangeRingHom_continuous

L58 ↗

CompletedGroupAlgebra.finiteGroupAlgebra_mapRangeRingHom_continuous

Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit G [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [IsTopologicalRing R] in

Lean source · full declaration

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) := by
  classical
  let : Fintype Q := Fintype.ofFinite Q
  let : TopologicalSpace (MonoidAlgebra R Q) := finiteGroupAlgebraTopology R Q
  let : TopologicalSpace (MonoidAlgebra S Q) := finiteGroupAlgebraTopology S Q
  let eS : MonoidAlgebra S Q ≃ (Q → S) :=
    MonoidAlgebra.coeffEquiv.trans Finsupp.equivFunOnFinite
  have heS : Topology.IsInducing (eS : MonoidAlgebra S Q → Q → S) :=
    Topology.IsInducing.induced eS
  have hcoordR : ∀ q : Q, Continuous fun x : MonoidAlgebra R Q => x.coeff q := by
    intro q
    exact finiteGroupAlgebra_coordinate_continuous R Q q
  rw [heS.continuous_iff]
  apply continuous_pi
  intro q
  change Continuous fun x : MonoidAlgebra R Q =>
    (MonoidAlgebra.mapRingHom Q f x : MonoidAlgebra S Q).coeff q
  change Continuous (f ∘ fun x : MonoidAlgebra R Q => x.coeff q)
  exact hf.comp (hcoordR q)

theorem

finiteGroupAlgebraTopology_discrete_of_discrete_coeff

L91 ↗

CompletedGroupAlgebra.finiteGroupAlgebraTopology_discrete_of_discrete_coeff

Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit R G [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G] in

Lean source · full declaration

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) := by
  classical
  let : Fintype Q := Fintype.ofFinite Q
  let : TopologicalSpace (MonoidAlgebra S Q) := finiteGroupAlgebraTopology S Q
  let e : MonoidAlgebra S Q ≃ (Q → S) :=
    MonoidAlgebra.coeffEquiv.trans Finsupp.equivFunOnFinite
  exact DiscreteTopology.of_continuous_injective
    (continuous_induced_dom : Continuous (e : MonoidAlgebra S Q → Q → S)) e.injective

abbrev

CompletedGroupAlgebraCoeffQuotientStage

L109 ↗

CompletedGroupAlgebra.CompletedGroupAlgebraCoeffQuotientStage

Documentation

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.

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

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)

def

completedGroupAlgebraStageCoeffQuotientMap

L117 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageCoeffQuotientMap

Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

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

theorem

completedGroupAlgebraStageCoeffQuotientMap_single

L132 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageCoeffQuotientMap_single

Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

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)

theorem

completedGroupAlgebraStageCoeffQuotientMap_surjective

L144 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageCoeffQuotientMap_surjective

Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

theorem completedGroupAlgebraStageCoeffQuotientMap_surjective
    (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
    Function.Surjective (completedGroupAlgebraStageCoeffQuotientMap R G I U)

def

groupAlgebraFiniteQuotientMap

L156 ↗

CompletedGroupAlgebra.groupAlgebraFiniteQuotientMap

Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

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

theorem

groupAlgebraFiniteQuotientMap_single

L170 ↗

CompletedGroupAlgebra.groupAlgebraFiniteQuotientMap_single

Documentation

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]\).

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

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)

theorem

groupAlgebraFiniteQuotientMap_of

L196 ↗

CompletedGroupAlgebra.groupAlgebraFiniteQuotientMap_of

Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

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)

theorem

groupAlgebraFiniteQuotientMap_eq_mapDomain_comp_mapRange

L219 ↗

CompletedGroupAlgebra.groupAlgebraFiniteQuotientMap_eq_mapDomain_comp_mapRange

Documentation

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.

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

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))

theorem

groupAlgebraFiniteQuotientMap_surjective

L246 ↗

CompletedGroupAlgebra.groupAlgebraFiniteQuotientMap_surjective

Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

theorem groupAlgebraFiniteQuotientMap_surjective
    (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
    Function.Surjective (groupAlgebraFiniteQuotientMap R G I U)

def

groupAlgebraFiniteQuotientKernel

L260 ↗

CompletedGroupAlgebra.groupAlgebraFiniteQuotientKernel

Documentation

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\).

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

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)

theorem

mem_groupAlgebraFiniteQuotientKernel_iff

L273 ↗

CompletedGroupAlgebra.mem_groupAlgebraFiniteQuotientKernel_iff

Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

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

theorem

groupAlgebraFiniteQuotientKernel_eq_comap

L286 ↗

CompletedGroupAlgebra.groupAlgebraFiniteQuotientKernel_eq_comap

Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

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))

def

completedGroupAlgebraCoeffQuotientTransition

L297 ↗

CompletedGroupAlgebra.completedGroupAlgebraCoeffQuotientTransition

Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

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

theorem

completedGroupAlgebraCoeffQuotientTransition_single

L312 ↗

CompletedGroupAlgebra.completedGroupAlgebraCoeffQuotientTransition_single

Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

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)

theorem

completedGroupAlgebraCoeffQuotientTransition_comp_stageCoeffQuotientMap

L325 ↗

CompletedGroupAlgebra.completedGroupAlgebraCoeffQuotientTransition_comp_stageCoeffQuotientMap

Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

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

theorem

completedGroupAlgebraCoeffQuotientTransition_surjective

L340 ↗

CompletedGroupAlgebra.completedGroupAlgebraCoeffQuotientTransition_surjective

Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

theorem completedGroupAlgebraCoeffQuotientTransition_surjective
    {I J : Ideal R} (hIJ : I ≤ J) (U : CompletedGroupAlgebraIndex G) :
    Function.Surjective (completedGroupAlgebraCoeffQuotientTransition R G hIJ U)

def

completedGroupAlgebraCoeffQuotientGroupTransition

L353 ↗

CompletedGroupAlgebra.completedGroupAlgebraCoeffQuotientGroupTransition

Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

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

theorem

completedGroupAlgebraCoeffQuotientGroupTransition_single

L370 ↗

CompletedGroupAlgebra.completedGroupAlgebraCoeffQuotientGroupTransition_single

Documentation

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.

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

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

theorem

completedGroupAlgebraCoeffQuotientGroupTransition_comp_stageCoeffQuotientMap

L397 ↗

CompletedGroupAlgebra.completedGroupAlgebraCoeffQuotientGroupTransition_comp_stageCoeffQuotientMap

Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

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)

theorem

completedGroupAlgebraQuotientTransition_surjective

L414 ↗

CompletedGroupAlgebra.completedGroupAlgebraQuotientTransition_surjective

Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] [IsTopologicalGroup G] in

Lean source · statement

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)

theorem

completedGroupAlgebraCoeffQuotientGroupTransition_surjective

L431 ↗

CompletedGroupAlgebra.completedGroupAlgebraCoeffQuotientGroupTransition_surjective

Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

theorem completedGroupAlgebraCoeffQuotientGroupTransition_surjective
    (I : Ideal R) {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    Function.Surjective (completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV)

def

completedGroupAlgebraFiniteQuotientTransition

L446 ↗

CompletedGroupAlgebra.completedGroupAlgebraFiniteQuotientTransition

Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

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

theorem

completedGroupAlgebraFiniteQuotientTransition_single

L461 ↗

CompletedGroupAlgebra.completedGroupAlgebraFiniteQuotientTransition_single

Documentation

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\).

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

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)

theorem

completedGroupAlgebraCoeffQuotientGroupTransition_comp_finiteQuotientMap

L489 ↗

CompletedGroupAlgebra.completedGroupAlgebraCoeffQuotientGroupTransition_comp_finiteQuotientMap

Documentation

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\).

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

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

theorem

completedGroupAlgebraFiniteQuotientTransition_comp_finiteQuotientMap

L528 ↗

CompletedGroupAlgebra.completedGroupAlgebraFiniteQuotientTransition_comp_finiteQuotientMap

Documentation

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.

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

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

theorem

completedGroupAlgebraFiniteQuotientTransition_surjective

L545 ↗

CompletedGroupAlgebra.completedGroupAlgebraFiniteQuotientTransition_surjective

Documentation

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

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R] in

Lean source · statement

theorem completedGroupAlgebraFiniteQuotientTransition_surjective
    {I J : Ideal R} (hIJ : I ≤ J) {U V : CompletedGroupAlgebraIndex G}
    (hUV : U ≤ V) :
    Function.Surjective (completedGroupAlgebraFiniteQuotientTransition R G hIJ hUV)

def

completedGroupAlgebraFiniteQuotientProjection

L559 ↗

CompletedGroupAlgebra.completedGroupAlgebraFiniteQuotientProjection

Documentation

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

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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

theorem

completedGroupAlgebraFiniteQuotientProjection_toCompletedGroupAlgebra

L573 ↗

CompletedGroupAlgebra.completedGroupAlgebraFiniteQuotientProjection_toCompletedGroupAlgebra

Documentation

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

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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

theorem

completedGroupAlgebraFiniteQuotientProjection_apply_toCompletedGroupAlgebra

L587 ↗

CompletedGroupAlgebra.completedGroupAlgebraFiniteQuotientProjection_apply_toCompletedGroupAlgebra

Documentation

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

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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

theorem

completedGroupAlgebraFiniteQuotientTransition_comp_projection

L599 ↗

CompletedGroupAlgebra.completedGroupAlgebraFiniteQuotientTransition_comp_projection

Documentation

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

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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

Module documentation

Finite coefficient-and-group quotients

Declarations