Source: ProCGroups.FoxDifferential.Completed.DifferentialModule.Identity

1import ProCGroups.FoxDifferential.Completed.FiniteStage.Bifiltered.InverseSystem

3/-!

4# Fox differential: completed — differential module — identity

6The principal declarations in this module are:

8- `identityCompletedGroupAlgebraOpenSubgroup`

9 The identity completed-group-algebra open subgroup used for the identity quotient stage.

10- `identityCompletedGroupAlgebraOpenNormalSubgroup`

11 The identity open normal subgroup of a discrete group.

12- `identityCompletedGroupAlgebraOpenNormalSubgroup_coe`

13 The identity completed-group-algebra open normal subgroup coerces to the corresponding open

14 subgroup.

15- `openNormalSubgroupInClassProj_identityCompletedGroupAlgebraIndex_injective`

16 The projection to the identity completed stage is injective on group elements.

17-/

19namespace FoxDifferential

21noncomputable section

23open ProCGroups

24open ProCGroups.ProC

26universe u v

28variable (ℓ : ℕ) [Fact (0 < ℓ)]

29variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

30variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

32/-- The identity completed-group-algebra open subgroup used for the identity quotient stage. -/

33def identityCompletedGroupAlgebraOpenSubgroup

34 (G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G] :

35 OpenSubgroup G :=

36 OpenSubgroup.mk (⊥ : Subgroup G) (isOpen_discrete _)

38/-- The identity open normal subgroup of a discrete group. -/

39def identityCompletedGroupAlgebraOpenNormalSubgroup

40 (G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G] :

41 OpenNormalSubgroup G :=

42 OpenNormalSubgroup.mk (identityCompletedGroupAlgebraOpenSubgroup G)

43 (Subgroup.Normal.mk (by

44 intro n hn g

45 change n ∈ (⊥ : Subgroup G) at hn

46 rw [Subgroup.mem_bot] at hn

47 subst n

48 simp only [mul_one, mul_inv_cancel, one_mem]))

50/--

51The identity completed-group-algebra open normal subgroup coerces to the corresponding open

52subgroup.

53-/

54@[simp]

55theorem identityCompletedGroupAlgebraOpenNormalSubgroup_coe

56 (G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G] :

57 ((identityCompletedGroupAlgebraOpenNormalSubgroup G : OpenNormalSubgroup G) :

58 Subgroup G) = ⊥ := rfl

60/--

61The identity quotient \(G/1\), as a completed-group-algebra index for a finite discrete group.

62-/

63def identityCompletedGroupAlgebraSubgroupInClass

64 (G : Type u) [Group G] [TopologicalSpace G]

65 [DiscreteTopology G] [Finite G] :

66 OpenNormalSubgroupInClass ProCGroups.FiniteGroupClass.allFinite G := by

67 refine ⟨identityCompletedGroupAlgebraOpenNormalSubgroup G, ?_⟩

68 change Finite

69 (G ⧸ ((identityCompletedGroupAlgebraOpenNormalSubgroup G : OpenNormalSubgroup G) :

70 Subgroup G))

71 rw [identityCompletedGroupAlgebraOpenNormalSubgroup_coe]

72 infer_instance

74/--

75The identity quotient \(G/1\), as a class-restricted completed-group-algebra stage whenever G

76itself lies in the finite-group class.

77-/

78def identityCompletedGroupAlgebraSubgroupInClassOfMem

79 (C : ProCGroups.FiniteGroupClass.{u})

80 (G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G]

81 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C) (hG : C G) :

82 OpenNormalSubgroupInClass C G := by

83 refine ⟨identityCompletedGroupAlgebraOpenNormalSubgroup G, ?_⟩

84 change C (G ⧸ (⊥ : Subgroup G))

85 exact hIso ⟨(QuotientGroup.quotientBot (G := G)).symm⟩ hG

87/-- The completed-group-algebra stage whose group quotient is \(G/1\). -/

88def identityCompletedGroupAlgebraIndex

89 (G : Type u) [Group G] [TopologicalSpace G]

90 [DiscreteTopology G] [Finite G] :

91 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G :=

92 OrderDual.toDual (identityCompletedGroupAlgebraSubgroupInClass G)

