ProCGroups.FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Augmentation

15 Theorems | 6 Definitions | 1 Abbreviation

The principal declarations in this module are:

primePowerCompletedGroupAlgebraAugmentationAddHom The canonical prime-power augmentation as an additive homomorphism. - primePowerCompletedGroupAlgebraAugmentationRingHom The prime-power completed augmentation bundled as a ring homomorphism. - primePowerCompletedGroupAlgebraAugmentation_comp_coeffToGroupAlgebra The prime-power completed augmentation composed with the coefficient-to-group-algebra map is the identity. - mem_primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal_iff A prime-power completed group-algebra element lies in the augmentation ideal iff its prime-power augmentation is zero.

import

ProCGroups.FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.LimitEquiv

Imported by

Theorem FoxDifferential.primePowerCompletedGroupAlgebraAugmentation_comp_coeffToGroupAlgebra

omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraAugmentation_comp_coeffToGroupAlgebra
    (x : PrimePowerCompletedCoeff ℓ G) :
    primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G)
        (primePowerCompletedCoeffToGroupAlgebra (ℓ := ℓ) (G := G) x) = x

The prime-power completed augmentation composed with the coefficient-to-group-algebra map is the identity.

Show Lean proof

Definition FoxDifferential.primePowerCompletedGroupAlgebraAugmentationAddHom

def primePowerCompletedGroupAlgebraAugmentationAddHom :
    PrimePowerCompletedGroupAlgebra ℓ G →+ PrimePowerCompletedCoeff ℓ G where
  toFun := primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G)
  map_zero' := by
    apply (primePowerCompletedCoeffSystem ℓ G).ext
    intro i
    change modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
        (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i 0) = 0
    rw [primePowerCompletedGroupAlgebraProjection_zero]
    exact map_zero
      (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2)
  map_add' x y := by
    apply (primePowerCompletedCoeffSystem ℓ G).ext
    intro i
    change modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
        (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (x + y)) =
      modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
          (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x) +
        modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
          (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i y)
    rw [primePowerCompletedGroupAlgebraProjection_add]
    exact map_add
      (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2)
      _ _

The canonical prime-power augmentation as an additive homomorphism.

Definition FoxDifferential.primePowerCompletedGroupAlgebraAugmentationRingHom

def primePowerCompletedGroupAlgebraAugmentationRingHom :
    PrimePowerCompletedGroupAlgebra ℓ G →+* PrimePowerCompletedCoeff ℓ G where
  toFun := primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G)
  map_one' := by
    apply (primePowerCompletedCoeffSystem ℓ G).ext
    intro i
    change modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
        (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i 1) =
      primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i 1
    rw [primePowerCompletedGroupAlgebraProjection_one,
      primePowerCompletedCoeffProjection_one]
    exact map_one (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2)
  map_mul' := by
    intro x y
    apply (primePowerCompletedCoeffSystem ℓ G).ext
    intro i
    change modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
        (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (x * y)) =
      primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
        (primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G) x *
          primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G) y)
    rw [primePowerCompletedGroupAlgebraProjection_mul,
      primePowerCompletedCoeffProjection_mul]
    exact map_mul (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2)
      _ _
  map_zero' := by
    exact map_zero (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G))
  map_add' := by
    intro x y
    exact map_add (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G)) x y

The prime-power completed augmentation bundled as a ring homomorphism.

Abbreviation FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal

abbrev primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal :
    Ideal (PrimePowerCompletedGroupAlgebra ℓ G) :=
  RingHom.ker (primePowerCompletedGroupAlgebraAugmentationRingHom (ℓ := ℓ) (G := G))

The completed augmentation ideal is an ideal of the corresponding completed group algebra.

Theorem FoxDifferential.mem_primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal_iff

omit [Fact (0 < ℓ)] in
@[simp]
theorem mem_primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal_iff
    {x : PrimePowerCompletedGroupAlgebra ℓ G} :
    x ∈ primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal (ℓ := ℓ) (G := G) ↔
      primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G) x =
        (0 : PrimePowerCompletedCoeff ℓ G)

A prime-power completed group-algebra element lies in the augmentation ideal iff its prime-power augmentation is zero.

Show Lean proof

Theorem FoxDifferential.mem_primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal_iff_forall

