ProCGroups.FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.LimitEquiv

13 Theorems | 3 Definitions

The principal declarations in this module are:

toPrimePowerCompletedGroupAlgebraAugmentationIdeal A prime-power augmentation-kernel point determines a compatible family in the finite-stage augmentation ideals. - ofPrimePowerCompletedGroupAlgebraAugmentationIdeal A compatible family of prime-power finite-stage augmentation-ideal elements determines a prime-power augmentation-kernel point. - primePowerCompletedGroupAlgebraAugmentationIdealProjection_zero The finite-stage augmentation-ideal projection is compatible with zero. - primePowerCompletedGroupAlgebraAugmentationIdealProjection_add The finite-stage augmentation-ideal projection is compatible with addition.

import

ProCGroups.FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Module

Imported by

Theorem FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealProjection_zero

omit [Fact (0 < ℓ)] in
theorem primePowerCompletedGroupAlgebraAugmentationIdealProjection_zero
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i
        (0 : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) = 0

The finite-stage augmentation-ideal projection is compatible with zero.

Show Lean proof

Theorem FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealProjection_add

omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraAugmentationIdealProjection_add
    (i : PrimePowerCompletedGroupAlgebraIndex G)
    (x y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
    primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (x + y) =
      primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i x +
        primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i y

The finite-stage augmentation-ideal projection is compatible with addition.

Show Lean proof

Theorem FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealProjection_neg

omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraAugmentationIdealProjection_neg
    (i : PrimePowerCompletedGroupAlgebraIndex G)
    (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
    primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (-x) =
      -primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i x

The finite-stage augmentation-ideal projection is compatible with negation.

Show Lean proof

Theorem FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealProjection_sub

omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraAugmentationIdealProjection_sub
    (i : PrimePowerCompletedGroupAlgebraIndex G)
    (x y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
    primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (x - y) =
      primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i x -
        primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i y

The finite-stage augmentation-ideal projection is compatible with subtraction.

Show Lean proof

Theorem FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealProjection_nsmul

omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraAugmentationIdealProjection_nsmul
    (i : PrimePowerCompletedGroupAlgebraIndex G)
    (m : ℕ) (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
    primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (m • x) =
      m • primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i x

The finite-stage augmentation-ideal projection is compatible with natural-number scalar multiplication.

Show Lean proof

Theorem FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealProjection_zsmul

omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraAugmentationIdealProjection_zsmul
    (i : PrimePowerCompletedGroupAlgebraIndex G)
    (m : ℤ) (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
    primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (m • x) =
      m • primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i x

The finite-stage augmentation-ideal projection is compatible with integer scalar multiplication.

Show Lean proof

Theorem FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealProjection_smul

omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraAugmentationIdealProjection_smul
    (i : PrimePowerCompletedGroupAlgebraIndex G)
    (a : PrimePowerCompletedCoeff ℓ G)
    (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
    primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (a • x) =
      (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
        primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i x

The finite-stage augmentation-ideal projection is compatible with scalar multiplication.

Show Lean proof

Definition FoxDifferential.toPrimePowerCompletedGroupAlgebraAugmentationIdeal

def toPrimePowerCompletedGroupAlgebraAugmentationIdeal :
    PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G) →
      PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G := by
  intro x
  refine ⟨fun i => ⟨primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x.1, ?_⟩, ?_⟩
  · exact (mem_primePowerCompletedGroupAlgebraStageAugmentationIdeal_iff
      (ℓ := ℓ) (G := G) (i := i)
      (x := primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x.1)).2
      ((mem_primePowerCompletedGroupAlgebraAugmentationKernel_iff_forall
        (ℓ := ℓ) (G := G) (x := x.1)).1 x.2 i)
  · intro i j hij
    apply Subtype.ext
    exact (primePowerCompletedGroupAlgebraSystem ℓ G).projection_compatible x.1 i j hij

A prime-power augmentation-kernel point determines a compatible family in the finite-stage augmentation ideals.

Theorem FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealProjection_to

omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraAugmentationIdealProjection_to
    (x : PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G))
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    ((primePowerCompletedGroupAlgebraAugmentationIdealProjection
        (ℓ := ℓ) (G := G) i
        (toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) x)) :
      PrimePowerCompletedGroupAlgebraStage ℓ G i) =
      primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x.1

The projection-to-stage map is one direction of the completed augmentation-ideal stage equivalence.

Show Lean proof

Definition FoxDifferential.ofPrimePowerCompletedGroupAlgebraAugmentationIdeal

def ofPrimePowerCompletedGroupAlgebraAugmentationIdeal :
    PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G →
      PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G) := by
  intro x
  let y : PrimePowerCompletedGroupAlgebra ℓ G := ⟨fun i => (x.1 i).1, by
    intro i j hij
    exact congrArg Subtype.val (x.2 i j hij)⟩
  refine ⟨y, ?_⟩
  exact (mem_primePowerCompletedGroupAlgebraAugmentationKernel_iff_forall
    (ℓ := ℓ) (G := G) (x := y)).2 (fun i =>
      (mem_primePowerCompletedGroupAlgebraStageAugmentationIdeal_iff
        (ℓ := ℓ) (G := G) (i := i) (x := (x.1 i).1)).1 (x.1 i).2)

A compatible family of prime-power finite-stage augmentation-ideal elements determines a prime-power augmentation-kernel point.

Theorem FoxDifferential.primePowerCompletedGroupAlgebraProjection_ofAugmentationIdeal

omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraProjection_ofAugmentationIdeal
    (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G)
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
        (ofPrimePowerCompletedGroupAlgebraAugmentationIdeal
          (ℓ := ℓ) (G := G) x).1 =
      ((primePowerCompletedGroupAlgebraAugmentationIdealProjection
          (ℓ := ℓ) (G := G) i x) :
        PrimePowerCompletedGroupAlgebraStage ℓ G i)

Projecting an element of the completed augmentation ideal gives its corresponding finite-stage augmentation-ideal coordinate.

Show Lean proof

Theorem FoxDifferential.ofPrimePowerCompletedGroupAlgebraAugmentationIdeal_to

omit [Fact (0 < ℓ)] in
@[simp]
theorem ofPrimePowerCompletedGroupAlgebraAugmentationIdeal_to
    (x : PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G)) :
    ofPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G)
        (toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) x) = x

