Module

LimitEquiv.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.LimitEquiv

16 declarations indexed from sourceView source ↗

Module documentation

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

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.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Module

Imported by2

theorem

primePowerCompletedGroupAlgebraAugmentationIdealProjection_zero

L40 ↗

FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealProjection_zero

Documentation

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

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 primePowerCompletedGroupAlgebraAugmentationIdealProjection_zero
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i
        (0 : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) = 0

theorem

primePowerCompletedGroupAlgebraAugmentationIdealProjection_add

L49 ↗

FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealProjection_add

Documentation

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

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 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

theorem

primePowerCompletedGroupAlgebraAugmentationIdealProjection_neg

L60 ↗

FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealProjection_neg

Documentation

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

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 primePowerCompletedGroupAlgebraAugmentationIdealProjection_neg
    (i : PrimePowerCompletedGroupAlgebraIndex G)
    (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
    primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (-x) =
      -primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i x

theorem

primePowerCompletedGroupAlgebraAugmentationIdealProjection_sub

L70 ↗

FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealProjection_sub

Documentation

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

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 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

theorem

primePowerCompletedGroupAlgebraAugmentationIdealProjection_nsmul

L84 ↗

FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealProjection_nsmul

Documentation

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

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 primePowerCompletedGroupAlgebraAugmentationIdealProjection_nsmul
    (i : PrimePowerCompletedGroupAlgebraIndex G)
    (m : ℕ) (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
    primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (m • x) =
      m • primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i x

theorem

primePowerCompletedGroupAlgebraAugmentationIdealProjection_zsmul

L96 ↗

FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealProjection_zsmul

Documentation

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

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 primePowerCompletedGroupAlgebraAugmentationIdealProjection_zsmul
    (i : PrimePowerCompletedGroupAlgebraIndex G)
    (m : ℤ) (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
    primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (m • x) =
      m • primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i x

theorem

primePowerCompletedGroupAlgebraAugmentationIdealProjection_smul

L106 ↗

FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealProjection_smul

Documentation

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

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 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

def

toPrimePowerCompletedGroupAlgebraAugmentationIdeal

L119 ↗

FoxDifferential.toPrimePowerCompletedGroupAlgebraAugmentationIdeal

Documentation

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

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

def toPrimePowerCompletedGroupAlgebraAugmentationIdeal :
    PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G) →
      PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G

theorem

primePowerCompletedGroupAlgebraAugmentationIdealProjection_to

L139 ↗

FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealProjection_to

Documentation

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

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 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

def

ofPrimePowerCompletedGroupAlgebraAugmentationIdeal

L152 ↗

FoxDifferential.ofPrimePowerCompletedGroupAlgebraAugmentationIdeal

Documentation

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

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

def ofPrimePowerCompletedGroupAlgebraAugmentationIdeal :
    PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G →
      PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G)

theorem

primePowerCompletedGroupAlgebraProjection_ofAugmentationIdeal

L171 ↗

FoxDifferential.primePowerCompletedGroupAlgebraProjection_ofAugmentationIdeal

Documentation

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

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 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)

theorem

ofPrimePowerCompletedGroupAlgebraAugmentationIdeal_to

L187 ↗

FoxDifferential.ofPrimePowerCompletedGroupAlgebraAugmentationIdeal_to

Documentation

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

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 ofPrimePowerCompletedGroupAlgebraAugmentationIdeal_to
    (x : PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G)) :
    ofPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G)
        (toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) x) = x

theorem

toPrimePowerCompletedGroupAlgebraAugmentationIdeal_of

L202 ↗

FoxDifferential.toPrimePowerCompletedGroupAlgebraAugmentationIdeal_of

Documentation

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

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 toPrimePowerCompletedGroupAlgebraAugmentationIdeal_of
    (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
    toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G)
        (ofPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) x) = x

def

primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit

L215 ↗

FoxDifferential.primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit

Documentation

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

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 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)

theorem

primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_apply

L229 ↗

FoxDifferential.primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_apply

Documentation

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

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 primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_apply
    (x : PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G)) :
    primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit
        (ℓ := ℓ) (G := G) x =
      toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) x

theorem

primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_symm_apply

L241 ↗

FoxDifferential.primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_symm_apply

Documentation

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

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 primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_symm_apply
    (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
    (primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit
        (ℓ := ℓ) (G := G)).symm x =
      ofPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) x

Module documentation

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

Declarations