ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Basic

8 Theorems | 5 Definitions | 4 Abbreviations

The principal declarations in this module are:

ModNCompletedCoeff The coefficient ring \(\mathbb{Z}/n\mathbb{Z}\) used in one residue-coefficient stage. - ModNCompletedGroupRing The group ring \((\mathbb{Z}/n\mathbb{Z})[H]\) used in the residue-coefficient tower. - finite_modNCompletedGroupAlgebraStageInClass Each \(C\)-indexed finite stage of the mod-\(n\) completed group algebra is finite. - modNCompletedGroupAlgebraTransitionInClass_of The transition map sends a group-like basis element to the basis element supported at its image in the coarser quotient in the Fox differential construction.

imports

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebra
Mathlib.Data.ZMod.Basic

Imported by

Abbreviation FoxDifferential.ModNCompletedCoeff

omit [Fact (0 < n)] in
abbrev ModNCompletedCoeff : Type := ZMod n

The coefficient ring \(\mathbb{Z}/n\mathbb{Z}\) used in one residue-coefficient stage.

Abbreviation FoxDifferential.ModNCompletedGroupRing

omit [Fact (0 < n)] in
abbrev ModNCompletedGroupRing (H : Type*) : Type _ :=
  MonoidAlgebra (ModNCompletedCoeff n) H

The group ring \((\mathbb{Z}/n\mathbb{Z})[H]\) used in the residue-coefficient tower.

Abbreviation FoxDifferential.ModNCompletedGroupAlgebraStageInClass

omit [Fact (0 < n)] in
abbrev ModNCompletedGroupAlgebraStageInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) : Type _ :=
  ModNCompletedGroupRing n (CompletedGroupAlgebraQuotientInClass G C U)

The residue-coefficient stage over a class-restricted finite quotient \(G/U\).

Theorem FoxDifferential.finite_modNCompletedGroupAlgebraStageInClass

theorem finite_modNCompletedGroupAlgebraStageInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Finite (ModNCompletedGroupAlgebraStageInClass n G C U)

Each \(C\)-indexed finite stage of the mod-\(n\) completed group algebra is finite.

Show Lean proof

Definition FoxDifferential.modNCompletedGroupAlgebraTransitionInClass

omit [Fact (0 < n)] in
def modNCompletedGroupAlgebraTransitionInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
    ModNCompletedGroupAlgebraStageInClass n G C V →+*
      ModNCompletedGroupAlgebraStageInClass n G C U :=
  MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n)
    (OpenNormalSubgroupInClass.map
      (C := C) (G := G)
      (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)

The transition map between class-restricted residue-coefficient stages.

Theorem FoxDifferential.modNCompletedGroupAlgebraTransitionInClass_of

omit [Fact (0 < n)] in
@[simp]
theorem modNCompletedGroupAlgebraTransitionInClass_of
    (C : ProCGroups.FiniteGroupClass.{u})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
    (g : CompletedGroupAlgebraQuotientInClass G C V) :
    modNCompletedGroupAlgebraTransitionInClass n G C hUV
        (MonoidAlgebra.of (ModNCompletedCoeff n) _ g) =
      MonoidAlgebra.single
        ((OpenNormalSubgroupInClass.map
          (C := C) (G := G)
          (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) g) 1

The transition map sends a group-like basis element to the basis element supported at its image in the coarser quotient in the Fox differential construction.

Show Lean proof

Theorem FoxDifferential.modNCompletedGroupAlgebraTransitionInClass_single

omit [Fact (0 < n)] in
@[simp]
theorem modNCompletedGroupAlgebraTransitionInClass_single
    (C : ProCGroups.FiniteGroupClass.{u})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
    (q : CompletedGroupAlgebraQuotientInClass G C V)
    (a : ModNCompletedCoeff n) :
    modNCompletedGroupAlgebraTransitionInClass n G C hUV
        (MonoidAlgebra.single q a) =
      MonoidAlgebra.single
        ((OpenNormalSubgroupInClass.map
          (C := C) (G := G)
          (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) a

The \(C\)-indexed transition map between finite stages sends a singleton supported at a class of the finer quotient to the singleton supported at its image in the coarser quotient, preserving the coefficient.

Show Lean proof

Theorem FoxDifferential.modNCompletedGroupAlgebraTransitionInClass_id

omit [Fact (0 < n)] in
@[simp]
theorem modNCompletedGroupAlgebraTransitionInClass_id
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
    modNCompletedGroupAlgebraTransitionInClass n G C (le_rfl : U ≤ U) = RingHom.id _

The transition map attached to the identity refinement is the identity homomorphism in the Fox differential construction.

Show Lean proof

Theorem FoxDifferential.modNCompletedGroupAlgebraTransitionInClass_comp

omit [Fact (0 < n)] in
@[simp]
theorem modNCompletedGroupAlgebraTransitionInClass_comp
    (C : ProCGroups.FiniteGroupClass.{u})
    {U V W : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) (hVW : V ≤ W) :
    (modNCompletedGroupAlgebraTransitionInClass n G C hUV).comp
        (modNCompletedGroupAlgebraTransitionInClass n G C hVW) =
      modNCompletedGroupAlgebraTransitionInClass n G C (hUV.trans hVW)

Class-indexed mod-\(n\) completed group-algebra transitions compose along quotient refinements.

Show Lean proof

Definition FoxDifferential.modNCompletedGroupAlgebraSystemInClass

omit [Fact (0 < n)] in
def modNCompletedGroupAlgebraSystemInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    InverseSystem (I := CompletedGroupAlgebraIndexInClass G C) where
  X := ModNCompletedGroupAlgebraStageInClass n G C
  topologicalSpace := fun _ => ⊥
  map := fun {U V} hUV => modNCompletedGroupAlgebraTransitionInClass n G C hUV
  continuous_map := by
    intro U V hUV
    letI : TopologicalSpace (ModNCompletedGroupAlgebraStageInClass n G C U) := ⊥
    letI : TopologicalSpace (ModNCompletedGroupAlgebraStageInClass n G C V) := ⊥
    letI : DiscreteTopology (ModNCompletedGroupAlgebraStageInClass n G C V) := ⟨rfl⟩
    exact continuous_of_discreteTopology
  map_id := by
    intro U
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (modNCompletedGroupAlgebraTransitionInClass_id n G C U)) x
  map_comp := by
    intro U V W hUV hVW
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (modNCompletedGroupAlgebraTransitionInClass_comp n G C hUV hVW)) x

The class-restricted inverse system \(U \mapsto (\mathbb{Z}/n\mathbb{Z})[G/U]\).

Theorem FoxDifferential.modNCompletedGroupAlgebraTransitionInClass_surjective

omit [Fact (0 < n)] in
theorem modNCompletedGroupAlgebraTransitionInClass_surjective
    (C : ProCGroups.FiniteGroupClass.{u})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
    Function.Surjective (modNCompletedGroupAlgebraTransitionInClass n G C hUV)

The finite-stage transition map is surjective, with preimages obtained by lifting quotient representatives.

Show Lean proof

Definition FoxDifferential.modNCompletedGroupAlgebraStageMapInClass

omit [Fact (0 < n)] in
def modNCompletedGroupAlgebraStageMapInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
    ModNCompletedGroupRing n G →+* ModNCompletedGroupAlgebraStageInClass n G C U :=
  MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n)
    (openNormalSubgroupInClassProj (C := C) (G := G) U)

The quotient map \((\mathbb{Z}/n\mathbb{Z})[G] \to (\mathbb{Z}/n\mathbb{Z})[G/U]\) for a class-restricted stage.

Theorem FoxDifferential.modNCompletedGroupAlgebraStageMapInClass_of

omit [Fact (0 < n)] in
@[simp]
theorem modNCompletedGroupAlgebraStageMapInClass_of
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) (g : G) :
    modNCompletedGroupAlgebraStageMapInClass n G C U
        (MonoidAlgebra.of (ModNCompletedCoeff n) _ g) =
      MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) 1

