NYLL
Module

AddCommGroup.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.AddCommGroup
16 declarations indexed from sourceView source ↗

Module documentation

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

The principal declarations in this module are:

  • instAddCommGroupPrimePowerCompletedCoeffStage

Each coefficient stage \(\mathbb{Z}/\ell^i\mathbb{Z}\) carries its standard additive group.

  • instAddCommGroupPrimePowerCompletedCoeffFamily

The dependent family of prime-power coefficient stages carries the pointwise additive commutative group structure.

  • coe_zero_primePowerCompletedCoeff

The inclusion of the prime-power completed coefficient ring preserves zero.

  • coe_add_primePowerCompletedCoeff

The inclusion of the prime-power completed coefficient ring preserves addition.

Imports1
Imported by2

Declarations

instance

instZeroPrimePowerCompletedCoeff

L41 ↗
FoxDifferential.instZeroPrimePowerCompletedCoeff
Documentation

The zero element of the prime-power completed coefficient ring is the compatible family of finite-stage zero elements.

Source context 7 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]
Lean source · full declaration
instance instZeroPrimePowerCompletedCoeff : Zero (PrimePowerCompletedCoeff ℓ G) where
  zero := ⟨fun i => (0 : ZMod (ℓ ^ i.1)), by
    intro i j hij
    exact map_zero
      (modNCompletedCoeffMap
        (n := ℓ ^ i.1) (m := ℓ ^ j.1)
        (primePow_dvd_primePow (ℓ := ℓ) hij.1))⟩
instance

instAddPrimePowerCompletedCoeff

L53 ↗
FoxDifferential.instAddPrimePowerCompletedCoeff
Documentation

Addition in the prime-power completed coefficient ring is defined coordinatewise through finite-stage coefficient additions.

Source context 7 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]
Lean source · full declaration
instance instAddPrimePowerCompletedCoeff : Add (PrimePowerCompletedCoeff ℓ G) where
  add x y := ⟨fun i =>
      (show ZMod (ℓ ^ i.1) from x.1 i) + (show ZMod (ℓ ^ i.1) from y.1 i), by
    intro i j hij
    change modNCompletedCoeffMap
        (n := ℓ ^ i.1) (m := ℓ ^ j.1)
        (primePow_dvd_primePow (ℓ := ℓ) hij.1)
        ((show ZMod (ℓ ^ j.1) from x.1 j) + (show ZMod (ℓ ^ j.1) from y.1 j)) =
      (show ZMod (ℓ ^ i.1) from x.1 i) + (show ZMod (ℓ ^ i.1) from y.1 i)
    rw [map_add]
    exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩
instance

instAddZeroClassPrimePowerCompletedCoeff

L69 ↗
FoxDifferential.instAddZeroClassPrimePowerCompletedCoeff
Documentation

Coordinatewise zero and addition on the prime-power completed coefficient ring satisfy the left and right zero laws.

Source context 7 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]
Lean source · full declaration
instance instAddZeroClassPrimePowerCompletedCoeff :
    AddZeroClass (PrimePowerCompletedCoeff ℓ G) where
  zero := 0
  add := (· + ·)
  zero_add x := by
    apply Subtype.ext
    funext i
    change (0 : ZMod (ℓ ^ i.1)) + (show ZMod (ℓ ^ i.1) from x.1 i) =
      (show ZMod (ℓ ^ i.1) from x.1 i)
    exact zero_add (show ZMod (ℓ ^ i.1) from x.1 i)
  add_zero x := by
    apply Subtype.ext
    funext i
    change (show ZMod (ℓ ^ i.1) from x.1 i) + (0 : ZMod (ℓ ^ i.1)) =
      (show ZMod (ℓ ^ i.1) from x.1 i)
    exact add_zero (show ZMod (ℓ ^ i.1) from x.1 i)
instance

instNegPrimePowerCompletedCoeff

L90 ↗
FoxDifferential.instNegPrimePowerCompletedCoeff
Documentation

Negation on the prime-power completed coefficient ring is defined coordinatewise through finite-stage coefficient negations.

