NYLL
Module

Projection.lean

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

Module documentation

Fox differential: in class — system — ring — projection

The principal declarations in this module are:

  • primePowerCompletedGroupAlgebraProjectionInClass_one

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

  • primePowerCompletedGroupAlgebraProjectionInClass_mul

The finite-stage projection preserves multiplication.

  • primePowerCompletedGroupAlgebraProjectionInClass_zero

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

  • primePowerCompletedGroupAlgebraProjectionInClass_add

The prime-power finite-stage projection preserves addition.

Imports1
Imported by4

Declarations

theorem

primePowerCompletedGroupAlgebraProjectionInClass_one

L39 ↗
FoxDifferential.primePowerCompletedGroupAlgebraProjectionInClass_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 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraProjectionInClass_one
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
    primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i
        (1 : PrimePowerCompletedGroupAlgebraInClass ℓ G C) = 1
theorem

primePowerCompletedGroupAlgebraProjectionInClass_mul

L48 ↗
FoxDifferential.primePowerCompletedGroupAlgebraProjectionInClass_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 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraProjectionInClass_mul
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
    (x y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
    primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (x * y) =
      primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x *
        primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i y
theorem

primePowerCompletedGroupAlgebraProjectionInClass_zero

L59 ↗
FoxDifferential.primePowerCompletedGroupAlgebraProjectionInClass_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 primePowerCompletedGroupAlgebraProjectionInClass_zero
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
    primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i
      (0 : PrimePowerCompletedGroupAlgebraInClass ℓ G C) = 0
theorem

primePowerCompletedGroupAlgebraProjectionInClass_add

L68 ↗
FoxDifferential.primePowerCompletedGroupAlgebraProjectionInClass_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 primePowerCompletedGroupAlgebraProjectionInClass_add
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
    (x y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
    primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (x + y) =
      primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x +
        primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i y
theorem

primePowerCompletedGroupAlgebraProjectionInClass_neg

L79 ↗
FoxDifferential.primePowerCompletedGroupAlgebraProjectionInClass_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 primePowerCompletedGroupAlgebraProjectionInClass_neg
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
    (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
    primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (-x) =
      -primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x
theorem

primePowerCompletedGroupAlgebraProjectionInClass_sub

L89 ↗
FoxDifferential.primePowerCompletedGroupAlgebraProjectionInClass_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 primePowerCompletedGroupAlgebraProjectionInClass_sub
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
    (x y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
    primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (x - y) =
      primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x -
        primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i y
theorem

primePowerCompletedGroupAlgebraProjectionInClass_nsmul

L100 ↗
FoxDifferential.primePowerCompletedGroupAlgebraProjectionInClass_nsmul
Documentation

The finite-stage projection is compatible with natural-number scalar 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 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraProjectionInClass_nsmul
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
    (m : ℕ) (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
    primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (m • x) =
      m • primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x
theorem

primePowerCompletedGroupAlgebraProjectionInClass_zsmul

L110 ↗
FoxDifferential.primePowerCompletedGroupAlgebraProjectionInClass_zsmul
Documentation

The finite-stage projection is compatible with integer scalar 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 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraProjectionInClass_zsmul
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
    (m : ℤ) (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
    primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (m • x) =
      m • primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x

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