FoxDifferential/Completed/DifferentialModule/Identity.lean
1import FoxDifferential.Completed.FiniteStage.Bifiltered.InverseSystem
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/DifferentialModule/Identity.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Completed differential modules
14The completed differential module is organized separately from coefficient algebras; its universal and quotient maps are used by completed crossed differentials.
15-/
16namespace FoxDifferential
18noncomputable section
20open ProCGroups
21open ProCGroups.ProC
23universe u v
25variable (ℓ : ℕ) [Fact (0 < ℓ)]
26variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
27variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
29/-- Definition of identityCompletedGroupAlgebraOpenSubgroup. -/
31 (G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G] :
32 OpenSubgroup G :=
33 OpenSubgroup.mk (⊥ : Subgroup G) (isOpen_discrete _)
35/-- The identity open normal subgroup of a discrete group. -/
37 (G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G] :
38 OpenNormalSubgroup G :=
39 OpenNormalSubgroup.mk (identityCompletedGroupAlgebraOpenSubgroup G)
40 (Subgroup.Normal.mk (by
41 intro n hn g
42 change n ∈ (⊥ : Subgroup G) at hn
43 rw [Subgroup.mem_bot] at hn
44 subst n
45 simp only [mul_one, mul_inv_cancel, one_mem]))
47/-- 標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
48@[simp]
50 (G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G] :
51 ((identityCompletedGroupAlgebraOpenNormalSubgroup G : OpenNormalSubgroup G) :
52 Subgroup G) = ⊥ := rfl
54/-- The identity quotient `G/1`, as a completed-group-algebra index for a finite discrete group. -/
56 (G : Type u) [Group G] [TopologicalSpace G]
57 [DiscreteTopology G] [Finite G] :
59 refine ⟨identityCompletedGroupAlgebraOpenNormalSubgroup G, ?_⟩
60 change Finite
61 (G ⧸ ((identityCompletedGroupAlgebraOpenNormalSubgroup G : OpenNormalSubgroup G) :
62 Subgroup G))
64 infer_instance
66/-- The identity quotient `G/1`, as a class-restricted completed-group-algebra stage whenever
69 (C : ProCGroups.FiniteGroupClass.{u})
70 (G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G]
71 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C) (hG : C G) :
72 OpenNormalSubgroupInClass C G := by
73 refine ⟨identityCompletedGroupAlgebraOpenNormalSubgroup G, ?_⟩
74 change C (G ⧸ (⊥ : Subgroup G))
75 exact hIso ⟨(QuotientGroup.quotientBot (G := G)).symm⟩ hG
77/-- The completed-group-algebra stage whose group quotient is `G/1`. -/
79 (G : Type u) [Group G] [TopologicalSpace G]
80 [DiscreteTopology G] [Finite G] :
81 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G :=
82 OrderDual.toDual (identityCompletedGroupAlgebraSubgroupInClass G)
84/-- The class-restricted completed-group-algebra stage whose group quotient is `G/1`. -/
86 (C : ProCGroups.FiniteGroupClass.{u})
87 (G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G]
88 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C) (hG : C G) :
89 CompletedGroupAlgebraIndexInClass G C :=
90 OrderDual.toDual (identityCompletedGroupAlgebraSubgroupInClassOfMem C G hIso hG)
92/-- The projection to the identity completed stage is injective on group elements. -/
94 (G : Type u) [Group G] [TopologicalSpace G]
95 [DiscreteTopology G] [Finite G] :
96 Function.Injective
98 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
99 (identityCompletedGroupAlgebraIndex G)) := by
100 intro g h hgh
101 change QuotientGroup.mk' (⊥ : Subgroup G) g =
102 QuotientGroup.mk' (⊥ : Subgroup G) h at hgh
103 have hbase := congrArg (QuotientGroup.quotientBot (G := G)) hgh
104 simpa using hbase
106/-- The projection to the class-restricted identity completed stage is injective on group
107elements. -/
109 (C : ProCGroups.FiniteGroupClass.{u})
110 (G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G]
111 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C) (hG : C G) :
112 Function.Injective
114 (C := C) (G := G)
115 (identityCompletedGroupAlgebraIndexInClassOfMem C G hIso hG)) := by
116 intro g h hgh
117 change QuotientGroup.mk' (⊥ : Subgroup G) g =
118 QuotientGroup.mk' (⊥ : Subgroup G) h at hgh
119 have hbase := congrArg (QuotientGroup.quotientBot (G := G)) hgh
120 simpa using hbase
122/-- The residue group-algebra stage map to the identity completed stage is injective. -/
124 (n : ℕ)
125 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
126 [DiscreteTopology G] [Finite G] :
127 Function.Injective
129 (identityCompletedGroupAlgebraIndex G)) := by
130 classical
131 change Function.Injective
132 (MonoidAlgebra.mapDomain
133 (R := ModNCompletedCoeff n)
135 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
137 exact MonoidAlgebra.mapDomain_injective
140/-- The residue group-algebra stage map to the class-restricted identity completed stage is
141injective. -/
143 (n : ℕ) (C : ProCGroups.FiniteGroupClass.{u})
144 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
145 [DiscreteTopology G]
146 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C) (hG : C G) :
147 Function.Injective
149 (identityCompletedGroupAlgebraIndexInClassOfMem C G hIso hG)) := by
150 classical
151 change Function.Injective
152 (MonoidAlgebra.mapDomain
153 (R := ModNCompletedCoeff n)
155 (C := C) (G := G)
156 (identityCompletedGroupAlgebraIndexInClassOfMem C G hIso hG)))
157 exact MonoidAlgebra.mapDomain_injective
159 C G hIso hG)
161end
163end FoxDifferential