FoxDifferential/Completed/ProCIntegerCoefficients/AugmentationIdeal/Basic.lean
1import FoxDifferential.Completed.ProCIntegerCoefficients.Core
2import Mathlib.RingTheory.Ideal.Basic
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/ProCIntegerCoefficients/AugmentationIdeal/Basic.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Completed group algebra coefficients
15This module records augmentation-ideal statements for pro-\(C\) integer completed coefficient rings, including closure, finite-stage membership, and kernel descriptions.
16-/
17namespace FoxDifferential
19noncomputable section
21universe u
23section AugmentationIdeal
25variable (C : ProCGroups.FiniteGroupClass.{u})
26variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
28/-- The algebraic ideal generated by the standard completed augmentation generators `[h] - 1`.
30The completed augmentation ideal itself is the kernel of the completed augmentation map, defined
31in `FoxDifferential.Completed.ProCIntegerCoefficients.Augmentation`. -/
33 Ideal (ZCCompletedGroupAlgebra C H) :=
34 Ideal.span (Set.range fun h : H => zcGroupLike C H h - 1)
36/-- The standard completed augmentation-generator ideal, viewed as a submodule, is the submodule
37span of the standard generators. -/
40 Ideal (ZCCompletedGroupAlgebra C H)) :
41 Submodule (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebra C H)) =
42 Submodule.span (ZCCompletedGroupAlgebra C H)
43 (Set.range fun h : H => zcGroupLike C H h - 1) :=
44 rfl
46/-- Each standard completed augmentation generator `[h] - 1` lies in the algebraic ideal
47generated by such standard generators. -/
48theorem zcGroupLike_sub_one_mem_standardAugmentationIdeal (h : H) :
49 zcGroupLike C H h - 1 ∈ zcCompletedGroupAlgebraStandardAugmentationIdeal C H :=
50 Ideal.subset_span (Set.mem_range_self h)
52variable {G : Type u} [Group G]
54/-- The completed Fox boundary lands in the algebraic standard-generator ideal. -/
56 (ψ : G →* H) (g : G) :
57 zcCompletedGroupAlgebraBoundary C ψ g ∈
59 simpa [zcCompletedGroupAlgebraBoundary] using
62/-- The completed Fox boundary, with codomain restricted to the algebraic standard
63augmentation-generator ideal. -/
65 (ψ : G →* H) (g : G) :
67 ⟨zcCompletedGroupAlgebraBoundary C ψ g,
70/-- The standard-augmentation-ideal-valued completed Fox boundary is a crossed differential. -/
72 (ψ : G →* H) :
75 (zcCompletedGroupAlgebraBoundaryToStandardAugmentationIdeal C H ψ) := by
76 intro g h
77 apply Subtype.ext
78 exact zcCompletedGroupAlgebraBoundary_mul C ψ g h
80/-- The completed Fox tail with codomain restricted to the algebraic standard augmentation
81ideal. -/
83 (ψ : G →* H) :
84 ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
87 (A := zcCompletedGroupAlgebraStandardAugmentationIdeal C H) C ψ
91@[simp]
92theorem zcToStdAugIdeal_val
93 (ψ : G →* H) (x : ZCCompletedDifferentialModule C ψ) :
94 ((zcToStdAugIdeal C H ψ x :
95 ZCCompletedGroupAlgebra C H)) =
96 zcToCompletedGroupAlgebra C ψ x := by
97 let L := zcToStdAugIdeal C H ψ
98 have hL :
99 (zcCompletedGroupAlgebraStandardAugmentationIdeal C H).subtype.comp L =
100 zcToCompletedGroupAlgebra C ψ := by
101 apply zcCompletedDifferentialModuleHom_ext C ψ
102 intro g
103 simp only [zcToStdAugIdeal, LinearMap.coe_comp, Submodule.coe_subtype, Function.comp_apply,
104 zcCompletedDifferentialModuleLift_universal, zcCompletedGroupAlgebraBoundaryToStandardAugmentationIdeal,
106 simpa [L] using congrArg (fun f => f x) hL
108/-- The completed Fox tail lands in the algebraic standard augmentation-generator ideal. -/
110 (ψ : G →* H) (x : ZCCompletedDifferentialModule C ψ) :
111 zcToCompletedGroupAlgebra C ψ x ∈
113 simpa [zcToStdAugIdeal_val] using
114 (zcToStdAugIdeal C H ψ x).2
116/-- The range of the completed Fox tail is contained in the algebraic standard augmentation
117ideal. -/
119 (ψ : G →* H) :
120 LinearMap.range (zcToCompletedGroupAlgebra C ψ) ≤
122 Submodule (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebra C H)) := by
123 rintro x ⟨m, rfl⟩
124 exact zcToCompletedGroupAlgebra_mem_standardAugmentationIdeal C H ψ m
126/-- If `ψ` is surjective, the completed Fox tail has range exactly the algebraic standard
127augmentation-generator ideal. -/
129 (ψ : G →* H) (hψ : Function.Surjective ψ) :
130 LinearMap.range (zcToCompletedGroupAlgebra C ψ) =
132 Submodule (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebra C H)) := by
133 refine le_antisymm
136 refine Submodule.span_le.2 ?_
137 rintro _ ⟨h, rfl⟩
138 rcases hψ h with ⟨g, rfl⟩
139 exact ⟨zcUniversalDifferential C ψ g, by simp only [zcToCompletedGroupAlgebra_universal, zcCompletedGroupAlgebraBoundary]⟩
141/-- If `ψ` is surjective, the standard-augmentation-ideal-valued completed Fox tail is
142surjective. -/
144 (ψ : G →* H) (hψ : Function.Surjective ψ) :
145 Function.Surjective
146 (zcToStdAugIdeal C H ψ) := by
147 intro y
148 have hy :
149 (y : ZCCompletedGroupAlgebra C H) ∈
150 LinearMap.range (zcToCompletedGroupAlgebra C ψ) := by
152 C H ψ hψ]
153 exact y.2
154 rcases hy with ⟨x, hx⟩
155 refine ⟨x, Subtype.ext ?_⟩
156 simpa [zcToStdAugIdeal_val] using hx
158end AugmentationIdeal
160end
162end FoxDifferential