Source context 7 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]
Lean source · full declaration
instance instNegPrimePowerCompletedCoeff : Neg (PrimePowerCompletedCoeff ℓ G) where
  neg x := ⟨fun i => -(show ZMod (ℓ ^ i.1) from x.1 i), by
    intro i j hij
    change modNCompletedCoeffMap
        (n := ℓ ^ i.1) (m := ℓ ^ j.1)
        (primePow_dvd_primePow (ℓ := ℓ) hij.1)
        (-(show ZMod (ℓ ^ j.1) from x.1 j)) =
      -(show ZMod (ℓ ^ i.1) from x.1 i)
    rw [map_neg]
    exact congrArg Neg.neg (x.2 i j hij)⟩
instance

instSubPrimePowerCompletedCoeff

L105 ↗
FoxDifferential.instSubPrimePowerCompletedCoeff
Documentation

Subtraction in the prime-power completed coefficient ring is defined coordinatewise through finite-stage coefficient-ring subtractions.

Source context 7 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]
Lean source · full declaration
instance instSubPrimePowerCompletedCoeff : Sub (PrimePowerCompletedCoeff ℓ G) where
  sub x y := ⟨fun i =>
      (show ZMod (ℓ ^ i.1) from x.1 i) - (show ZMod (ℓ ^ i.1) from y.1 i), by
    intro i j hij
    change modNCompletedCoeffMap
        (n := ℓ ^ i.1) (m := ℓ ^ j.1)
        (primePow_dvd_primePow (ℓ := ℓ) hij.1)
        ((show ZMod (ℓ ^ j.1) from x.1 j) - (show ZMod (ℓ ^ j.1) from y.1 j)) =
      (show ZMod (ℓ ^ i.1) from x.1 i) - (show ZMod (ℓ ^ i.1) from y.1 i)
    rw [map_sub]
    exact congrArg₂ HSub.hSub (x.2 i j hij) (y.2 i j hij)⟩
instance

instSMulNatPrimePowerCompletedCoeff

L121 ↗
FoxDifferential.instSMulNatPrimePowerCompletedCoeff
Documentation

The prime-power completed coefficient ring carries natural-number scalar multiplication coordinatewise at every finite coefficient stage.

Source context 7 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]
Lean source · full declaration
instance instSMulNatPrimePowerCompletedCoeff : SMul ℕ (PrimePowerCompletedCoeff ℓ G) where
  smul m x := ⟨fun i => m • (show ZMod (ℓ ^ i.1) from x.1 i), by
    intro i j hij
    change modNCompletedCoeffMap
        (n := ℓ ^ i.1) (m := ℓ ^ j.1)
        (primePow_dvd_primePow (ℓ := ℓ) hij.1)
        (m • (show ZMod (ℓ ^ j.1) from x.1 j)) =
      m • (show ZMod (ℓ ^ i.1) from x.1 i)
    rw [map_nsmul]
    exact congrArg (m • ·) (x.2 i j hij)⟩
instance

instSMulIntPrimePowerCompletedCoeff

L136 ↗
FoxDifferential.instSMulIntPrimePowerCompletedCoeff
Documentation

The prime-power completed coefficient ring carries integer scalar multiplication coordinatewise at every finite coefficient stage.

Source context 7 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]
Lean source · full declaration
instance instSMulIntPrimePowerCompletedCoeff : SMul ℤ (PrimePowerCompletedCoeff ℓ G) where
  smul m x := ⟨fun i => m • (show ZMod (ℓ ^ i.1) from x.1 i), by
    intro i j hij
    change modNCompletedCoeffMap
        (n := ℓ ^ i.1) (m := ℓ ^ j.1)
        (primePow_dvd_primePow (ℓ := ℓ) hij.1)
        (m • (show ZMod (ℓ ^ j.1) from x.1 j)) =
      m • (show ZMod (ℓ ^ i.1) from x.1 i)
    rw [map_zsmul]
    exact congrArg (m • ·) (x.2 i j hij)⟩
def

instAddCommGroupPrimePowerCompletedCoeffStage

L148 ↗
FoxDifferential.instAddCommGroupPrimePowerCompletedCoeffStage
Documentation

Each coefficient stage \(\mathbb{Z}/\ell^i\mathbb{Z}\) carries its standard additive group.