94/-- The class-restricted completed-group-algebra stage whose group quotient is \(G/1\). -/

95def identityCompletedGroupAlgebraIndexInClassOfMem

96 (C : ProCGroups.FiniteGroupClass.{u})

97 (G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G]

98 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C) (hG : C G) :

99 CompletedGroupAlgebraIndexInClass G C :=

100 OrderDual.toDual (identityCompletedGroupAlgebraSubgroupInClassOfMem C G hIso hG)

101

102/-- The projection to the identity completed stage is injective on group elements. -/

103theorem openNormalSubgroupInClassProj_identityCompletedGroupAlgebraIndex_injective

104 (G : Type u) [Group G] [TopologicalSpace G]

105 [DiscreteTopology G] [Finite G] :

106 Function.Injective

107 (openNormalSubgroupInClassProj

108 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)

109 (identityCompletedGroupAlgebraIndex G)) := by

110 intro g h hgh

111 change QuotientGroup.mk' (⊥ : Subgroup G) g =

112 QuotientGroup.mk' (⊥ : Subgroup G) h at hgh

113 have hdiv : g / h ∈ (⊥ : Subgroup G) :=

114 QuotientGroup.eq_iff_div_mem.mp hgh

115 exact div_eq_one.mp (Subgroup.mem_bot.mp hdiv)

116

117/--

118The projection to the class-restricted identity completed stage is injective on group elements.

119-/

120theorem openNormalSubgroupInClassProj_identityCompletedGAIndexInClassOfMem_inj

121 (C : ProCGroups.FiniteGroupClass.{u})

122 (G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G]

123 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C) (hG : C G) :

124 Function.Injective

125 (openNormalSubgroupInClassProj

126 (C := C) (G := G)

127 (identityCompletedGroupAlgebraIndexInClassOfMem C G hIso hG)) := by

128 intro g h hgh

129 change QuotientGroup.mk' (⊥ : Subgroup G) g =

130 QuotientGroup.mk' (⊥ : Subgroup G) h at hgh

131 have hdiv : g / h ∈ (⊥ : Subgroup G) :=

132 QuotientGroup.eq_iff_div_mem.mp hgh

133 exact div_eq_one.mp (Subgroup.mem_bot.mp hdiv)

134

135/-- The residue group-algebra stage map to the identity completed stage is injective. -/

136theorem modNCompletedGroupAlgebraStageMap_identityCompletedGroupAlgebraIndex_injective

137 (n : ℕ)

138 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

139 [DiscreteTopology G] [Finite G] :

140 Function.Injective

141 (modNCompletedGroupAlgebraStageMap n G

142 (identityCompletedGroupAlgebraIndex G)) := by

143 classical

144 change Function.Injective

145 (MonoidAlgebra.mapDomain

146 (R := ModNCompletedCoeff n)

147 (openNormalSubgroupInClassProj

148 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)

149 (identityCompletedGroupAlgebraIndex G)))

150 exact MonoidAlgebra.mapDomain_injective

151 (openNormalSubgroupInClassProj_identityCompletedGroupAlgebraIndex_injective G)

152

153/--

154The residue group-algebra stage map to the class-restricted identity completed stage is

155injective.

156-/

157theorem modNCompletedGAStageMapInClass_identityCompletedGAIndexInClassOfMem_inj

158 (n : ℕ) (C : ProCGroups.FiniteGroupClass.{u})

159 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

160 [DiscreteTopology G]

161 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C) (hG : C G) :

162 Function.Injective

163 (modNCompletedGroupAlgebraStageMapInClass n G C

164 (identityCompletedGroupAlgebraIndexInClassOfMem C G hIso hG)) := by

165 classical

166 change Function.Injective

167 (MonoidAlgebra.mapDomain

168 (R := ModNCompletedCoeff n)

169 (openNormalSubgroupInClassProj

170 (C := C) (G := G)

171 (identityCompletedGroupAlgebraIndexInClassOfMem C G hIso hG)))

172 exact MonoidAlgebra.mapDomain_injective

173 (openNormalSubgroupInClassProj_identityCompletedGAIndexInClassOfMem_inj

174 C G hIso hG)

175

176end

177

178end FoxDifferential