Module

StageMaps.lean

Nyll.ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.StageMaps

9 declarations indexed from sourceView source ↗

Module documentation

Functorial maps at in-class finite stages

This file constructs the finite-stage group-algebra map induced by a continuous group homomorphism. It proves formulas on basis elements and scalars and compatibility with coefficient change, transitions, and the completed map.

Imports2

Imported by2

def

completedGroupAlgebraFunctorialStageMapInClass

L38 ↗

CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMapInClass

Documentation

The \(C\)-indexed finite-stage map \(R[G/\varphi^{-1}(V)]\to R[H/V]\) is induced by a continuous homomorphism \(\varphi : G \to H\).

Source context 10 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
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 completedGroupAlgebraFunctorialStageMapInClass
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (R : Type u) [CommRing R] (φ : G →* H) (hφ : Continuous φ)
    (V : CompletedGroupAlgebraIndexInClass H C) :
    CompletedGroupAlgebraStageInClass C R G
        (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) →+*
      CompletedGroupAlgebraStageInClass C R H V

theorem

completedGroupAlgebraFunctorialStageMapInClass_surjective_of_surjective

L50 ↗

CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMapInClass_surjective_of_surjective

Documentation

A surjective group homomorphism induces a surjective finite-stage group-algebra 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
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 completedGroupAlgebraFunctorialStageMapInClass_surjective_of_surjective
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (hφsurj : Function.Surjective φ)
    (V : CompletedGroupAlgebraIndexInClass H C) :
    Function.Surjective
      (completedGroupAlgebraFunctorialStageMapInClass
        (G := G) (H := H) C hHer (R := R) φ hφ V)

theorem

completedGroupAlgebraFunctorialStageMapInClass_single

L69 ↗

CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMapInClass_single

Documentation

The functorial finite-stage map sends singleton coefficients to singleton coefficients.

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
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 completedGroupAlgebraFunctorialStageMapInClass_single
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C)
    (q : CompletedGroupAlgebraQuotientInClass G C
      (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)) (r : R) :
    completedGroupAlgebraFunctorialStageMapInClass
        (G := G) (H := H) C hHer (R := R) φ hφ V (MonoidAlgebra.single q r) =
      MonoidAlgebra.single
        (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H)
          C hHer φ hφ V q) r

theorem

completedGroupAlgebraFunctorialStageMapInClass_algebraMap

L91 ↗

CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMapInClass_algebraMap

Documentation

The functorial finite-stage map preserves coefficient algebra-map elements.

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
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 completedGroupAlgebraFunctorialStageMapInClass_algebraMap
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) (r : R) :
    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

theorem

completedGroupAlgebraStageCoeffMapInClass_comp_functorialStageMapInClass

L114 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageCoeffMapInClass_comp_functorialStageMapInClass

Documentation

Functorial finite-stage maps commute with coefficient change.

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
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 completedGroupAlgebraStageCoeffMapInClass_comp_functorialStageMapInClass
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (S : Type w) [CommRing S] (f : R →+* S)
    (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
    (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := H) C S f V).comp
        (completedGroupAlgebraFunctorialStageMapInClass
          (G := G) (H := H) C hHer (R := R) φ hφ V) =
      (completedGroupAlgebraFunctorialStageMapInClass
          (G := G) (H := H) C hHer (R := S) φ hφ V).comp
        (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f
          (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V))

theorem

continuous_completedGroupAlgebraFunctorialStageMapInClass

L131 ↗

CompletedGroupAlgebra.continuous_completedGroupAlgebraFunctorialStageMapInClass

Documentation

The functorial finite-stage group-algebra map is continuous for the finite-stage topologies.