Source context 7 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]
Lean source · statement
def instAddCommGroupPrimePowerCompletedCoeffStage
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    AddCommGroup ((primePowerCompletedCoeffSystem ℓ G).X i)
def

instAddCommGroupPrimePowerCompletedCoeffFamily

L160 ↗
FoxDifferential.instAddCommGroupPrimePowerCompletedCoeffFamily
Documentation

The dependent family of prime-power coefficient stages carries the pointwise additive commutative group structure.

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]
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
Lean source · statement
def instAddCommGroupPrimePowerCompletedCoeffFamily :
    AddCommGroup
      ((i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedCoeffSystem ℓ G).X i)
theorem

coe_zero_primePowerCompletedCoeff

L171 ↗
FoxDifferential.coe_zero_primePowerCompletedCoeff
Documentation

The inclusion of the prime-power completed coefficient ring preserves zero.

Source context 10 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]
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffFamily
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
Lean source · statement
theorem coe_zero_primePowerCompletedCoeff :
    ((0 : PrimePowerCompletedCoeff ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedCoeffSystem ℓ G).X i) = 0
theorem

coe_add_primePowerCompletedCoeff

L181 ↗
FoxDifferential.coe_add_primePowerCompletedCoeff
Documentation

The inclusion of the prime-power completed coefficient ring preserves addition.

Source context 10 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]
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffFamily
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
Lean source · statement
theorem coe_add_primePowerCompletedCoeff
    (x y : PrimePowerCompletedCoeff ℓ G) :
    ((x + y : PrimePowerCompletedCoeff ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedCoeffSystem ℓ G).X i) = x + y
theorem

coe_neg_primePowerCompletedCoeff

L192 ↗
FoxDifferential.coe_neg_primePowerCompletedCoeff
Documentation

The inclusion of the prime-power completed coefficient ring preserves negation.

Source context 10 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]
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffFamily
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
Lean source · statement
theorem coe_neg_primePowerCompletedCoeff
    (x : PrimePowerCompletedCoeff ℓ G) :
    ((-x : PrimePowerCompletedCoeff ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedCoeffSystem ℓ G).X i) = -x
theorem

coe_sub_primePowerCompletedCoeff

L203 ↗
FoxDifferential.coe_sub_primePowerCompletedCoeff
Documentation

The inclusion of the prime-power completed coefficient ring preserves subtraction.

Source context 10 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]
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffFamily
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
Lean source · statement
theorem coe_sub_primePowerCompletedCoeff
    (x y : PrimePowerCompletedCoeff ℓ G) :
    ((x - y : PrimePowerCompletedCoeff ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedCoeffSystem ℓ G).X i) = x - y
theorem

coe_nsmul_primePowerCompletedCoeff

L217 ↗
FoxDifferential.coe_nsmul_primePowerCompletedCoeff
Documentation

The inclusion of the prime-power completed coefficient ring preserves natural-number scalar multiplication.

Source context 10 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]
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffFamily
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
Lean source · statement
theorem coe_nsmul_primePowerCompletedCoeff
    (m : ℕ) (x : PrimePowerCompletedCoeff ℓ G) :
    ((m • x : PrimePowerCompletedCoeff ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedCoeffSystem ℓ G).X i) = m • x
theorem

coe_zsmul_primePowerCompletedCoeff

L231 ↗
FoxDifferential.coe_zsmul_primePowerCompletedCoeff
Documentation

The inclusion of the prime-power completed coefficient ring preserves integer scalar multiplication.

Source context 10 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]
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffFamily
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
Lean source · statement
theorem coe_zsmul_primePowerCompletedCoeff
    (m : ℤ) (x : PrimePowerCompletedCoeff ℓ G) :
    ((m • x : PrimePowerCompletedCoeff ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedCoeffSystem ℓ G).X i) = m • x
def

instAddCommGroupPrimePowerCompletedCoeff

L243 ↗
FoxDifferential.instAddCommGroupPrimePowerCompletedCoeff
Documentation

The prime-power completed coefficient ring inherits an additive commutative group structure from its injective inclusion into the family of coefficient stages.

Source context 9 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]
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffFamily
Lean source · statement
def instAddCommGroupPrimePowerCompletedCoeff :
    AddCommGroup (PrimePowerCompletedCoeff ℓ G)

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