Module

Comap.lean

Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.Comap

6 declarations indexed from sourceView source ↗

Module documentation

Completed Group Algebra / All Finite Functoriality / Comap

This module constructs the inverse-image finite quotient attached to a continuous group homomorphism and the induced quotient homomorphism. It is the index-level input for all-finite functoriality and has no dependency on augmentation theory.

Imports1

Nyll.ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Index

Imported by2

def

completedGroupAlgebraComapIndex

L36 ↗

CompletedGroupAlgebra.completedGroupAlgebraComapIndex

Documentation

The inverse image of an open-finite quotient of \(H\) along a continuous homomorphism \(G\to H\), regarded as an open-finite quotient of the profinite group \(G\). This is the index-level operation underlying Lemma 5.3.5(e)'s functoriality in the group variable.

Source context 8 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe v
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def completedGroupAlgebraComapIndex
    (φ : G →* H) (hφ : Continuous φ)
    (V : CompletedGroupAlgebraIndex H) : CompletedGroupAlgebraIndex G

theorem

completedGroupAlgebraComapIndex_subgroup

L60 ↗

CompletedGroupAlgebra.completedGroupAlgebraComapIndex_subgroup

Documentation

The subgroup underlying the comap index is the subgroup-theoretic comap.

Source context 9 commands

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

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

Lean source · statement

theorem completedGroupAlgebraComapIndex_subgroup
    (φ : G →* H) (hφ : Continuous φ)
    (V : CompletedGroupAlgebraIndex H) :
    (((OrderDual.ofDual (completedGroupAlgebraComapIndex (G := G) φ hφ V)).1 :
        OpenNormalSubgroup G) : Subgroup G) =
      (((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H).comap φ

theorem

completedGroupAlgebraComapIndex_mono

L70 ↗

CompletedGroupAlgebra.completedGroupAlgebraComapIndex_mono

Documentation

Comap of all-finite completed-group-algebra indices is monotone.

Source context 9 commands

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

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

Lean source · statement

theorem completedGroupAlgebraComapIndex_mono
    (φ : G →* H) (hφ : Continuous φ)
    {V W : CompletedGroupAlgebraIndex H} (hVW : V ≤ W) :
    completedGroupAlgebraComapIndex (G := G) φ hφ V ≤
      completedGroupAlgebraComapIndex (G := G) φ hφ W

def

completedGroupAlgebraComapQuotientMap

L83 ↗

CompletedGroupAlgebra.completedGroupAlgebraComapQuotientMap

Documentation

The quotient homomorphism \(G/\varphi^{-1}(V) \to H/V\) induced by a continuous homomorphism \(\varphi: G \to H\).

Source context 8 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe v
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def completedGroupAlgebraComapQuotientMap
    (φ : G →* H) (hφ : Continuous φ)
    (V : CompletedGroupAlgebraIndex H) :
    CompletedGroupAlgebraQuotient G (completedGroupAlgebraComapIndex (G := G) φ hφ V) →*
      CompletedGroupAlgebraQuotient H V

theorem

completedGroupAlgebraComapQuotientMap_mk

L97 ↗

CompletedGroupAlgebra.completedGroupAlgebraComapQuotientMap_mk

Documentation

The quotient map associated with the inverse-image subgroup sends the class of \(g\in G\) to the class of \(\varphi(g)\in H\).

Source context 8 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe v
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem completedGroupAlgebraComapQuotientMap_mk
    (φ : G →* H) (hφ : Continuous φ)
    (V : CompletedGroupAlgebraIndex H) (g : G) :
    completedGroupAlgebraComapQuotientMap (G := G) φ hφ V
        (QuotientGroup.mk'
          ((((OrderDual.ofDual (completedGroupAlgebraComapIndex (G := G) φ hφ V)).1 :
            OpenNormalSubgroup G) : Subgroup G)) g) =
      QuotientGroup.mk'
        ((((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H)) (φ g)

theorem

completedGroupAlgebraComapQuotientMap_surjective

L109 ↗

CompletedGroupAlgebra.completedGroupAlgebraComapQuotientMap_surjective

Documentation

A surjective homomorphism induces a surjective map on the comap quotients.

Source context 8 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe v
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem completedGroupAlgebraComapQuotientMap_surjective
    (φ : G →* H) (hφ : Continuous φ)
    (hφsurj : Function.Surjective φ) (V : CompletedGroupAlgebraIndex H) :
    Function.Surjective (completedGroupAlgebraComapQuotientMap (G := G) φ hφ V)

Module documentation

Completed Group Algebra / All Finite Functoriality / Comap

Declarations

completedGroupAlgebraComapIndex

completedGroupAlgebraComapIndex_subgroup

completedGroupAlgebraComapIndex_mono

completedGroupAlgebraComapQuotientMap

completedGroupAlgebraComapQuotientMap_mk

completedGroupAlgebraComapQuotientMap_surjective