ProCGroups.CrowellExactSequence.Profinite.SequenceMaps.Basic

3 Theorems | 3 Definitions

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.

import

ProCGroups.FoxDifferential.Completed.Continuous.Universal.NaturalTopology

Imported by

Definition CrowellExactSequence.presentedCompletedDifferentialBoundaryProCInteger

def presentedCompletedDifferentialBoundaryProCInteger
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) (g : G) :
    ZCCompletedGroupAlgebra C H :=
  zcCompletedGroupAlgebraBoundary C psi.toMonoidHom g

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

Definition CrowellExactSequence.presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger

def presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
    ZCCompletedDifferentialModule C psi.toMonoidHom →ₗ[ZCCompletedGroupAlgebra C H]
      ZCCompletedGroupAlgebra C H :=
  zcToCompletedGroupAlgebra C psi.toMonoidHom

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

Definition CrowellExactSequence.presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger

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 :=
  zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra C hC psi

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

Theorem CrowellExactSequence.presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger_d

omit [IsTopologicalGroup G] in
@[simp]
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

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

Show Lean proof

Theorem CrowellExactSequence.presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger_d

omit [IsTopologicalGroup G] in
@[simp]
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

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

Show Lean proof

Theorem CrowellExactSequence.presentedSepToZC_comp_toSep

omit [IsTopologicalGroup G] in
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

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

Show Lean proof

ProCGroups.CrowellExactSequence.Profinite.SequenceMaps.Basic

Declarations