FoxDifferential.Completed.DifferentialModule.Identity
This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.
def identityCompletedGroupAlgebraOpenSubgroup
(G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G] :
OpenSubgroup G :=
OpenSubgroup.mk (⊥ : Subgroup G) (isOpen_discrete _)The identity completed-group-algebra open subgroup used for the identity quotient stage.
def identityCompletedGroupAlgebraOpenNormalSubgroup
(G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G] :
OpenNormalSubgroup G :=
OpenNormalSubgroup.mk (identityCompletedGroupAlgebraOpenSubgroup G)
(Subgroup.Normal.mk (by
intro n hn g
change n ∈ (⊥ : Subgroup G) at hn
rw [Subgroup.mem_bot] at hn
subst n
simp only [mul_one, mul_inv_cancel, one_mem]))The identity open normal subgroup of a discrete group.
theorem identityCompletedGroupAlgebraOpenNormalSubgroup_coe
(G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G] :
((identityCompletedGroupAlgebraOpenNormalSubgroup G : OpenNormalSubgroup G) :
Subgroup G) = ⊥The identity completed-group-algebra open normal subgroup coerces to the corresponding open subgroup.
Show proof
rflProof. Unfold the identity completed-group-algebra stage. The open normal subgroup is \(1\), so the quotient is \(G/1\) and the stage maps are the corresponding residue or class-restricted group-algebra maps. Injectivity and compatibility are checked on group-like basis elements and then extended by linearity; class membership is the stated finite-group-class hypothesis.
□def identityCompletedGroupAlgebraSubgroupInClass
(G : Type u) [Group G] [TopologicalSpace G]
[DiscreteTopology G] [Finite G] :
OpenNormalSubgroupInClass ProCGroups.FiniteGroupClass.allFinite G := by
refine ⟨identityCompletedGroupAlgebraOpenNormalSubgroup G, ?_⟩
change Finite
(G ⧸ ((identityCompletedGroupAlgebraOpenNormalSubgroup G : OpenNormalSubgroup G) :
Subgroup G))
rw [identityCompletedGroupAlgebraOpenNormalSubgroup_coe]
infer_instanceThe identity quotient \(G/1\), as a completed-group-algebra index for a finite discrete group.
def identityCompletedGroupAlgebraSubgroupInClassOfMem
(C : ProCGroups.FiniteGroupClass.{u})
(G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G]
(hIso : ProCGroups.FiniteGroupClass.IsomClosed C) (hG : C G) :
OpenNormalSubgroupInClass C G := by
refine ⟨identityCompletedGroupAlgebraOpenNormalSubgroup G, ?_⟩
change C (G ⧸ (⊥ : Subgroup G))
exact hIso ⟨(QuotientGroup.quotientBot (G := G)).symm⟩ hGThe identity quotient \(G/1\), as a class-restricted completed-group-algebra stage whenever G itself lies in the finite-group class.
def identityCompletedGroupAlgebraIndex
(G : Type u) [Group G] [TopologicalSpace G]
[DiscreteTopology G] [Finite G] :
_root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G :=
OrderDual.toDual (identityCompletedGroupAlgebraSubgroupInClass G)The completed-group-algebra stage whose group quotient is \(G/1\).
def identityCompletedGroupAlgebraIndexInClassOfMem
(C : ProCGroups.FiniteGroupClass.{u})
(G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G]
(hIso : ProCGroups.FiniteGroupClass.IsomClosed C) (hG : C G) :
CompletedGroupAlgebraIndexInClass G C :=
OrderDual.toDual (identityCompletedGroupAlgebraSubgroupInClassOfMem C G hIso hG)The class-restricted completed-group-algebra stage whose group quotient is \(G/1\).
theorem openNormalSubgroupInClassProj_identityCompletedGroupAlgebraIndex_injective
(G : Type u) [Group G] [TopologicalSpace G]
[DiscreteTopology G] [Finite G] :
Function.Injective
(openNormalSubgroupInClassProj
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
(identityCompletedGroupAlgebraIndex G))The projection to the identity completed stage is injective on group elements.
Show proof
by
intro g h hgh
change QuotientGroup.mk' (⊥ : Subgroup G) g =
QuotientGroup.mk' (⊥ : Subgroup G) h at hgh
have hbase := congrArg (QuotientGroup.quotientBot (G := G)) hgh
simpa using hbaseProof. Unfold the identity completed-group-algebra stage. The open normal subgroup is \(1\), so the quotient is \(G/1\) and the stage maps are the corresponding residue or class-restricted group-algebra maps. Injectivity and compatibility are checked on group-like basis elements and then extended by linearity; class membership is the stated finite-group-class hypothesis.
□theorem openNormalSubgroupInClassProj_identityCompletedGAIndexInClassOfMem_inj
(C : ProCGroups.FiniteGroupClass.{u})
(G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G]
(hIso : ProCGroups.FiniteGroupClass.IsomClosed C) (hG : C G) :
Function.Injective
(openNormalSubgroupInClassProj
(C := C) (G := G)
(identityCompletedGroupAlgebraIndexInClassOfMem C G hIso hG))The projection to the class-restricted identity completed stage is injective on group elements.
Show proof
by
intro g h hgh
change QuotientGroup.mk' (⊥ : Subgroup G) g =
QuotientGroup.mk' (⊥ : Subgroup G) h at hgh
have hbase := congrArg (QuotientGroup.quotientBot (G := G)) hgh
simpa using hbaseProof. Unfold the identity completed-group-algebra stage. The open normal subgroup is \(1\), so the quotient is \(G/1\) and the stage maps are the corresponding residue or class-restricted group-algebra maps. Injectivity and compatibility are checked on group-like basis elements and then extended by linearity; class membership is the stated finite-group-class hypothesis.
□theorem modNCompletedGroupAlgebraStageMap_identityCompletedGroupAlgebraIndex_injective
(n : ℕ)
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[DiscreteTopology G] [Finite G] :
Function.Injective
(modNCompletedGroupAlgebraStageMap n G
(identityCompletedGroupAlgebraIndex G))The residue group-algebra stage map to the identity completed stage is injective.
Show proof
by
classical
change Function.Injective
(MonoidAlgebra.mapDomain
(R := ModNCompletedCoeff n)
(openNormalSubgroupInClassProj
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
(identityCompletedGroupAlgebraIndex G)))
exact MonoidAlgebra.mapDomain_injective
(openNormalSubgroupInClassProj_identityCompletedGroupAlgebraIndex_injective G)Proof. Unfold the identity completed-group-algebra stage. The open normal subgroup is \(1\), so the quotient is \(G/1\) and the stage maps are the corresponding residue or class-restricted group-algebra maps. Injectivity and compatibility are checked on group-like basis elements and then extended by linearity; class membership is the stated finite-group-class hypothesis.
□theorem modNCompletedGAStageMapInClass_identityCompletedGAIndexInClassOfMem_inj
(n : ℕ) (C : ProCGroups.FiniteGroupClass.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[DiscreteTopology G]
(hIso : ProCGroups.FiniteGroupClass.IsomClosed C) (hG : C G) :
Function.Injective
(modNCompletedGroupAlgebraStageMapInClass n G C
(identityCompletedGroupAlgebraIndexInClassOfMem C G hIso hG))The residue group-algebra stage map to the class-restricted identity completed stage is injective.
Show proof
by
classical
change Function.Injective
(MonoidAlgebra.mapDomain
(R := ModNCompletedCoeff n)
(openNormalSubgroupInClassProj
(C := C) (G := G)
(identityCompletedGroupAlgebraIndexInClassOfMem C G hIso hG)))
exact MonoidAlgebra.mapDomain_injective
(openNormalSubgroupInClassProj_identityCompletedGAIndexInClassOfMem_inj
C G hIso hG)Proof. Unfold the identity completed-group-algebra stage. The open normal subgroup is \(1\), so the quotient is \(G/1\) and the stage maps are the corresponding residue or class-restricted group-algebra maps. Injectivity and compatibility are checked on group-like basis elements and then extended by linearity; class membership is the stated finite-group-class hypothesis.
□