FoxDifferential/Completed/ProCIntegerCoefficients/AugmentationIdeal/Closure.lean
1import FoxDifferential.Completed.Continuous.Topology
2import FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.FiniteStage
3import ProCGroups.InverseSystems.ProjectionImageSystems
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FoxDifferential/Completed/ProCIntegerCoefficients/AugmentationIdeal/Closure.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Completed group algebra coefficients
16This module records augmentation-ideal statements for pro-\(C\) integer completed coefficient rings, including closure, finite-stage membership, and kernel descriptions.
17-/
18namespace FoxDifferential
20noncomputable section
22open scoped Topology
23open ProCGroups.Completion
24open ProCGroups.InverseSystems
25open ProCGroups.ProC
27universe u
29section Closure
31variable (C : ProCGroups.FiniteGroupClass.{u})
32variable [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)]
34variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
36omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)]
37 [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] [IsTopologicalGroup H] in
38/-- The `Z_C[[H]]` finite-stage index is directed when both the coefficient and group-quotient
41 (hForm : ProCGroups.FiniteGroupClass.Formation C) :
42 Directed (· ≤ ·) (id : ZCCompletedGroupAlgebraIndex C H → ZCCompletedGroupAlgebraIndex C H) := by
43 intro i j
44 rcases ProCIntegerIndex.directed_of_formation hForm i.1 j.1 with
45 ⟨n, hin, hjn⟩
47 (C := C) (G := H) hForm i.2 j.2 with
48 ⟨U, hiU, hjU⟩
49 exact ⟨(n, U), ⟨hin, hiU⟩, ⟨hjn, hjU⟩⟩
51omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)]
53/-- Every finite-stage augmentation-ideal element is the projection of an element of the algebraic
54standard augmentation ideal. -/
56 (i : ZCCompletedGroupAlgebraIndex C H)
57 (x : zcCompletedGroupAlgebraStageAugmentationIdeal C H i) :
59 zcCompletedGroupAlgebraProjection C H i y = (x : ZCCompletedGroupAlgebraStage C H i) := by
60 let P : zcCompletedGroupAlgebraStageAugmentationIdeal C H i → Prop := fun x =>
62 zcCompletedGroupAlgebraProjection C H i y =
63 (x : ZCCompletedGroupAlgebraStage C H i)
64 have hxSpan :
65 x ∈ Submodule.span (ZCCompletedGroupAlgebraStage C H i)
66 (Set.range (zcCompletedGroupAlgebraStageAugmentationGeneratorSubtype C H i)) := by
68 (C := C) (H := H) i]
69 simp only [Submodule.mem_top]
70 refine Submodule.span_induction (p := fun z _ => P z) ?_ ?_ ?_ ?_ hxSpan
71 · rintro _ ⟨q, rfl⟩
72 rcases QuotientGroup.mk'_surjective
73 ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup H) : Subgroup H)) q with
74 ⟨h, rfl⟩
75 refine ⟨zcGroupLike C H h - 1,
78 MonoidAlgebra.of_apply, zcCompletedGroupAlgebraProjection_one,
79 zcCompletedGroupAlgebraStageAugmentationGeneratorSubtype, zcCompletedGroupAlgebraStageAugmentationGenerator,
80 QuotientGroup.mk'_apply]
81 · exact ⟨0, (zcCompletedGroupAlgebraStandardAugmentationIdeal C H).zero_mem, by simp only [zcCompletedGroupAlgebraProjection_zero, ZeroMemClass.coe_zero]⟩
82 · intro x y _ _ hx hy
83 rcases hx with ⟨x', hx'mem, hx'proj⟩
84 rcases hy with ⟨y', hy'mem, hy'proj⟩
85 refine ⟨x' + y',
86 (zcCompletedGroupAlgebraStandardAugmentationIdeal C H).add_mem hx'mem hy'mem, ?_⟩
87 simp only [zcCompletedGroupAlgebraProjection_add, hx'proj, hy'proj, Submodule.coe_add]
88 · intro a x _ hx
89 rcases hx with ⟨x', hx'mem, hx'proj⟩
90 rcases zcCompletedGroupAlgebraProjection_surjective C H i a with ⟨a', ha'⟩
91 refine ⟨a' * x',
92 (zcCompletedGroupAlgebraStandardAugmentationIdeal C H).mul_mem_left a' hx'mem, ?_⟩
93 rw [zcCompletedGroupAlgebraProjection_mul, ha', hx'proj]
94 rfl
96/-- The completed augmentation ideal is the closure of the algebraic standard-generator ideal. -/
98 (hForm : ProCGroups.FiniteGroupClass.Formation C) :
99 closure
101 Ideal (ZCCompletedGroupAlgebra C H)) : Set (ZCCompletedGroupAlgebra C H)) =
103 Ideal (ZCCompletedGroupAlgebra C H)) : Set (ZCCompletedGroupAlgebra C H)) := by
104 let S := zcCompletedGroupAlgebraSystem C H
105 let Y : Set (ZCCompletedGroupAlgebra C H) :=
107 Set (ZCCompletedGroupAlgebra C H))
108 let Z : Set (ZCCompletedGroupAlgebra C H) :=
110 Set (ZCCompletedGroupAlgebra C H))
111 letI : Nonempty (ZCCompletedGroupAlgebraIndex C H) :=
112 ⟨(ProCIntegerIndex.terminal (C := C) inferInstance, zcCompletedGroupAlgebraTopIndex C H)⟩
113 letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, TopologicalSpace (S.X i) := fun _ =>
114 inferInstance
115 letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, CompactSpace (S.X i) := fun i => by
116 dsimp [S, zcCompletedGroupAlgebraSystem]
117 infer_instance
118 letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, T2Space (S.X i) := fun i => by
119 dsimp [S, zcCompletedGroupAlgebraSystem]
120 infer_instance
121 have hdir : Directed (· ≤ ·) (id : ZCCompletedGroupAlgebraIndex C H →
122 ZCCompletedGroupAlgebraIndex C H) :=
123 directed_zcCompletedGroupAlgebraIndex (C := C) (H := H) hForm
124 have hclosedZ : IsClosed Z := by
125 simpa [Z] using isClosed_zcCompletedGroupAlgebraAugmentationIdeal (C := C) (G := H)
126 refine le_antisymm ?_ ?_
127 · exact closure_minimal
128 (by
129 intro x hx
131 hclosedZ
132 · intro z hz
133 have hzClosure :
134 z ∈ closure Y := by
135 rw [S.mem_isClosed_iff_forall_projection_mem hdir isClosed_closure]
136 intro i
137 have hzi :
138 zcCompletedGroupAlgebraProjection C H i z ∈
139 zcCompletedGroupAlgebraStageAugmentationIdeal C H i := by
140 let zAug : ZCCompletedGroupAlgebraAugmentationIdeal C H := ⟨z, by simpa [Z] using hz⟩
141 simpa using
142 (zcCompletedGroupAlgebraAugmentationIdealProjection C H i zAug).2
143 rcases
145 (C := C) (H := H) i
146 ⟨zcCompletedGroupAlgebraProjection C H i z, hzi⟩ with
147 ⟨y, hy, hyproj⟩
148 refine ⟨y, subset_closure (by simpa [Y] using hy), ?_⟩
149 exact hyproj
150 simpa [Y] using hzClosure
152end Closure
154end
156end FoxDifferential