Source context 10 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
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_completedGroupAlgebraFunctorialStageMapInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
    letI : TopologicalSpace
        (CompletedGroupAlgebraStageInClass C R G
          (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)) :=
      (completedGroupAlgebraSystemInClass C R G).topologicalSpace
        (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)
    letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R H V) :=
      (completedGroupAlgebraSystemInClass C R H).topologicalSpace V
    Continuous (completedGroupAlgebraFunctorialStageMapInClass
      (G := G) (H := H) C hHer (R := R) φ hφ V) := by
  let : Finite (CompletedGroupAlgebraQuotientInClass G C
      (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)) :=
    finite_completedGroupAlgebraQuotientInClass G C
      (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)
  let : Finite (CompletedGroupAlgebraQuotientInClass H C V) :=
    finite_completedGroupAlgebraQuotientInClass H C V
  let : TopologicalSpace
      (CompletedGroupAlgebraStageInClass C R G
        (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)) :=
    (completedGroupAlgebraSystemInClass C R G).topologicalSpace
      (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)
  let : TopologicalSpace (CompletedGroupAlgebraStageInClass C R H V) :=
    (completedGroupAlgebraSystemInClass C R H).topologicalSpace V
  exact finiteGroupAlgebra_mapDomainRingHom_continuous R
    (CompletedGroupAlgebraQuotientInClass G C
      (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V))
    (CompletedGroupAlgebraQuotientInClass H C V)
    (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hHer φ hφ V)

theorem

completedGroupAlgebraFunctorialStageMapInClass_transition

L166 ↗

CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMapInClass_transition

Documentation

Functorial finite-stage maps commute with transition maps.

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
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 completedGroupAlgebraFunctorialStageMapInClass_transition
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ)
    {V W : CompletedGroupAlgebraIndexInClass H C} (hVW : V ≤ W) :
    (completedGroupAlgebraTransitionInClass C R H hVW).comp
        (completedGroupAlgebraFunctorialStageMapInClass
          (G := G) (H := H) C hHer (R := R) φ hφ W) =
      (completedGroupAlgebraFunctorialStageMapInClass
          (G := G) (H := H) C hHer (R := R) φ hφ V).comp
        (completedGroupAlgebraTransitionInClass C R G
          (completedGroupAlgebraComapIndexInClass_mono
            (G := G) (H := H) C hHer φ hφ hVW))

theorem

completedGAStageCoeffMapInClass_comp_transition_comp_functorialStageMapInClass

L206 ↗

CompletedGroupAlgebra.completedGAStageCoeffMapInClass_comp_transition_comp_functorialStageMapInClass

Documentation

Functorial finite-stage maps commute with a group transition followed by coefficient change.

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
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 completedGAStageCoeffMapInClass_comp_transition_comp_functorialStageMapInClass
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (S : Type w) [CommRing S] (f : R →+* S)
    (φ : G →* H) (hφ : Continuous φ)
    {V W : CompletedGroupAlgebraIndexInClass H C} (hVW : V ≤ W) :
    ((completedGroupAlgebraStageCoeffMapInClass (R := R) (G := H) C S f V).comp
        (completedGroupAlgebraTransitionInClass C R H hVW)).comp
        (completedGroupAlgebraFunctorialStageMapInClass
          (G := G) (H := H) C hHer (R := R) φ hφ W) =
      (completedGroupAlgebraFunctorialStageMapInClass
          (G := G) (H := H) C hHer (R := S) φ hφ V).comp
        ((completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f
          (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)).comp
          (completedGroupAlgebraTransitionInClass C R G
            (completedGroupAlgebraComapIndexInClass_mono
              (G := G) (H := H) C hHer φ hφ hVW)))

theorem

completedGroupAlgebraFunctorialStageMapInClass_comp_stageMap

L233 ↗

CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMapInClass_comp_stageMap

Documentation

The functorial finite-stage map agrees with the stage map after passing to the comap quotient.

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
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 completedGroupAlgebraFunctorialStageMapInClass_comp_stageMap
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
    (completedGroupAlgebraFunctorialStageMapInClass
        (G := G) (H := H) C hHer (R := R) φ hφ V).comp
        (completedGroupAlgebraStageMapInClass C R G
          (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)) =
      (completedGroupAlgebraStageMapInClass C R H V).comp
        (MonoidAlgebra.mapDomainRingHom R φ)

Module documentation

Functorial maps at in-class finite stages

Declarations