Source: ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Basic
1import ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.Core
2import Mathlib.RingTheory.Ideal.Basic
4/-!
5# Fox differential: completed — \(\mathbb{Z}_C\) coefficients — augmentation ideal — basic
7The principal declarations in this module are:
9- `zcCompletedGroupAlgebraStandardAugmentationIdeal`
10 The algebraic ideal generated by the standard completed augmentation generators \([h]-1\). The
11 completed augmentation ideal itself is the kernel of the completed augmentation map, defined in
12 the completed augmentation construction with \(\mathbb{Z}_C\)-coefficients.
13- `zcCompletedGroupAlgebraBoundaryToStandardAugmentationIdeal`
14 The completed Fox boundary, with codomain restricted to the algebraic standard
15 augmentation-generator ideal.
16- `zcCompletedGroupAlgebraStandardAugmentationIdeal_eq_span`
17 The standard completed augmentation-generator ideal, viewed as a submodule, is the submodule span
18 of the standard generators.
19- `zcGroupLike_sub_one_mem_standardAugmentationIdeal`
20 Each completed group-like generator \([h]-1\) lies in the algebraic standard
21 augmentation-generator ideal.
22-/
24namespace FoxDifferential
26noncomputable section
28universe u
30section AugmentationIdeal
32variable (C : ProCGroups.FiniteGroupClass.{u})
33variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
35/--
36The algebraic ideal generated by the standard completed augmentation generators \([h]-1\). The
37completed augmentation ideal itself is the kernel of the completed augmentation map, defined in
38the completed augmentation construction with \(\mathbb{Z}_C\)-coefficients.
39-/
40def zcCompletedGroupAlgebraStandardAugmentationIdeal :
41 Ideal (ZCCompletedGroupAlgebra C H) :=
42 Ideal.span (Set.range fun h : H => zcGroupLike C H h - 1)
44/--
45The standard completed augmentation-generator ideal, viewed as a submodule, is the submodule
46span of the standard generators.
47-/
48theorem zcCompletedGroupAlgebraStandardAugmentationIdeal_eq_span :
49 ((zcCompletedGroupAlgebraStandardAugmentationIdeal C H :
50 Ideal (ZCCompletedGroupAlgebra C H)) :
51 Submodule (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebra C H)) =
52 Submodule.span (ZCCompletedGroupAlgebra C H)
53 (Set.range fun h : H => zcGroupLike C H h - 1) :=
54 rfl
56/--
57Each completed group-like generator \([h]-1\) lies in the algebraic standard
58augmentation-generator ideal.
59-/
60theorem zcGroupLike_sub_one_mem_standardAugmentationIdeal (h : H) :
61 zcGroupLike C H h - 1 ∈ zcCompletedGroupAlgebraStandardAugmentationIdeal C H :=
62 Ideal.subset_span (Set.mem_range_self h)
64variable {G : Type u} [Group G]
66/-- The completed Fox boundary lies in the algebraic standard augmentation-generator ideal. -/
67theorem zcCompletedGroupAlgebraBoundary_mem_standardAugmentationIdeal
68 (ψ : G →* H) (g : G) :
69 zcCompletedGroupAlgebraBoundary C ψ g ∈
70 zcCompletedGroupAlgebraStandardAugmentationIdeal C H := by
71 change zcGroupLike C H (ψ g) - 1 ∈
72 zcCompletedGroupAlgebraStandardAugmentationIdeal C H
73 exact zcGroupLike_sub_one_mem_standardAugmentationIdeal C H (ψ g)
75/--
76The completed Fox boundary, with codomain restricted to the algebraic standard
77augmentation-generator ideal.
78-/
79def zcCompletedGroupAlgebraBoundaryToStandardAugmentationIdeal
80 (ψ : G →* H) :
81 ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
82 (zcCompletedGroupAlgebraStandardAugmentationIdeal C H) where
83 toFun g :=
84 ⟨zcCompletedGroupAlgebraBoundary C ψ g,
85 zcCompletedGroupAlgebraBoundary_mem_standardAugmentationIdeal C H ψ g⟩
86 map_mul' g h := by
87 apply Subtype.ext
88 exact (zcCompletedGroupAlgebraBoundary C ψ).map_mul g h
90/--
91The completed Fox tail is restricted to the algebraic standard augmentation ideal as its
92codomain.
93-/
94def zcToStdAugIdeal
95 (ψ : G →* H) :
96 ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
97 zcCompletedGroupAlgebraStandardAugmentationIdeal C H :=
98 crossedHomModuleLift
99 (A := zcCompletedGroupAlgebraStandardAugmentationIdeal C H)
100 (zcCompletedGroupAlgebraScalar C ψ)
101 (zcCompletedGroupAlgebraBoundaryToStandardAugmentationIdeal C H ψ)
103/--
104The value of the standard-augmentation-ideal-valued completed Fox tail is the underlying
105completed group-algebra tail.
106-/
107@[simp]
108theorem zcToStdAugIdeal_val
109 (ψ : G →* H) (x : ZCCompletedDifferentialModule C ψ) :
110 ((zcToStdAugIdeal C H ψ x :
111 ZCCompletedGroupAlgebra C H)) =
112 zcToCompletedGroupAlgebra C ψ x := by
113 let L := zcToStdAugIdeal C H ψ
114 have hL :
115 (zcCompletedGroupAlgebraStandardAugmentationIdeal C H).subtype.comp L =
116 zcToCompletedGroupAlgebra C ψ := by
117 apply crossedDifferentialModuleHom_ext
118 (A := ZCCompletedGroupAlgebra C H)
119 (zcCompletedGroupAlgebraScalar C ψ)
120 intro g
121 simp only [zcToStdAugIdeal, LinearMap.coe_comp, Submodule.coe_subtype,
122 Function.comp_apply, crossedHomModuleLift_universal,
123 zcCompletedGroupAlgebraBoundaryToStandardAugmentationIdeal, L]
124 exact (zcToCompletedGroupAlgebra_universal C ψ g).symm
125 simpa [L] using congrArg (fun f => f x) hL
127/-- The completed Fox tail lands in the algebraic standard augmentation-generator ideal. -/
128theorem zcToCompletedGroupAlgebra_mem_standardAugmentationIdeal
129 (ψ : G →* H) (x : ZCCompletedDifferentialModule C ψ) :
130 zcToCompletedGroupAlgebra C ψ x ∈
131 zcCompletedGroupAlgebraStandardAugmentationIdeal C H := by
132 simpa [zcToStdAugIdeal_val] using
133 (zcToStdAugIdeal C H ψ x).2
135/--
136The range of the completed Fox tail is contained in the algebraic standard
137augmentation-generator ideal.
138-/
139theorem zcToCompletedGroupAlgebra_range_le_standardAugmentationIdeal
140 (ψ : G →* H) :
141 LinearMap.range (zcToCompletedGroupAlgebra C ψ) ≤
142 (zcCompletedGroupAlgebraStandardAugmentationIdeal C H :
143 Submodule (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebra C H)) := by
144 rintro x ⟨m, rfl⟩
145 exact zcToCompletedGroupAlgebra_mem_standardAugmentationIdeal C H ψ m
147/--
148If \(\psi\) is surjective, the completed Fox tail has range exactly the algebraic standard
149augmentation-generator ideal.
150-/
151theorem zcToCompletedGroupAlgebra_range_eq_standardAugmentationIdeal_of_surjective
152 (ψ : G →* H) (hψ : Function.Surjective ψ) :
153 LinearMap.range (zcToCompletedGroupAlgebra C ψ) =
154 (zcCompletedGroupAlgebraStandardAugmentationIdeal C H :
155 Submodule (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebra C H)) := by
156 refine le_antisymm
157 (zcToCompletedGroupAlgebra_range_le_standardAugmentationIdeal C H ψ) ?_
158 rw [zcCompletedGroupAlgebraStandardAugmentationIdeal_eq_span]
159 refine Submodule.span_le.2 ?_
160 rintro _ ⟨h, rfl⟩
161 rcases hψ h with ⟨g, rfl⟩
162 refine ⟨zcUniversalDifferential C ψ g, ?_⟩
163 rw [zcToCompletedGroupAlgebra_universal]
164 rfl
166/--
167If \(\psi\) is surjective, the standard-augmentation-ideal-valued completed Fox tail is
168surjective.
169-/
170theorem zcToStdAugIdeal_surjective_of_surjective
171 (ψ : G →* H) (hψ : Function.Surjective ψ) :
172 Function.Surjective
173 (zcToStdAugIdeal C H ψ) := by
174 intro y
175 have hy :
176 (y : ZCCompletedGroupAlgebra C H) ∈
177 LinearMap.range (zcToCompletedGroupAlgebra C ψ) := by
178 rw [zcToCompletedGroupAlgebra_range_eq_standardAugmentationIdeal_of_surjective
179 C H ψ hψ]
180 exact y.2
181 rcases hy with ⟨x, hx⟩
182 refine ⟨x, Subtype.ext ?_⟩
183 simpa [zcToStdAugIdeal_val] using hx
185end AugmentationIdeal
187end
189end FoxDifferential