The completion-to-stage map is one direction of the completed augmentation-ideal stage equivalence.

Show Lean proof

Theorem FoxDifferential.toPrimePowerCompletedGroupAlgebraAugmentationIdeal_of

omit [Fact (0 < ℓ)] in
@[simp]
theorem toPrimePowerCompletedGroupAlgebraAugmentationIdeal_of
    (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
    toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G)
        (ofPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) x) = x

The stage-to-completion map is one direction of the completed augmentation-ideal stage equivalence.

Show Lean proof

Definition FoxDifferential.primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit

def primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit :
    PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G) ≃
      PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G where
  toFun := toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G)
  invFun := ofPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G)
  left_inv := ofPrimePowerCompletedGroupAlgebraAugmentationIdeal_to (ℓ := ℓ) (G := G)
  right_inv := toPrimePowerCompletedGroupAlgebraAugmentationIdeal_of (ℓ := ℓ) (G := G)

The prime-power completed augmentation kernel is canonically equivalent to the inverse limit of the prime-power finite-stage augmentation ideals.

Theorem FoxDifferential.primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_apply

omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_apply
    (x : PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G)) :
    primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit
        (ℓ := ℓ) (G := G) x =
      toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) x

The forward augmentation-kernel equivalence is the canonical map to the inverse-limit augmentation ideal.

Show Lean proof

Theorem FoxDifferential.primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_symm_apply

omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_symm_apply
    (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
    (primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit
        (ℓ := ℓ) (G := G)).symm x =
      ofPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) x

The inverse augmentation-kernel equivalence reconstructs a kernel element from an inverse-limit augmentation-ideal element.

Show Lean proof

ProCGroups.FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.LimitEquiv

Declarations