ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.Augmentation

5 Theorems | 4 Definitions | 2 Abbreviations

The principal declarations in this module are:

modNCompletedGroupAlgebraCoeffMap The modulus-direction map on residue-coefficient completed group algebras. - modNCompletedGroupAlgebraAugmentationKernelCoeffMap Coefficient change is performed stagewise: supports are unchanged and coefficients are transported by the given ring homomorphism. - modNCompletedGroupAlgebraProjection_coeffMap The mod-\(n\) completed group-algebra projection commutes with the coefficient map. - modNCompletedGroupAlgebraStageAugmentation_comp_coeffMap Finite-stage augmentation commutes with coefficient reduction.

imports

Imported by

Definition FoxDifferential.modNCompletedGroupAlgebraCoeffMap

def modNCompletedGroupAlgebraCoeffMap (hnm : n ∣ m) :
    ModNCompletedGroupAlgebra m G → ModNCompletedGroupAlgebra n G := by
  intro x
  refine ⟨fun U =>
      modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm (x.1 U), ?_⟩
  intro U V hUV
  calc
    modNCompletedGroupAlgebraTransition n G hUV
        (modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) V hnm (x.1 V))
      =
    modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm
      (modNCompletedGroupAlgebraTransition m G hUV (x.1 V)) := by
        symm
        exact congrFun
          (congrArg DFunLike.coe
            (modNCompletedGroupAlgebraStageCoeffMap_compatible
              (n := n) (m := m) (G := G) hUV hnm)) (x.1 V)
    _ =
      modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm (x.1 U) := by
        exact congrArg
          (modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm)
          (x.2 U V hUV)

The modulus-direction map on residue-coefficient completed group algebras.

Theorem FoxDifferential.modNCompletedGroupAlgebraProjection_coeffMap

omit [Fact (0 < n)] [Fact (0 < m)] in
@[simp]
theorem modNCompletedGroupAlgebraProjection_coeffMap
    (hnm : n ∣ m) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G)
    (x : ModNCompletedGroupAlgebra m G) :
    modNCompletedGroupAlgebraProjection n G U
        (modNCompletedGroupAlgebraCoeffMap (n := n) (m := m) (G := G) hnm x) =
      modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm
        (modNCompletedGroupAlgebraProjection m G U x)

The mod-\(n\) completed group-algebra projection commutes with the coefficient map.

Show Lean proof

Theorem FoxDifferential.modNCompletedGroupAlgebraStageAugmentation_comp_coeffMap