omit [Fact (0 < ℓ)] in
theorem mem_primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal_iff_forall
    {x : PrimePowerCompletedGroupAlgebra ℓ G} :
    x ∈ primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal (ℓ := ℓ) (G := G) ↔
      ∀ i : PrimePowerCompletedGroupAlgebraIndex G,
        modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
          (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x) = 0

Membership in the prime-power completed augmentation ideal is equivalent to vanishing of every finite-stage augmentation projection.

Show Lean proof

Definition FoxDifferential.primePowerCompletedGroupAlgebraAugmentationAddSubgroup

def primePowerCompletedGroupAlgebraAugmentationAddSubgroup :
    AddSubgroup (PrimePowerCompletedGroupAlgebra ℓ G) :=
  { carrier := {x |
      primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G) x = 0}
    zero_mem' := by
      exact map_zero (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G))
    add_mem' := by
      intro x y hx hy
      change primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G) (x + y) = 0
      rw [map_add, hx, hy]
      simp only [add_zero]
    neg_mem' := by
      intro x hx
      change primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G) (-x) = 0
      rw [map_neg, hx]
      simp only [neg_zero]}

The additive kernel of the prime-power augmentation.

Theorem FoxDifferential.primePowerCompletedGroupAlgebraAugmentation_surjective

omit [Fact (0 < ℓ)] in
theorem primePowerCompletedGroupAlgebraAugmentation_surjective :
    Function.Surjective (primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G))

The prime-power completed augmentation is surjective.

Show Lean proof

Theorem FoxDifferential.primePowerCompletedGroupAlgebraAugmentationAddHom_surjective

omit [Fact (0 < ℓ)] in
theorem primePowerCompletedGroupAlgebraAugmentationAddHom_surjective :
    Function.Surjective (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G))

The additive form of the prime-power completed augmentation is surjective.

Show Lean proof

Theorem FoxDifferential.exact_primePowerCompletedGroupAlgebraAugmentationAddSubgroup_subtype

omit [Fact (0 < ℓ)] in
theorem exact_primePowerCompletedGroupAlgebraAugmentationAddSubgroup_subtype :
    Function.Exact
      (primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G)).subtype
      (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G))

The subtype map from the additive augmentation subgroup has image equal to the kernel of the prime-power augmentation add-hom.

Show Lean proof

Theorem FoxDifferential.primePowerCompletedGroupAlgebraAugmentationAddSubgroup_subtype_injective

omit [Fact (0 < ℓ)] in
theorem primePowerCompletedGroupAlgebraAugmentationAddSubgroup_subtype_injective :
    Function.Injective
      (primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G)).subtype

The subtype inclusion for the additive subgroup underlying the prime-power augmentation kernel is injective.

Show Lean proof

Theorem FoxDifferential.primePowerCompletedGroupAlgebraAugmentationAdd_shortExact

omit [Fact (0 < ℓ)] in
theorem primePowerCompletedGroupAlgebraAugmentationAdd_shortExact :
    Function.Injective
        (primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G)).subtype ∧
      Function.Exact
        (primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G)).subtype
        (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G)) ∧
      Function.Surjective
        (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G))

The canonical augmentation sequence with augmentation ideal as kernel is short exact: the inclusion is injective, its image is the kernel of augmentation, and the augmentation is surjective.

Show Lean proof

Definition FoxDifferential.primePowerCompletedGroupAlgebraAugmentationLinear

def primePowerCompletedGroupAlgebraAugmentationLinear :
    PrimePowerCompletedGroupAlgebra ℓ G →ₗ[ℤ] PrimePowerCompletedCoeff ℓ G :=
  (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G)).toIntLinearMap

The canonical prime-power augmentation is viewed as a \(\mathbb{Z}\)-linear map.

Definition FoxDifferential.primePowerCompletedGroupAlgebraAugmentationCoeffLinear

def primePowerCompletedGroupAlgebraAugmentationCoeffLinear :
    PrimePowerCompletedGroupAlgebra ℓ G →ₗ[PrimePowerCompletedCoeff ℓ G]
      PrimePowerCompletedCoeff ℓ G where
  toFun := primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G)
  map_add' := by
    intro x y
    exact map_add (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G)) x y
  map_smul' := by
    intro a x
    apply (primePowerCompletedCoeffSystem ℓ G).ext
    intro i
    change modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
        (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (a • x)) =
      primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a *
        modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
        (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x)
    rw [primePowerCompletedGroupAlgebraProjection_smul, Algebra.smul_def, map_mul,
      primePowerCompletedGroupAlgebraStageAugmentation_algebraMap]

