ProCGroups.FoxDifferential.Completed.DifferentialModule.Identity

5 Theorems | 6 Definitions

The principal declarations in this module are:

identityCompletedGroupAlgebraOpenSubgroup The identity completed-group-algebra open subgroup used for the identity quotient stage. - identityCompletedGroupAlgebraOpenNormalSubgroup The identity open normal subgroup of a discrete group. - identityCompletedGroupAlgebraOpenNormalSubgroup_coe The identity completed-group-algebra open normal subgroup coerces to the corresponding open subgroup. - openNormalSubgroupInClassProj_identityCompletedGroupAlgebraIndex_injective The projection to the identity completed stage is injective on group elements.

import

ProCGroups.FoxDifferential.Completed.FiniteStage.Bifiltered.InverseSystem

Imported by

Definition FoxDifferential.identityCompletedGroupAlgebraOpenSubgroup

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.

Definition FoxDifferential.identityCompletedGroupAlgebraOpenNormalSubgroup

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 FoxDifferential.identityCompletedGroupAlgebraOpenNormalSubgroup_coe

@[simp]
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 Lean proof

Definition FoxDifferential.identityCompletedGroupAlgebraSubgroupInClass

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_instance

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

Definition FoxDifferential.identityCompletedGroupAlgebraSubgroupInClassOfMem

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⟩ hG

The identity quotient \(G/1\), as a class-restricted completed-group-algebra stage whenever G itself lies in the finite-group class.

Definition FoxDifferential.identityCompletedGroupAlgebraIndex

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\).

Definition FoxDifferential.identityCompletedGroupAlgebraIndexInClassOfMem

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 FoxDifferential.openNormalSubgroupInClassProj_identityCompletedGroupAlgebraIndex_injective

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 Lean proof

Theorem FoxDifferential.openNormalSubgroupInClassProj_identityCompletedGAIndexInClassOfMem_inj

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 Lean proof

Theorem FoxDifferential.modNCompletedGroupAlgebraStageMap_identityCompletedGroupAlgebraIndex_injective

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 Lean proof

Theorem FoxDifferential.modNCompletedGAStageMapInClass_identityCompletedGAIndexInClassOfMem_inj

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 Lean proof

ProCGroups.FoxDifferential.Completed.DifferentialModule.Identity

Declarations