The finite-stage group-like map sends a group element to the corresponding singleton basis element in the quotient group algebra in the Fox differential construction.

Show Lean proof

Theorem FoxDifferential.modNCompletedGroupAlgebraStageMapInClass_compatible

omit [Fact (0 < n)] in
@[simp]
theorem modNCompletedGroupAlgebraStageMapInClass_compatible
    (C : ProCGroups.FiniteGroupClass.{u})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
    (modNCompletedGroupAlgebraTransitionInClass n G C hUV).comp
        (modNCompletedGroupAlgebraStageMapInClass n G C V) =
      modNCompletedGroupAlgebraStageMapInClass n G C U

The class-restricted mod-\(n\) completed group-algebra stage maps are compatible with quotient refinement.

Show Lean proof

Definition FoxDifferential.ModNCompletedGroupAlgebraCompatibleInClass

omit [Fact (0 < n)] in
def ModNCompletedGroupAlgebraCompatibleInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (x : ∀ U : CompletedGroupAlgebraIndexInClass G C,
      ModNCompletedGroupAlgebraStageInClass n G C U) : Prop :=
  (modNCompletedGroupAlgebraSystemInClass n G C).Compatible x

Compatibility for a class-restricted residue-coefficient completed group algebra family.

Abbreviation FoxDifferential.ModNCompletedGroupAlgebraInClass

omit [Fact (0 < n)] in
abbrev ModNCompletedGroupAlgebraInClass (C : ProCGroups.FiniteGroupClass.{u}) : Type _ :=
  {x : ∀ U : CompletedGroupAlgebraIndexInClass G C,
      ModNCompletedGroupAlgebraStageInClass n G C U //
    ModNCompletedGroupAlgebraCompatibleInClass n G C x}

The class-restricted residue-coefficient completed group algebra as an inverse-limit subtype.

Definition FoxDifferential.modNCompletedGroupAlgebraProjectionInClass

omit [Fact (0 < n)] in
def modNCompletedGroupAlgebraProjectionInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
    ModNCompletedGroupAlgebraInClass n G C →
      ModNCompletedGroupAlgebraStageInClass n G C U :=
  (modNCompletedGroupAlgebraSystemInClass n G C).projection U

The projection from the class-restricted residue-coefficient completed group algebra to a stage.

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Basic

Declarations