The canonical prime-power augmentation is viewed as a linear map over the prime-power completed coefficient ring.

Theorem FoxDifferential.primePowerCompletedGroupAlgebraAugmentationCoeffLinear_of

@[simp]
theorem primePowerCompletedGroupAlgebraAugmentationCoeffLinear_of
    (ell : Nat)
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (h : H) :
    primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ell) (G := H)
        (primePowerCompletedGroupAlgebraOf (ell := ell) h) =
      1

The coefficient-linear prime-power augmentation sends a group-like basis element to \(1\).

Show Lean proof

Theorem FoxDifferential.primePowerCompletedGroupAlgebraAugmentationCoeffLinear_one

@[simp]
theorem primePowerCompletedGroupAlgebraAugmentationCoeffLinear_one
    (ell : Nat)
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ell) (G := H)
        (1 : PrimePowerCompletedGroupAlgebra ell H) =
      1

The coefficient-linear prime-power completed augmentation sends the unit element to \(1\).

Show Lean proof

Theorem FoxDifferential.primePowerCompletedGroupAlgebraAugmentationCoeffLinear_mul

@[simp]
theorem primePowerCompletedGroupAlgebraAugmentationCoeffLinear_mul
    (ell : Nat)
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (x y : PrimePowerCompletedGroupAlgebra ell H) :
    primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ell) (G := H) (x * y) =
      primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ell) (G := H) x *
        primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ell) (G := H) y

The coefficient-linear prime-power augmentation is multiplicative on products.

Show Lean proof

Definition FoxDifferential.primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear

def primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear :
    primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G) →ₗ[ℤ]
      PrimePowerCompletedGroupAlgebra ℓ G :=
  (primePowerCompletedGroupAlgebraAugmentationAddSubgroup
    (ℓ := ℓ) (G := G)).subtype.toIntLinearMap

The kernel inclusion of the prime-power augmentation is viewed as a \(\mathbb{Z}\)-linear map.

Theorem FoxDifferential.primePowerCompletedGroupAlgebraAugmentationLinear_surjective

omit [Fact (0 < ℓ)] in
theorem primePowerCompletedGroupAlgebraAugmentationLinear_surjective :
    Function.Surjective
      (primePowerCompletedGroupAlgebraAugmentationLinear (ℓ := ℓ) (G := G))

The linear form of the prime-power completed augmentation is surjective.

Show Lean proof

Theorem FoxDifferential.primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear_injective

omit [Fact (0 < ℓ)] in
theorem primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear_injective :
    Function.Injective
      (primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear
        (ℓ := ℓ) (G := G))

The linear subtype inclusion for the additive subgroup underlying the prime-power augmentation kernel is injective.

Show Lean proof

Theorem FoxDifferential.exact_primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear

omit [Fact (0 < ℓ)] in
theorem exact_primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear :
    Function.Exact
      (primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear
        (ℓ := ℓ) (G := G))
      (primePowerCompletedGroupAlgebraAugmentationLinear (ℓ := ℓ) (G := G))

The linear subtype map from the additive augmentation subgroup has image equal to the kernel of the prime-power augmentation linear map.

Show Lean proof

Theorem FoxDifferential.primePowerCompletedGroupAlgebraAugmentationLinear_shortExact

omit [Fact (0 < ℓ)] in
theorem primePowerCompletedGroupAlgebraAugmentationLinear_shortExact :
    Function.Injective
        (primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear
          (ℓ := ℓ) (G := G)) ∧
      Function.Exact
        (primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear
          (ℓ := ℓ) (G := G))
        (primePowerCompletedGroupAlgebraAugmentationLinear (ℓ := ℓ) (G := G)) ∧
      Function.Surjective
        (primePowerCompletedGroupAlgebraAugmentationLinear (ℓ := ℓ) (G := G))

The canonical augmentation sequence with augmentation ideal as kernel is short exact: the inclusion is injective, its image is the kernel of augmentation, and the augmentation is surjective.

Show Lean proof

ProCGroups.FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Augmentation

Declarations