Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Projection
ProCGroups/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/Coeff/Projection

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Projection

9 Theorems

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.
import
Imported by

Declarations

Theorem FoxDifferential.primePowerCompletedCoeffProjection_one 
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
@[simp]
theorem primePowerCompletedCoeffProjection_one
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
        (1 : PrimePowerCompletedCoeff ℓ G) = 1

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

Show Lean proof
Theorem FoxDifferential.primePowerCompletedCoeffProjection_mul 
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
@[simp]
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

The finite-stage projection preserves multiplication.

Show Lean proof
Theorem FoxDifferential.primePowerCompletedCoeffProjection_natCast 
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
@[simp]
theorem primePowerCompletedCoeffProjection_natCast
    (i : PrimePowerCompletedGroupAlgebraIndex G) (n : ℕ) :
    primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
        (n : PrimePowerCompletedCoeff ℓ G) = n

The finite-stage projection preserves natural number casts.

Show Lean proof
Theorem FoxDifferential.primePowerCompletedCoeffProjection_intCast 
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
@[simp]
theorem primePowerCompletedCoeffProjection_intCast
    (i : PrimePowerCompletedGroupAlgebraIndex G) (n : ℤ) :
    primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
        (n : PrimePowerCompletedCoeff ℓ G) = n

The finite-stage projection preserves integer casts.

Show Lean proof
Theorem FoxDifferential.primePowerCompletedCoeffProjection_zero 
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
@[simp]
theorem primePowerCompletedCoeffProjection_zero
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
        (0 : PrimePowerCompletedCoeff ℓ G) = 0

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

Show Lean proof
Theorem FoxDifferential.primePowerCompletedCoeffProjection_add 
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
@[simp]
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

The prime-power coefficient projection preserves addition.

Show Lean proof
Theorem FoxDifferential.primePowerCompletedCoeffProjection_neg 
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
@[simp]
theorem primePowerCompletedCoeffProjection_neg
    (i : PrimePowerCompletedGroupAlgebraIndex G)
    (x : PrimePowerCompletedCoeff ℓ G) :
    primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (-x) =
      -primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i x

The prime-power coefficient projection preserves negation.

Show Lean proof
Theorem FoxDifferential.primePowerCompletedCoeffProjection_sub 
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
@[simp]
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

The prime-power coefficient projection preserves subtraction.

Show Lean proof
Theorem FoxDifferential.primePowerCompletedCoeffProjection_eq_of_same_exponent 
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
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

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.

Show Lean proof