Yamaguchi Lean 4 Library
Source: ProCGroups.CrowellExactSequence.Profinite.SequenceMaps.Basic
ProCGroups/CrowellExactSequence/Profinite/SequenceMaps/Basic/Source

Source: ProCGroups.CrowellExactSequence.Profinite.SequenceMaps.Basic

1import ProCGroups.FoxDifferential.Completed.Continuous.Universal.NaturalTopology
3/-!
4# Basic maps in the profinite Crowell sequence
6This file defines the completed differential boundary and the maps from completed and separated
7differential modules to the completed \(\mathbb Z_C\)-group algebra. It proves their values on
8universal differentials and compatibility with separation.
9-/
11namespace CrowellExactSequence
13noncomputable section
15open scoped BigOperators
16open FoxDifferential
18universe u v w
20variable {G H : Type u}
21variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
22variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
24/--
25The displayed boundary map \(A_{\psi}(C) \to \mathbb{Z}_C\llbracket H\rrbracket\) sends the
26generator \(dg\) to \(\psi(g)-1\).
27-/
28def presentedCompletedDifferentialBoundaryProCInteger
29 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) (g : G) :
30 ZCCompletedGroupAlgebra C H :=
31 zcCompletedGroupAlgebraBoundary C psi.toMonoidHom g
33/-- The displayed Crowell map \(A_{\psi}(C) \to \mathbb{Z}_C\llbracket H\rrbracket\). -/
34def presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
35 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
36 ZCCompletedDifferentialModule C psi.toMonoidHom →ₗ[ZCCompletedGroupAlgebra C H]
37 ZCCompletedGroupAlgebra C H :=
38 zcToCompletedGroupAlgebra C psi.toMonoidHom
40/--
41The displayed Crowell boundary \(A_{\psi}(C)_{\mathrm{sep}} \to \mathbb{Z}_C\llbracket
42H\rrbracket\) from the separated completed middle term.
43-/
44def presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
45 (C : ProCGroups.FiniteGroupClass.{u})
47 (psi : ContinuousMonoidHom G H) :
48 ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom →ₗ[ZCCompletedGroupAlgebra C H]
49 ZCCompletedGroupAlgebra C H :=
50 zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra C hC psi
52omit [IsTopologicalGroup G] in
53/-- The displayed Crowell map sends the universal differential \(dg\) to \(\psi(g)-1\). -/
54@[simp]
55theorem presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger_d
56 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) (g : G) :
57 presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger (G := G) (H := H) C psi
58 (zcUniversalDifferential C psi.toMonoidHom g) =
59 presentedCompletedDifferentialBoundaryProCInteger (G := G) (H := H) C psi g := by
60 exact zcToCompletedGroupAlgebra_universal C psi.toMonoidHom g
62omit [IsTopologicalGroup G] in
63/--
64The separated Crowell boundary sends the separated universal differential \(dg\) to
65\(\psi(g)-1\).
66-/
67@[simp]
68theorem presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger_d
69 (C : ProCGroups.FiniteGroupClass.{u})
71 (psi : ContinuousMonoidHom G H) (g : G) :
72 presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
73 (G := G) (H := H) C hC psi
74 (zcSeparatedUniversalDifferential C psi.toMonoidHom g) =
75 presentedCompletedDifferentialBoundaryProCInteger (G := G) (H := H) C psi g := by
76 exact zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra_universal
77 (G := G) (H := H) C hC psi g
79omit [IsTopologicalGroup G] in
80/--
81Passing the completed differential module to its separated quotient before applying the
82separated Crowell map recovers the completed Crowell map.
83-/
84theorem presentedSepToZC_comp_toSep
85 (C : ProCGroups.FiniteGroupClass.{u})
87 (psi : ContinuousMonoidHom G H) :
88 (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
89 (G := G) (H := H) C hC psi).comp
90 (zcCompletedDifferentialModuleToSeparated C psi.toMonoidHom) =
91 presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
92 (G := G) (H := H) C psi := by
93 exact zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra_comp_toSeparated
94 (G := G) (H := H) C hC psi
96end
98end CrowellExactSequence