NYLL
Module

ComapIndex.lean

Nyll.ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.ComapIndex
7 declarations indexed from sourceView source ↗

Module documentation

Pulling back in-class quotient indices

An open-normal quotient index on the target pulls back along a continuous group homomorphism to an index on the source. This file defines that comap, the induced finite quotient map, and its monotonicity, compatibility, and surjectivity properties.

Imports1
Imported by2

Declarations

def

completedGroupAlgebraComapIndexInClass

L39 ↗
CompletedGroupAlgebra.completedGroupAlgebraComapIndexInClass
Documentation

The inverse image of a \(C\)-quotient of \(H\) along a continuous homomorphism \(G\to H\), again as a \(C\)-quotient of \(G\), when \(C\) is hereditary.

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]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
def completedGroupAlgebraComapIndexInClass
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
    CompletedGroupAlgebraIndexInClass G C
theorem

completedGroupAlgebraComapIndexInClass_subgroup

L50 ↗
CompletedGroupAlgebra.completedGroupAlgebraComapIndexInClass_subgroup
Documentation

The comap of an open normal subgroup along a continuous homomorphism is again open normal.

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
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]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup G] [IsTopologicalGroup H] in
Lean source · statement
theorem completedGroupAlgebraComapIndexInClass_subgroup
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
    (((OrderDual.ofDual (completedGroupAlgebraComapIndexInClass
        (G := G) (H := H) C hHer φ hφ V)).1 : OpenNormalSubgroup G) : Subgroup G) =
      (((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H).comap φ
theorem

completedGroupAlgebraComapIndexInClass_mono

L60 ↗
CompletedGroupAlgebra.completedGroupAlgebraComapIndexInClass_mono
Documentation

Comap indices are monotone with respect to refinement of open normal subgroups.

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
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]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup G] [IsTopologicalGroup H] in
Lean source · statement
theorem completedGroupAlgebraComapIndexInClass_mono
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ)
    {V W : CompletedGroupAlgebraIndexInClass H C} (hVW : V ≤ W) :
    completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V ≤
      completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ W
def

completedGroupAlgebraComapQuotientMapInClass

L71 ↗
CompletedGroupAlgebra.completedGroupAlgebraComapQuotientMapInClass
Documentation

The quotient homomorphism \(G/\varphi^{-1}(V) \to H/V\) for a \(C\)-indexed 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]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
def completedGroupAlgebraComapQuotientMapInClass
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
    CompletedGroupAlgebraQuotientInClass G C
        (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) →*
      CompletedGroupAlgebraQuotientInClass H C V
theorem

completedGroupAlgebraComapQuotientMapInClass_mk

L83 ↗
CompletedGroupAlgebra.completedGroupAlgebraComapQuotientMapInClass_mk
Documentation

The quotient map attached to a comap index sends a coset to the coset of its image.

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]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem completedGroupAlgebraComapQuotientMapInClass_mk
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) (g : G) :
    completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hHer φ hφ V
        (QuotientGroup.mk'
          ((((OrderDual.ofDual (completedGroupAlgebraComapIndexInClass
            (G := G) (H := H) C hHer φ hφ V)).1 : OpenNormalSubgroup G) :
              Subgroup G)) g) =
      QuotientGroup.mk' ((((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H))
        (φ g)
theorem

completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective

L98 ↗
CompletedGroupAlgebra.completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
Documentation

A surjective group homomorphism induces a surjective map on the corresponding finite quotients.

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]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem completedGroupAlgebraComapQuotientMapInClass_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
      (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hHer φ hφ V)
theorem

completedGroupAlgebraComapQuotientMapInClass_compatible

L119 ↗
CompletedGroupAlgebra.completedGroupAlgebraComapQuotientMapInClass_compatible
Documentation

The class-restricted completed group-algebra pullback quotient map is compatible with transition maps and coordinate projections for the completed group algebra.

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]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem completedGroupAlgebraComapQuotientMapInClass_compatible
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ)
    {V W : CompletedGroupAlgebraIndexInClass H C} (hVW : V ≤ W) :
    (OpenNormalSubgroupInClass.map
        (C := C) (G := H)
        (U := OrderDual.ofDual V) (V := OrderDual.ofDual W) hVW).comp
        (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hHer φ hφ W) =
      (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hHer φ hφ V).comp
        (OpenNormalSubgroupInClass.map
          (C := C) (G := G)
          (U := OrderDual.ofDual
            (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V))
          (V := OrderDual.ofDual
            (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ W))
          (completedGroupAlgebraComapIndexInClass_mono
            (G := G) (H := H) C hHer φ hφ hVW))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.