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

8 Theorems | 2 Definitions | 3 Abbreviations | 1 Instance

The principal declarations in this module are:

PrimePowerCompletedGroupAlgebraStage The stage at index \((a,U)\), namely \((\mathrm{ZMod}\,\ell^a)[G/U]\). - primePowerCompletedGroupAlgebraTransition The combined transition map for the two-parameter prime-power stage calculus. - primePowerCompletedGroupAlgebraTransition_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. - primePowerCompletedGroupAlgebraTransition_eq The transition map for the prime-power completed group algebra commutes with the finite-stage coordinate maps.

imports

Imported by

Abbreviation FoxDifferential.PrimePowerCompletedGroupAlgebraStage

omit [Fact (0 < ℓ)] in
abbrev PrimePowerCompletedGroupAlgebraStage
    (i : PrimePowerCompletedGroupAlgebraIndex G) : Type _ :=
  ModNCompletedGroupAlgebraStage (ℓ ^ i.1) G i.2

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

Instance FoxDifferential.instFinitePrimePowerCompletedGroupAlgebraStage

instance instFinitePrimePowerCompletedGroupAlgebraStage
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    Finite (PrimePowerCompletedGroupAlgebraStage ℓ G i) := by
  letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
  exact instFiniteModNCompletedGroupAlgebraStage (n := ℓ ^ i.1) (G := G) i.2

Each prime-power completed group-algebra stage is finite.

Definition FoxDifferential.primePowerCompletedGroupAlgebraTransition

omit [Fact (0 < ℓ)] in
def primePowerCompletedGroupAlgebraTransition
    {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) :
    PrimePowerCompletedGroupAlgebraStage ℓ G j →+* PrimePowerCompletedGroupAlgebraStage ℓ G i := by
  exact
    (modNCompletedGroupAlgebraStageCoeffMap
        (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) i.2
        (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
      (modNCompletedGroupAlgebraTransition (ℓ ^ j.1) G hij.2)

The combined transition map for the two-parameter prime-power stage calculus.

Theorem FoxDifferential.primePowerCompletedGroupAlgebraTransition_of

omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraTransition_of
    {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j)
    (q : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G j.2) :
    primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
        (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ j.1)) _ q) =
      MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1)) _
        ((OpenNormalSubgroupInClass.map
          (C := ProCGroups.FiniteGroupClass.allFinite) (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.primePowerCompletedGroupAlgebraTransition_eq

omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraTransition_eq
    {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) :
    primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij =
      (modNCompletedGroupAlgebraStageCoeffMap
          (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) i.2
          (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
        (modNCompletedGroupAlgebraTransition (ℓ ^ j.1) G hij.2)

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

Show Lean proof

Theorem FoxDifferential.primePowerCompletedGroupAlgebraTransition_eq'

omit [Fact (0 < ℓ)] in
theorem primePowerCompletedGroupAlgebraTransition_eq'
    {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) :
    primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij =
      (modNCompletedGroupAlgebraTransition (ℓ ^ i.1) G hij.2).comp
        (modNCompletedGroupAlgebraStageCoeffMap
          (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) j.2
          (primePow_dvd_primePow (ℓ := ℓ) hij.1))

The same combined transition can also be read as coefficient reduction at the source stage followed by the quotient-direction transition at the smaller modulus.

Show Lean proof

Theorem FoxDifferential.primePowerCompletedGroupAlgebraTransition_id

omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraTransition_id
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) (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.primePowerCompletedGroupAlgebraTransition_comp

omit [Fact (0 < ℓ)] in
@[simp 900]
theorem primePowerCompletedGroupAlgebraTransition_comp
    {i j k : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) (hjk : j ≤ k) :
    (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij).comp
        (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hjk) =
      primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) (hij.trans hjk)

Prime-power completed group-algebra transitions compose along a chain of quotient refinements.

Show Lean proof

Definition FoxDifferential.primePowerCompletedGroupAlgebraSystem

omit [Fact (0 < ℓ)] in
def primePowerCompletedGroupAlgebraSystem :
    InverseSystem (I := PrimePowerCompletedGroupAlgebraIndex G) where
  X := PrimePowerCompletedGroupAlgebraStage ℓ G
  topologicalSpace := fun _ => ⊥
  map := fun {i j} hij => primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
  continuous_map := by
    intro i j hij
    letI : TopologicalSpace (PrimePowerCompletedGroupAlgebraStage ℓ G i) := ⊥
    letI : TopologicalSpace (PrimePowerCompletedGroupAlgebraStage ℓ G j) := ⊥
    letI : DiscreteTopology (PrimePowerCompletedGroupAlgebraStage ℓ G j) := ⟨rfl⟩
    exact continuous_of_discreteTopology
  map_id := by
    intro i
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (primePowerCompletedGroupAlgebraTransition_id (ℓ := ℓ) (G := G) i)) x
  map_comp := by
    intro i j k hij hjk
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (primePowerCompletedGroupAlgebraTransition_comp (ℓ := ℓ) (G := G) hij hjk)) x

The inverse system indexed by prime powers and finite quotients.

Abbreviation FoxDifferential.PrimePowerCompletedGroupAlgebra

omit [Fact (0 < ℓ)] in
abbrev PrimePowerCompletedGroupAlgebra :=
  (primePowerCompletedGroupAlgebraSystem ℓ G).inverseLimit

The inverse-limit object of the prime-power finite-stage system.

Abbreviation FoxDifferential.primePowerCompletedGroupAlgebraProjection

omit [Fact (0 < ℓ)] in
abbrev primePowerCompletedGroupAlgebraProjection (i : PrimePowerCompletedGroupAlgebraIndex G) :
    PrimePowerCompletedGroupAlgebra ℓ G → PrimePowerCompletedGroupAlgebraStage ℓ G i :=
  (primePowerCompletedGroupAlgebraSystem ℓ G).projection i

The projection from the prime-power completed group algebra to one finite stage.

Theorem FoxDifferential.directed_primePowerCompletedGroupAlgebraIndex

omit [IsTopologicalGroup G] in
theorem directed_primePowerCompletedGroupAlgebraIndex :
    Directed (· ≤ ·) (id : PrimePowerCompletedGroupAlgebraIndex G →
      PrimePowerCompletedGroupAlgebraIndex G)

The prime-power group-algebra index family is directed under the componentwise order.

Show Lean proof

Theorem FoxDifferential.primePowerCompletedGroupAlgebraTransition_surjective

omit [Fact (0 < ℓ)] in
theorem primePowerCompletedGroupAlgebraTransition_surjective
    {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) :
    Function.Surjective
      (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij)

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

Show Lean proof

Theorem FoxDifferential.primePowerCompletedGroupAlgebraProjection_surjective

theorem primePowerCompletedGroupAlgebraProjection_surjective
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    Function.Surjective (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i)

Every finite-stage projection from the prime-power completed group algebra is surjective.

Show Lean proof

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

Declarations