NYLL
Module

Basic.lean

Nyll.ProCGroups.CrowellExactSequence.Profinite.SequenceMaps.Basic
6 declarations indexed from sourceView source ↗

Module documentation

Basic maps in the profinite Crowell sequence

This file defines the completed differential boundary and the maps from completed and separated differential modules to the completed \(\mathbb Z_C\)-group algebra. It proves their values on universal differentials and compatibility with separation.

Imports1
Imported by4

Declarations

def

presentedCompletedDifferentialBoundaryProCInteger

L34 ↗
CrowellExactSequence.presentedCompletedDifferentialBoundaryProCInteger
Documentation

The displayed boundary map \(A_{\psi}(C) \to \mathbb{Z}_C\llbracket H\rrbracket\) sends the generator \(dg\) to \(\psi(g)-1\).

Source context 8 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
universe u v w
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
def presentedCompletedDifferentialBoundaryProCInteger
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) (g : G) :
    ZCCompletedGroupAlgebra C H
def

presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger

L40 ↗
CrowellExactSequence.presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
Documentation

The displayed Crowell map \(A_{\psi}(C) \to \mathbb{Z}_C\llbracket H\rrbracket\).

Source context 8 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
universe u v w
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
def presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
    ZCCompletedDifferentialModule C psi.toMonoidHom →ₗ[ZCCompletedGroupAlgebra C H]
      ZCCompletedGroupAlgebra C H
def

presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger

L50 ↗
CrowellExactSequence.presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
Documentation

The displayed Crowell boundary \(A_{\psi}(C)_{\mathrm{sep}} \to \mathbb{Z}_C\llbracket H\rrbracket\) from the separated completed middle term.

Source context 8 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
universe u v w
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
def presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
    (C : ProCGroups.FiniteGroupClass.{u})
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H) :
    ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom →ₗ[ZCCompletedGroupAlgebra C H]
      ZCCompletedGroupAlgebra C H
theorem

presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger_d

L61 ↗
CrowellExactSequence.presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger_d
Documentation

The displayed Crowell map sends the universal differential \(dg\) to \(\psi(g)-1\).

Source context 9 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
universe u v w
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger_d
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) (g : G) :
    presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger (G := G) (H := H) C psi
        (zcUniversalDifferential C psi.toMonoidHom g) =
      presentedCompletedDifferentialBoundaryProCInteger (G := G) (H := H) C psi g
theorem

presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger_d

L74 ↗
CrowellExactSequence.presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger_d
Documentation

The separated Crowell boundary sends the separated universal differential \(dg\) to \(\psi(g)-1\).

Source context 9 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
universe u v w
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger_d
    (C : ProCGroups.FiniteGroupClass.{u})
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H) (g : G) :
    presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
        (G := G) (H := H) C hC psi
        (zcSeparatedUniversalDifferential C psi.toMonoidHom g) =
      presentedCompletedDifferentialBoundaryProCInteger (G := G) (H := H) C psi g
theorem

presentedSepToZC_comp_toSep

L90 ↗
CrowellExactSequence.presentedSepToZC_comp_toSep
Documentation

Passing the completed differential module to its separated quotient before applying the separated Crowell map recovers the completed Crowell map.

Source context 9 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
universe u v w
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem presentedSepToZC_comp_toSep
    (C : ProCGroups.FiniteGroupClass.{u})
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H) :
    (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
        (G := G) (H := H) C hC psi).comp
      (zcCompletedDifferentialModuleToSeparated C psi.toMonoidHom) =
    presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
      (G := G) (H := H) C psi

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