Source: ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Closure
1import ProCGroups.FoxDifferential.Completed.Continuous.Topology
2import ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.FiniteStage
3import ProCGroups.InverseSystems.ProjectionImageSystems
5/-!
6# Fox differential: completed — \(\mathbb{Z}_C\) coefficients — augmentation ideal — closure
8The principal declarations in this module are:
10- `zcCompletedGroupAlgebraStageAugmentationIdeal_mem_projection_standard`
11 Every finite-stage augmentation-ideal element is the projection of an element of the algebraic
12 standard augmentation ideal.
13- `closure_zcCompletedGroupAlgebraStandardAugmentationIdeal_eq_augmentationIdeal`
14 The completed augmentation ideal is the closure of the algebraic standard-generator ideal.
15-/
17namespace FoxDifferential
19noncomputable section
21open scoped Topology
22open ProCGroups.Completion
23open ProCGroups.InverseSystems
24open ProCGroups.ProC
26universe u
28section Closure
30variable (C : ProCGroups.FiniteGroupClass.{u})
32variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
34omit
36/--
37Every finite-stage augmentation-ideal element is the projection of an element of the algebraic
38standard augmentation ideal.
39-/
40theorem zcCompletedGroupAlgebraStageAugmentationIdeal_mem_projection_standard
41 (i : ZCCompletedGroupAlgebraIndex C H)
42 (x : zcCompletedGroupAlgebraStageAugmentationIdeal C H i) :
43 ∃ y ∈ zcCompletedGroupAlgebraStandardAugmentationIdeal C H,
44 zcCompletedGroupAlgebraProjection C H i y = (x : ZCCompletedGroupAlgebraStage C H i) := by
45 let P : zcCompletedGroupAlgebraStageAugmentationIdeal C H i → Prop := fun x =>
46 ∃ y ∈ zcCompletedGroupAlgebraStandardAugmentationIdeal C H,
47 zcCompletedGroupAlgebraProjection C H i y =
48 (x : ZCCompletedGroupAlgebraStage C H i)
49 have hxSpan :
50 x ∈ Submodule.span (ZCCompletedGroupAlgebraStage C H i)
51 (Set.range (zcCompletedGroupAlgebraStageAugmentationGeneratorSubtype C H i)) := by
52 rw [zcCompletedGroupAlgebraStageAugmentationIdeal_span_standardGenerators_eq_top
53 (C := C) (H := H) i]
54 simp only [Submodule.mem_top]
55 refine Submodule.span_induction (p := fun z _ => P z) ?_ ?_ ?_ ?_ hxSpan
56 · rintro _ ⟨q, rfl⟩
57 rcases QuotientGroup.mk'_surjective
58 ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup H) : Subgroup H)) q with
59 ⟨h, rfl⟩
60 refine ⟨zcGroupLike C H h - 1,
61 zcGroupLike_sub_one_mem_standardAugmentationIdeal C H h, ?_⟩
62 simp only [zcCompletedGroupAlgebraProjection_sub, zcCompletedGroupAlgebraProjection_groupLike,
63 MonoidAlgebra.of_apply, zcCompletedGroupAlgebraProjection_one,
64 zcCompletedGroupAlgebraStageAugmentationGeneratorSubtype,
65 zcCompletedGroupAlgebraStageAugmentationGenerator,
66 QuotientGroup.mk'_apply]
67 · exact ⟨0, (zcCompletedGroupAlgebraStandardAugmentationIdeal C H).zero_mem, by simp only
68 [zcCompletedGroupAlgebraProjection_zero, ZeroMemClass.coe_zero]⟩
69 · intro x y _ _ hx hy
70 rcases hx with ⟨x', hx'mem, hx'proj⟩
71 rcases hy with ⟨y', hy'mem, hy'proj⟩
72 refine ⟨x' + y',
73 (zcCompletedGroupAlgebraStandardAugmentationIdeal C H).add_mem hx'mem hy'mem, ?_⟩
74 simp only [zcCompletedGroupAlgebraProjection_add, hx'proj, hy'proj, Submodule.coe_add]
75 · intro a x _ hx
76 rcases hx with ⟨x', hx'mem, hx'proj⟩
77 rcases zcCompletedGroupAlgebraProjection_surjective C H i a with ⟨a', ha'⟩
78 refine ⟨a' * x',
79 (zcCompletedGroupAlgebraStandardAugmentationIdeal C H).mul_mem_left a' hx'mem, ?_⟩
80 rw [zcCompletedGroupAlgebraProjection_mul, ha', hx'proj]
81 rfl
83/-- The completed augmentation ideal is the closure of the algebraic standard-generator ideal. -/
84theorem closure_zcCompletedGroupAlgebraStandardAugmentationIdeal_eq_augmentationIdeal
85 (hForm : ProCGroups.FiniteGroupClass.Formation C) :
86 closure
87 ((zcCompletedGroupAlgebraStandardAugmentationIdeal C H :
88 Ideal (ZCCompletedGroupAlgebra C H)) : Set (ZCCompletedGroupAlgebra C H)) =
89 ((zcCompletedGroupAlgebraAugmentationIdeal C H :
90 Ideal (ZCCompletedGroupAlgebra C H)) : Set (ZCCompletedGroupAlgebra C H)) := by
91 let S := zcCompletedGroupAlgebraSystem C H
92 let Y : Set (ZCCompletedGroupAlgebra C H) :=
93 (zcCompletedGroupAlgebraStandardAugmentationIdeal C H :
94 Set (ZCCompletedGroupAlgebra C H))
95 let Z : Set (ZCCompletedGroupAlgebra C H) :=
96 (zcCompletedGroupAlgebraAugmentationIdeal C H :
97 Set (ZCCompletedGroupAlgebra C H))
98 letI : Nonempty (ZCCompletedGroupAlgebraIndex C H) :=
99 ⟨(ProCIntegerIndex.terminal (C := C) inferInstance, zcCompletedGroupAlgebraTopIndex C H)⟩
100 letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, TopologicalSpace (S.X i) := fun _ =>
101 inferInstance
102 letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, CompactSpace (S.X i) := fun i => by
103 dsimp [S, zcCompletedGroupAlgebraSystem]
104 change @CompactSpace (ZCCompletedGroupAlgebraStage C H i) ⊥
105 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
106 letI : Finite (ZCCompletedGroupAlgebraStage C H i) :=
107 finite_modNCompletedGroupAlgebraStageInClass
108 (n := i.1.modulus) (G := H) C i.2
109 exact Finite.compactSpace
110 letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, T2Space (S.X i) := fun i => by
111 dsimp [S, zcCompletedGroupAlgebraSystem]
112 change @T2Space (ZCCompletedGroupAlgebraStage C H i) ⊥
113 exact @DiscreteTopology.toT2Space _ ⊥ ⟨rfl⟩
114 have hdir : Directed (· ≤ ·) (id : ZCCompletedGroupAlgebraIndex C H →
115 ZCCompletedGroupAlgebraIndex C H) :=
116 directed_zcCompletedGroupAlgebraIndex_of_formation (C := C) (H := H) hForm
117 have hclosedZ : IsClosed Z := by
118 simpa [Z] using isClosed_zcCompletedGroupAlgebraAugmentationIdeal (C := C) (G := H)
119 refine le_antisymm ?_ ?_
120 · exact closure_minimal
121 (by
122 intro x hx
123 exact zcCompletedGroupAlgebraStandardAugmentationIdeal_le_augmentationIdeal C H hx)
124 hclosedZ
125 · intro z hz
126 have hzClosureS :
127 (show S.inverseLimit from z) ∈
128 closure (show Set S.inverseLimit from Y) := by
129 rw [S.mem_isClosed_iff_forall_projection_mem hdir isClosed_closure]
130 intro i
131 have hzi :
132 zcCompletedGroupAlgebraProjection C H i z ∈
133 zcCompletedGroupAlgebraStageAugmentationIdeal C H i := by
134 let zAug : ZCCompletedGroupAlgebraAugmentationIdeal C H := ⟨z, by simpa [Z] using hz⟩
135 simpa using
136 (zcCompletedGroupAlgebraAugmentationIdealProjection C H i zAug).2
137 rcases
138 zcCompletedGroupAlgebraStageAugmentationIdeal_mem_projection_standard
139 (C := C) (H := H) i
140 ⟨zcCompletedGroupAlgebraProjection C H i z, hzi⟩ with
141 ⟨y, hy, hyproj⟩
142 refine ⟨y, subset_closure ?_, ?_⟩
143 · convert hy using 1
144 rfl
145 exact hyproj
146 convert hzClosureS using 1 <;> rfl
148end Closure
150end
152end FoxDifferential