NYLL
Module

Augmentation.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Augmentation
22 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — coefficient rings — prime-power augmentation ideal — augmentation

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.

Imports1
Imported by2

Declarations

theorem

primePowerCompletedGroupAlgebraAugmentation_comp_coeffToGroupAlgebra

L44 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentation_comp_coeffToGroupAlgebra
Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraAugmentation_comp_coeffToGroupAlgebra
    (x : PrimePowerCompletedCoeff ℓ G) :
    primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G)
        (primePowerCompletedCoeffToGroupAlgebra (ℓ := ℓ) (G := G) x) = x
def

primePowerCompletedGroupAlgebraAugmentationAddHom

L58 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentationAddHom
Documentation

The canonical prime-power augmentation as an additive homomorphism.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
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)
      _ _
def

primePowerCompletedGroupAlgebraAugmentationRingHom

L84 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentationRingHom
Documentation

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

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
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
abbrev

primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal

L116 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal
Documentation

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

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
abbrev primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal :
    Ideal (PrimePowerCompletedGroupAlgebra ℓ G)
theorem

mem_primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal_iff

L127 ↗
FoxDifferential.mem_primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal_iff
Documentation

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

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem mem_primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal_iff
    {x : PrimePowerCompletedGroupAlgebra ℓ G} :
    x ∈ primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal (ℓ := ℓ) (G := G) ↔
      primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G) x =
        (0 : PrimePowerCompletedCoeff ℓ G)
theorem

mem_primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal_iff_forall

L141 ↗
FoxDifferential.mem_primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal_iff_forall
Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
omit [Fact (0 < ℓ)] in
Lean source · statement
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
def

primePowerCompletedGroupAlgebraAugmentationAddSubgroup

L152 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentationAddSubgroup
Documentation

The additive kernel of the prime-power augmentation.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
Lean source · statement
def primePowerCompletedGroupAlgebraAugmentationAddSubgroup :
    AddSubgroup (PrimePowerCompletedGroupAlgebra ℓ G)
theorem

primePowerCompletedGroupAlgebraAugmentation_surjective

L171 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentation_surjective
Documentation

The prime-power completed augmentation is surjective.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraAugmentation_surjective :
    Function.Surjective (primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G))
theorem

primePowerCompletedGroupAlgebraAugmentationAddHom_surjective

L180 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentationAddHom_surjective
Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraAugmentationAddHom_surjective :
    Function.Surjective (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G))
theorem

exact_primePowerCompletedGroupAlgebraAugmentationAddSubgroup_subtype

L190 ↗
FoxDifferential.exact_primePowerCompletedGroupAlgebraAugmentationAddSubgroup_subtype
Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem exact_primePowerCompletedGroupAlgebraAugmentationAddSubgroup_subtype :
    Function.Exact
      (primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G)).subtype
      (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G))
theorem

primePowerCompletedGroupAlgebraAugmentationAddSubgroup_subtype_injective

L206 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentationAddSubgroup_subtype_injective
Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraAugmentationAddSubgroup_subtype_injective :
    Function.Injective
      (primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G)).subtype
theorem

primePowerCompletedGroupAlgebraAugmentationAdd_shortExact

L218 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentationAdd_shortExact
Documentation

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.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraAugmentationAdd_shortExact :
    Function.Injective
        (primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G)).subtype ∧
      Function.Exact
        (primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G)).subtype
        (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G)) ∧
      Function.Surjective
        (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G))
def

primePowerCompletedGroupAlgebraAugmentationLinear

L233 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentationLinear
Documentation

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

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
Lean source · statement
def primePowerCompletedGroupAlgebraAugmentationLinear :
    PrimePowerCompletedGroupAlgebra ℓ G →ₗ[ℤ] PrimePowerCompletedCoeff ℓ G
def

primePowerCompletedGroupAlgebraAugmentationCoeffLinear

L241 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentationCoeffLinear
Documentation

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

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
Lean source · full declaration
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]
theorem

primePowerCompletedGroupAlgebraAugmentationCoeffLinear_of

L262 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentationCoeffLinear_of
Documentation

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

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
Lean source · statement
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
theorem

primePowerCompletedGroupAlgebraAugmentationCoeffLinear_one

L282 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentationCoeffLinear_one
Documentation

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

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
Lean source · statement
theorem primePowerCompletedGroupAlgebraAugmentationCoeffLinear_one
    (ell : Nat)
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ell) (G := H)
        (1 : PrimePowerCompletedGroupAlgebra ell H) =
      1
theorem

primePowerCompletedGroupAlgebraAugmentationCoeffLinear_mul

L294 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentationCoeffLinear_mul
Documentation

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

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
Lean source · statement
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
def

primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear

L309 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear
Documentation

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

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
Lean source · statement
def primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear :
    primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G) →ₗ[ℤ]
      PrimePowerCompletedGroupAlgebra ℓ G
theorem

primePowerCompletedGroupAlgebraAugmentationLinear_surjective

L317 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentationLinear_surjective
Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraAugmentationLinear_surjective :
    Function.Surjective
      (primePowerCompletedGroupAlgebraAugmentationLinear (ℓ := ℓ) (G := G))
theorem

primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear_injective

L328 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear_injective
Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear_injective :
    Function.Injective
      (primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear
        (ℓ := ℓ) (G := G))
theorem

exact_primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear

L340 ↗
FoxDifferential.exact_primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear
Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem exact_primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear :
    Function.Exact
      (primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear
        (ℓ := ℓ) (G := G))
      (primePowerCompletedGroupAlgebraAugmentationLinear (ℓ := ℓ) (G := G))
theorem

primePowerCompletedGroupAlgebraAugmentationLinear_shortExact

L356 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentationLinear_shortExact
Documentation

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.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraAugmentationLinear_shortExact :
    Function.Injective
        (primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear
          (ℓ := ℓ) (G := G)) ∧
      Function.Exact
        (primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear
          (ℓ := ℓ) (G := G))
        (primePowerCompletedGroupAlgebraAugmentationLinear (ℓ := ℓ) (G := G)) ∧
      Function.Surjective
        (primePowerCompletedGroupAlgebraAugmentationLinear (ℓ := ℓ) (G := G))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.