omit [Fact (0 < n)] [Fact (0 < m)] in
@[simp 900]
theorem modNCompletedGroupAlgebraStageAugmentation_comp_coeffMap
    (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (hnm : n ∣ m) :
    (modNCompletedGroupAlgebraStageAugmentation n G U).comp
        (modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm) =
      (modNCompletedCoeffMap (n := n) (m := m) hnm).comp
        (modNCompletedGroupAlgebraStageAugmentation m G U)

Finite-stage augmentation commutes with coefficient reduction.

Show Lean proof

Theorem FoxDifferential.modNCompletedGroupAlgebraStageAugmentationInClass_comp_coeffMap

omit [Fact (0 < n)] [Fact (0 < m)] in
@[simp 900]
theorem modNCompletedGroupAlgebraStageAugmentationInClass_comp_coeffMap
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) (hnm : n ∣
        m) :
    (modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
        (modNCompletedGroupAlgebraStageCoeffMapInClass
          (n := n) (m := m) (G := G) C U hnm) =
      (modNCompletedCoeffMap (n := n) (m := m) hnm).comp
        (modNCompletedGroupAlgebraStageAugmentationInClass m G C U)

Class-indexed finite-stage augmentation commutes with coefficient reduction.

Show Lean proof

Theorem FoxDifferential.modNCompletedGroupAlgebraAugmentation_coeffMap

omit [Fact (0 < n)] [Fact (0 < m)] in
@[simp]
theorem modNCompletedGroupAlgebraAugmentation_coeffMap
    (hnm : n ∣ m) (x : ModNCompletedGroupAlgebra m G) :
    modNCompletedGroupAlgebraAugmentation n G
        (modNCompletedGroupAlgebraCoeffMap (n := n) (m := m) (G := G) hnm x) =
      modNCompletedCoeffMap (n := n) (m := m) hnm
        (modNCompletedGroupAlgebraAugmentation m G x)

Completed augmentation commutes with the coefficient-reduction map between moduli.

Show Lean proof

Definition FoxDifferential.modNCompletedGroupAlgebraAugmentationKernelCoeffMap

def modNCompletedGroupAlgebraAugmentationKernelCoeffMap
    (hnm : n ∣ m) :
    ModNCompletedGroupAlgebraAugmentationKernel m G →
      ModNCompletedGroupAlgebraAugmentationKernel n G := by
  intro x
  refine ⟨modNCompletedGroupAlgebraCoeffMap (n := n) (m := m) (G := G) hnm x.1, ?_⟩
  rw [mem_modNCompletedGroupAlgebraAugmentationKernel_iff,
    modNCompletedGroupAlgebraAugmentation_coeffMap]
  simpa [map_zero, modNCompletedCoeffMap] using
    congrArg (modNCompletedCoeffMap (n := n) (m := m) hnm) x.2

Coefficient change is performed stagewise: supports are unchanged and coefficients are transported by the given ring homomorphism.

Theorem FoxDifferential.primePow_dvd_primePow

theorem primePow_dvd_primePow
    (ℓ : ℕ) {a b : ℕ} (hab : a ≤ b) :
    ℓ ^ a ∣ ℓ ^ b

The standard divisibility relation between prime powers with the same base.

Show Lean proof

Definition FoxDifferential.primePowCompletedGroupAlgebraCoeffMap

def primePowCompletedGroupAlgebraCoeffMap
    (ℓ : ℕ) {a b : ℕ}
    (hab : a ≤ b) :
    ModNCompletedGroupAlgebra (ℓ ^ b) G → ModNCompletedGroupAlgebra (ℓ ^ a) G :=
  modNCompletedGroupAlgebraCoeffMap (n := ℓ ^ a) (m := ℓ ^ b) (G := G)
    (primePow_dvd_primePow (ℓ := ℓ) hab)

The modulus-direction completed map specialized to prime-power stages.

Definition FoxDifferential.primePowCompletedGroupAlgebraAugmentationKernelCoeffMap

def primePowCompletedGroupAlgebraAugmentationKernelCoeffMap
    (ℓ : ℕ) {a b : ℕ}
    (hab : a ≤ b) :
    ModNCompletedGroupAlgebraAugmentationKernel (ℓ ^ b) G →
      ModNCompletedGroupAlgebraAugmentationKernel (ℓ ^ a) G :=
  modNCompletedGroupAlgebraAugmentationKernelCoeffMap
    (n := ℓ ^ a) (m := ℓ ^ b) (G := G)
    (primePow_dvd_primePow (ℓ := ℓ) hab)

The coefficient map between prime-power stages restricts to a map on augmentation kernels.

Abbreviation FoxDifferential.PrimePowerCompletedGroupAlgebraIndex

abbrev PrimePowerCompletedGroupAlgebraIndex :=
  ℕ × _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G

The two-parameter index \((a,U)\) for the prime-power residue-coefficient stages.

Abbreviation FoxDifferential.PrimePowerCompletedGroupAlgebraIndexInClass

abbrev PrimePowerCompletedGroupAlgebraIndexInClass (C : ProCGroups.FiniteGroupClass.{u}) :=
  ℕ × CompletedGroupAlgebraIndexInClass G C

The two-parameter index \((a,U)\) for prime-power stages over a quotient class \(C\).

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.Augmentation

Declarations