NYLL
Module

Projection.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.Projection
7 declarations indexed from sourceView source ↗

Module documentation

Fox differential: prime-power completed group algebra — system — ring — projection

The principal declarations in this module are:

  • primePowerCompletedGroupAlgebraProjection_natCast

The finite-stage projection preserves natural number casts.

  • primePowerCompletedGroupAlgebraProjection_intCast

The finite-stage projection preserves integer casts.

  • primePowerCompletedGroupAlgebraProjection_zero

The finite-stage projection sends \(0\) to \(0\).

  • primePowerCompletedGroupAlgebraProjection_add

The prime-power finite-stage projection preserves addition.

Imports1
Imported by2

Declarations

theorem

primePowerCompletedGroupAlgebraProjection_natCast

L39 ↗
FoxDifferential.primePowerCompletedGroupAlgebraProjection_natCast
Documentation

The finite-stage projection preserves natural number casts.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraProjection_natCast
    (i : PrimePowerCompletedGroupAlgebraIndex G) (n : ℕ) :
    primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
        (n : PrimePowerCompletedGroupAlgebra ℓ G) = n
theorem

primePowerCompletedGroupAlgebraProjection_intCast

L49 ↗
FoxDifferential.primePowerCompletedGroupAlgebraProjection_intCast
Documentation

The finite-stage projection preserves integer casts.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraProjection_intCast
    (i : PrimePowerCompletedGroupAlgebraIndex G) (n : ℤ) :
    primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
        (n : PrimePowerCompletedGroupAlgebra ℓ G) = n
theorem

primePowerCompletedGroupAlgebraProjection_zero

L59 ↗
FoxDifferential.primePowerCompletedGroupAlgebraProjection_zero
Documentation

The finite-stage projection sends \(0\) to \(0\).

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraProjection_zero
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
        (0 : PrimePowerCompletedGroupAlgebra ℓ G) = 0
theorem

primePowerCompletedGroupAlgebraProjection_add

L69 ↗
FoxDifferential.primePowerCompletedGroupAlgebraProjection_add
Documentation

The prime-power finite-stage projection preserves addition.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraProjection_add
    (i : PrimePowerCompletedGroupAlgebraIndex G)
    (x y : PrimePowerCompletedGroupAlgebra ℓ G) :
    primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (x + y) =
      primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x +
        primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i y
theorem

primePowerCompletedGroupAlgebraProjection_neg

L83 ↗
FoxDifferential.primePowerCompletedGroupAlgebraProjection_neg
Documentation

The prime-power finite-stage projection preserves negation.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraProjection_neg
    (i : PrimePowerCompletedGroupAlgebraIndex G)
    (x : PrimePowerCompletedGroupAlgebra ℓ G) :
    primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (-x) =
      -primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x
theorem

primePowerCompletedGroupAlgebraProjection_sub

L95 ↗
FoxDifferential.primePowerCompletedGroupAlgebraProjection_sub
Documentation

The prime-power finite-stage projection preserves subtraction.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraProjection_sub
    (i : PrimePowerCompletedGroupAlgebraIndex G)
    (x y : PrimePowerCompletedGroupAlgebra ℓ G) :
    primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (x - y) =
      primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x -
        primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i y
theorem

primePowerCompletedGroupAlgebraStageAugmentation_comp_transition

L112 ↗
FoxDifferential.primePowerCompletedGroupAlgebraStageAugmentation_comp_transition
Documentation

Finite-stage prime-power augmentation is compatible with transition maps and coefficient reduction.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraStageAugmentation_comp_transition
    {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) :
    (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2).comp
        (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij) =
      (modNCompletedCoeffMap
          (n := ℓ ^ i.1) (m := ℓ ^ j.1)
          (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
        (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ j.1) G j.2)

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