Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Basic
ProCGroups/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/System/Basic

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Basic

11 Theorems | 4 Definitions | 2 Abbreviations

The principal declarations in this module are:

  • PrimePowerCompletedGroupAlgebraStageInClass The class-restricted prime-power stage at index \((a,U)\), namely \((\mathrm{ZMod}\,\ell^a)[G/U]\). - primePowerCompletedGroupAlgebraTransitionInClass The combined transition map for class-restricted prime-power stage calculus. - finite_primePowerCompletedGroupAlgebraStageInClass Each class-indexed prime-power finite stage is finite. - primePowerCompletedGroupAlgebraTransitionInClass_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
Imported by

Declarations

Abbreviation FoxDifferential.PrimePowerCompletedGroupAlgebraStageInClass 
omit [Fact (0 < ℓ)] in
abbrev PrimePowerCompletedGroupAlgebraStageInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
    Type _ :=
  ModNCompletedGroupAlgebraStageInClass (ℓ ^ i.1) G C i.2

The class-restricted prime-power stage at index \((a,U)\), namely \((\mathrm{ZMod}\,\ell^a)[G/U]\).

Theorem FoxDifferential.finite_primePowerCompletedGroupAlgebraStageInClass 
theorem finite_primePowerCompletedGroupAlgebraStageInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
    Finite (PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i)

Each class-indexed prime-power finite stage is finite.

