NYLL
Module

Projection.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Projection
9 declarations indexed from sourceView source ↗

Module documentation

Fox differential: coefficient rings — prime-power completed group algebra — coeff — projection

The principal declarations in this module are:

  • primePowerCompletedCoeffProjection_one

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

  • primePowerCompletedCoeffProjection_mul

The finite-stage projection preserves multiplication.

  • primePowerCompletedCoeffProjection_natCast

The finite-stage projection preserves natural number casts.

  • primePowerCompletedCoeffProjection_intCast

The finite-stage projection preserves integer casts.

Imports1
Imported by2

Declarations

theorem

primePowerCompletedCoeffProjection_one

L39 ↗
FoxDifferential.primePowerCompletedCoeffProjection_one
Documentation

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

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 < ℓ)] [IsTopologicalGroup G] in
Lean source · statement
theorem primePowerCompletedCoeffProjection_one
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
        (1 : PrimePowerCompletedCoeff ℓ G) = 1
theorem

primePowerCompletedCoeffProjection_mul

L49 ↗
FoxDifferential.primePowerCompletedCoeffProjection_mul
Documentation

The finite-stage projection preserves multiplication.

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 < ℓ)] [IsTopologicalGroup G] in
Lean source · statement
theorem primePowerCompletedCoeffProjection_mul
    (i : PrimePowerCompletedGroupAlgebraIndex G)
    (x y : PrimePowerCompletedCoeff ℓ G) :
    primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (x * y) =
      primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i x *
        primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i y
theorem

primePowerCompletedCoeffProjection_natCast

L62 ↗
FoxDifferential.primePowerCompletedCoeffProjection_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 < ℓ)] [IsTopologicalGroup G] in
Lean source · statement
theorem primePowerCompletedCoeffProjection_natCast
    (i : PrimePowerCompletedGroupAlgebraIndex G) (n : ℕ) :
    primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
        (n : PrimePowerCompletedCoeff ℓ G) = n
theorem

primePowerCompletedCoeffProjection_intCast

L72 ↗
FoxDifferential.primePowerCompletedCoeffProjection_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 < ℓ)] [IsTopologicalGroup G] in
Lean source · statement
theorem primePowerCompletedCoeffProjection_intCast
    (i : PrimePowerCompletedGroupAlgebraIndex G) (n : ℤ) :
    primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
        (n : PrimePowerCompletedCoeff ℓ G) = n
theorem

primePowerCompletedCoeffProjection_zero

L82 ↗
FoxDifferential.primePowerCompletedCoeffProjection_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 < ℓ)] [IsTopologicalGroup G] in
Lean source · statement
theorem primePowerCompletedCoeffProjection_zero
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
        (0 : PrimePowerCompletedCoeff ℓ G) = 0
theorem

primePowerCompletedCoeffProjection_add

L92 ↗
FoxDifferential.primePowerCompletedCoeffProjection_add
Documentation

The prime-power coefficient 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 < ℓ)] [IsTopologicalGroup G] in
Lean source · statement
theorem primePowerCompletedCoeffProjection_add
    (i : PrimePowerCompletedGroupAlgebraIndex G)
    (x y : PrimePowerCompletedCoeff ℓ G) :
    primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (x + y) =
      primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i x +
        primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i y
theorem

primePowerCompletedCoeffProjection_neg

L105 ↗
FoxDifferential.primePowerCompletedCoeffProjection_neg
Documentation

The prime-power coefficient 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 < ℓ)] [IsTopologicalGroup G] in
Lean source · statement
theorem primePowerCompletedCoeffProjection_neg
    (i : PrimePowerCompletedGroupAlgebraIndex G)
    (x : PrimePowerCompletedCoeff ℓ G) :
    primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (-x) =
      -primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i x
theorem

primePowerCompletedCoeffProjection_sub

L117 ↗
FoxDifferential.primePowerCompletedCoeffProjection_sub
Documentation

The prime-power coefficient 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 < ℓ)] [IsTopologicalGroup G] in
Lean source · statement
theorem primePowerCompletedCoeffProjection_sub
    (i : PrimePowerCompletedGroupAlgebraIndex G)
    (x y : PrimePowerCompletedCoeff ℓ G) :
    primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (x - y) =
      primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i x -
        primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i y
theorem

primePowerCompletedCoeffProjection_eq_of_same_exponent

L133 ↗
FoxDifferential.primePowerCompletedCoeffProjection_eq_of_same_exponent
Documentation

Coefficient projections with the same prime-power exponent do not depend on the finite-quotient component of the group-algebra index. The second index component synchronizes coefficients and group-algebra stages in one inverse system.

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 < ℓ)] [IsTopologicalGroup G] in
Lean source · statement
theorem primePowerCompletedCoeffProjection_eq_of_same_exponent
    (a : ℕ) (U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G)
    (z : PrimePowerCompletedCoeff ℓ G) :
    primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) (a, U) z =
      primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) (a, V) z

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