Module

Comap.lean

Nyll.ProCGroups.FoxDifferential.Completed.DifferentialModule.Map.Comap

7 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — differential module — map — comap

The principal declarations in this module are:

completedGroupAlgebraComapIndex

The index map that sends a target finite quotient to its pullback finite quotient on the source.

completedGroupAlgebraComapQuotientMap

The quotient map from the pulled-back source quotient to the target quotient induced by the original homomorphism.

completedGroupAlgebraComapIndex_subgroup

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

completedGroupAlgebraComapQuotientMap_mk

The pullback quotient map sends the class of a source element to the class of its image in the target quotient in the Fox differential construction.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.DifferentialModule.Identity

Imported by2

def

completedGroupAlgebraComapIndex

L42 ↗

FoxDifferential.completedGroupAlgebraComapIndex

Documentation

The index map that sends a target finite quotient to its pullback finite quotient on the source.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def completedGroupAlgebraComapIndex
    (ψ : ContinuousMonoidHom G H) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex H) :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G

theorem

completedGroupAlgebraComapIndex_subgroup

L69 ↗

FoxDifferential.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.

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup G] in

Lean source · statement

theorem completedGroupAlgebraComapIndex_subgroup
    (ψ : ContinuousMonoidHom G H) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex H) :
    (((OrderDual.ofDual (completedGroupAlgebraComapIndex (G := G) (H := H) ψ U)).1 :
        OpenNormalSubgroup G) : Subgroup G) =
      Subgroup.comap ψ.toMonoidHom
        (((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H)

def

completedGroupAlgebraComapQuotientMap

L81 ↗

FoxDifferential.completedGroupAlgebraComapQuotientMap

Documentation

The quotient map from the pulled-back source quotient to the target quotient induced by the original homomorphism.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def completedGroupAlgebraComapQuotientMap
    (ψ : ContinuousMonoidHom G H) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex H) :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G
        (completedGroupAlgebraComapIndex (G := G) (H := H) ψ U) →*
      _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H U

theorem

completedGroupAlgebraComapQuotientMap_mk

L95 ↗

FoxDifferential.completedGroupAlgebraComapQuotientMap_mk

Documentation

The pullback quotient map sends the class of a source element to the class of its image in the target quotient in the Fox differential construction.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem completedGroupAlgebraComapQuotientMap_mk
    (ψ : ContinuousMonoidHom G H) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex
        H) (g : G) :
    completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ U
        (QuotientGroup.mk' _ g) =
      QuotientGroup.mk' (((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H) (ψ g)

theorem

completedGroupAlgebraComapQuotientMap_surjective

L109 ↗

FoxDifferential.completedGroupAlgebraComapQuotientMap_surjective

Documentation

If \(\psi : G \to H\) is surjective, the induced map from the pulled-back finite quotient \(G / \psi^{-1}(U)\) to \(H / U\) is surjective. This is the finite-quotient input used later to lift coefficients in the completed free-derivative construction.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem completedGroupAlgebraComapQuotientMap_surjective
    (ψ : ContinuousMonoidHom G H) (hψ : Function.Surjective ψ)
    (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex H) :
    Function.Surjective
      (completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ U)

theorem

completedGroupAlgebraComapIndex_mono

L127 ↗

FoxDifferential.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.

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup G] in

Lean source · statement

theorem completedGroupAlgebraComapIndex_mono
    (ψ : ContinuousMonoidHom G H) {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex
        H} (hUV : U ≤ V) :
    completedGroupAlgebraComapIndex (G := G) (H := H) ψ U ≤
      completedGroupAlgebraComapIndex (G := G) (H := H) ψ V

theorem

completedGroupAlgebraComapQuotientMap_compatible

L141 ↗

FoxDifferential.completedGroupAlgebraComapQuotientMap_compatible

Documentation

The comap quotient maps are compatible with refinement of finite quotients.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem completedGroupAlgebraComapQuotientMap_compatible
    (ψ : ContinuousMonoidHom G H) {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex
        H} (hUV : U ≤ V) :
    (OpenNormalSubgroupInClass.map
        (C := ProCGroups.FiniteGroupClass.allFinite) (G := H)
        (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV).comp
        (completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ V) =
      (completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ U).comp
        (OpenNormalSubgroupInClass.map
          (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
          (U := OrderDual.ofDual
            (completedGroupAlgebraComapIndex (G := G) (H := H) ψ U))
          (V := OrderDual.ofDual
            (completedGroupAlgebraComapIndex (G := G) (H := H) ψ V))
          (completedGroupAlgebraComapIndex_mono (G := G) (H := H) ψ hUV))

Module documentation

Fox differential: completed — differential module — map — comap

Declarations

completedGroupAlgebraComapIndex

completedGroupAlgebraComapIndex_subgroup

completedGroupAlgebraComapQuotientMap

completedGroupAlgebraComapQuotientMap_mk

completedGroupAlgebraComapQuotientMap_surjective

completedGroupAlgebraComapIndex_mono

completedGroupAlgebraComapQuotientMap_compatible