Show Lean proof
Definition FoxDifferential.primePowerCompletedGroupAlgebraTransitionInClass 
omit [Fact (0 < ℓ)] in
def primePowerCompletedGroupAlgebraTransitionInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j) :
    PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j →+*
      PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i := by
  exact
    (modNCompletedGroupAlgebraStageCoeffMapInClass
        (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C i.2
        (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
      (modNCompletedGroupAlgebraTransitionInClass (n := ℓ ^ j.1) (G := G) C hij.2)

The combined transition map for class-restricted prime-power stage calculus.

Theorem FoxDifferential.primePowerCompletedGroupAlgebraTransitionInClass_of 
omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraTransitionInClass_of
    (C : ProCGroups.FiniteGroupClass.{u})
    {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j)
    (q : CompletedGroupAlgebraQuotientInClass G C j.2) :
    primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
        (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ j.1)) _ q) =
      MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1)) _
        ((OpenNormalSubgroupInClass.map
          (C := C) (G := G)
          (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)

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.primePowerCompletedGroupAlgebraTransitionInClass_single 
omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraTransitionInClass_single
    (C : ProCGroups.FiniteGroupClass.{u})
    {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j)
    (q : CompletedGroupAlgebraQuotientInClass G C j.2)
    (a : ModNCompletedCoeff (ℓ ^ j.1)) :
    primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
        (MonoidAlgebra.single q a) =
      MonoidAlgebra.single
        ((OpenNormalSubgroupInClass.map
          (C := C) (G := G)
          (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)
        (modNCompletedCoeffMap
          (n := ℓ ^ i.1) (m := ℓ ^ j.1)
          (primePow_dvd_primePow (ℓ := ℓ) hij.1) 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.primePowerCompletedGroupAlgebraTransitionInClass_eq 
omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraTransitionInClass_eq
    (C : ProCGroups.FiniteGroupClass.{u})
    {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j) :
    primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij =
      (modNCompletedGroupAlgebraStageCoeffMapInClass
          (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C i.2
          (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
        (modNCompletedGroupAlgebraTransitionInClass (ℓ ^ j.1) G C hij.2)

The transition map for the prime-power completed group algebra commutes with the finite-stage coordinate maps.

Show Lean proof
Theorem FoxDifferential.primePowerCompletedGroupAlgebraTransitionInClass_eq' 
omit [Fact (0 < ℓ)] in
theorem primePowerCompletedGroupAlgebraTransitionInClass_eq'
    (C : ProCGroups.FiniteGroupClass.{u})
    {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j) :
    primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij =
      (modNCompletedGroupAlgebraTransitionInClass (ℓ ^ i.1) G C hij.2).comp
        (modNCompletedGroupAlgebraStageCoeffMapInClass
          (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C j.2
          (primePow_dvd_primePow (ℓ := ℓ) hij.1))

The class-indexed prime-power transition agrees with the explicit coefficient-and-quotient transition formula.

Show Lean proof
Theorem FoxDifferential.primePowerCompletedGroupAlgebraTransitionInClass_id 
omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraTransitionInClass_id
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
    primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C
        (le_rfl : i ≤ i) =
      RingHom.id _

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

Show Lean proof
Theorem FoxDifferential.primePowerCompletedGroupAlgebraTransitionInClass_comp 
omit [Fact (0 < ℓ)] in
@[simp 900]
theorem primePowerCompletedGroupAlgebraTransitionInClass_comp
    (C : ProCGroups.FiniteGroupClass.{u})
    {i j k : PrimePowerCompletedGroupAlgebraIndexInClass G C}
    (hij : i ≤ j) (hjk : j ≤ k) :
    (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij).comp
        (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hjk) =
      primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C
        (hij.trans hjk)

Class-indexed prime-power completed group-algebra transitions compose along quotient refinements.

Show Lean proof
Theorem FoxDifferential.primePowerCompletedGroupAlgebraStageAugmentationInClass_comp_transition 
omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraStageAugmentationInClass_comp_transition
    (C : ProCGroups.FiniteGroupClass.{u})
    {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j) :
    (modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ i.1) G C i.2).comp
        (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij) =
      (modNCompletedCoeffMap
          (n := ℓ ^ i.1) (m := ℓ ^ j.1)
          (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
        (modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ j.1) G C j.2)

Class-indexed finite-stage prime-power augmentation is compatible with transition maps and coefficient reduction.

Show Lean proof
Definition FoxDifferential.primePowerCompletedGroupAlgebraSystemInClass 
omit [Fact (0 < ℓ)] in
def primePowerCompletedGroupAlgebraSystemInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    InverseSystem (I := PrimePowerCompletedGroupAlgebraIndexInClass G C) where
  X := PrimePowerCompletedGroupAlgebraStageInClass ℓ G C
  topologicalSpace := fun _ => ⊥
  map := fun {i j} hij =>
    primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
  continuous_map := by
    intro i j hij
    letI : TopologicalSpace (PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) := ⊥
    letI : TopologicalSpace (PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j) := ⊥
    letI : DiscreteTopology (PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j) := ⟨rfl⟩
    exact continuous_of_discreteTopology
  map_id := by
    intro i
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (primePowerCompletedGroupAlgebraTransitionInClass_id
          (ℓ := ℓ) (G := G) C i)) x
  map_comp := by
    intro i j k hij hjk
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (primePowerCompletedGroupAlgebraTransitionInClass_comp
          (ℓ := ℓ) (G := G) C hij hjk)) x

The class-restricted inverse system indexed by prime powers and \(C\)-quotients.

Theorem FoxDifferential.directed_primePowerCompletedGroupAlgebraIndexInClass 
omit [IsTopologicalGroup G] in
theorem directed_primePowerCompletedGroupAlgebraIndexInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (hForm : ProCGroups.FiniteGroupClass.Formation C) :
    Directed (· ≤ ·) (id : PrimePowerCompletedGroupAlgebraIndexInClass G C →
      PrimePowerCompletedGroupAlgebraIndexInClass G C)

The class-restricted prime-power group-algebra index family is directed under componentwise order when \(C\) is a formation.

Show Lean proof
Theorem FoxDifferential.primePowerCompletedGroupAlgebraTransitionInClass_surjective 
omit [Fact (0 < ℓ)] in
theorem primePowerCompletedGroupAlgebraTransitionInClass_surjective
    (C : ProCGroups.FiniteGroupClass.{u})
    {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j) :
    Function.Surjective
      (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij)

Every transition in the class-restricted prime-power completed group-algebra system is surjective.

Show Lean proof
Definition FoxDifferential.PrimePowerCompletedGroupAlgebraCompatibleInClass 
omit [Fact (0 < ℓ)] in
def PrimePowerCompletedGroupAlgebraCompatibleInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (x : ∀ i : PrimePowerCompletedGroupAlgebraIndexInClass G C,
      PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) : Prop :=
  (primePowerCompletedGroupAlgebraSystemInClass ℓ G C).Compatible x

Compatibility for a class-restricted prime-power completed group algebra family.

Abbreviation FoxDifferential.PrimePowerCompletedGroupAlgebraInClass 
omit [Fact (0 < ℓ)] in
abbrev PrimePowerCompletedGroupAlgebraInClass (C : ProCGroups.FiniteGroupClass.{u}) : Type _ :=
  {x : ∀ i : PrimePowerCompletedGroupAlgebraIndexInClass G C,
      PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i //
    PrimePowerCompletedGroupAlgebraCompatibleInClass (ℓ := ℓ) (G := G) C x}

The class-restricted prime-power completed group algebra as an inverse-limit subtype. The all-finite PrimePowerCompletedGroupAlgebra below remains the ringed concrete formulation; this type is the class-indexed completed object that later Fox layers should target.

Definition FoxDifferential.primePowerCompletedGroupAlgebraProjectionInClass 
omit [Fact (0 < ℓ)] in
def primePowerCompletedGroupAlgebraProjectionInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
    PrimePowerCompletedGroupAlgebraInClass ℓ G C →
      PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i :=
  (primePowerCompletedGroupAlgebraSystemInClass ℓ G C).projection i

The projection from the class-restricted completed group algebra to a prime-power stage.

Theorem FoxDifferential.primePowerCompletedGroupAlgebraProjectionInClass_surjective 
theorem primePowerCompletedGroupAlgebraProjectionInClass_surjective
    (C : ProCGroups.FiniteGroupClass.{u})
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
    Function.Surjective
      (primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i)

Every finite-stage projection from the class-restricted prime-power completed group algebra is surjective when \(C\) is a formation of finite quotient groups.

Show Lean proof