NYLL
Module

Ring.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Ring
13 declarations indexed from sourceView source ↗

Module documentation

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

The principal declarations in this module are:

  • instCommRingPrimePowerCompletedCoeffStage

Each finite prime-power coefficient stage is a commutative ring.

  • instCommRingPrimePowerCompletedCoeffFamily

The family-level prime-power completed coefficient object is a commutative ring with operations computed coordinatewise.

  • coe_one_primePowerCompletedCoeff

The multiplicative identity in the prime-power completed coefficient ring is computed coordinatewise.

  • coe_mul_primePowerCompletedCoeff

Multiplication in the prime-power completed coefficient ring is computed coordinatewise.

Imports1
Imported by2

Declarations

instance

instOnePrimePowerCompletedCoeff

L46 ↗
FoxDifferential.instOnePrimePowerCompletedCoeff
Documentation

The unit of the prime-power completed coefficient ring is the compatible family of finite-stage units.

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
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeff
Lean source · full declaration
instance instOnePrimePowerCompletedCoeff : One (PrimePowerCompletedCoeff ℓ G) where
  one := ⟨fun i => (1 : ZMod (ℓ ^ i.1)), by
    intro i j hij
    exact map_one
      (modNCompletedCoeffMap
        (n := ℓ ^ i.1) (m := ℓ ^ j.1)
        (primePow_dvd_primePow (ℓ := ℓ) hij.1))⟩
instance

instMulPrimePowerCompletedCoeff

L58 ↗
FoxDifferential.instMulPrimePowerCompletedCoeff
Documentation

Multiplication on the prime-power completed coefficient ring is defined coordinatewise through finite-stage coefficient rings.

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
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeff
Lean source · full declaration
instance instMulPrimePowerCompletedCoeff : Mul (PrimePowerCompletedCoeff ℓ G) where
  mul 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_mul]
    exact congrArg₂ HMul.hMul (x.2 i j hij) (y.2 i j hij)⟩
instance

instNatCastPrimePowerCompletedCoeff

L74 ↗
FoxDifferential.instNatCastPrimePowerCompletedCoeff
Documentation

Natural number casts in the prime-power completed coefficient ring are computed coordinatewise from finite-stage natural number casts.

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
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeff
Lean source · full declaration
instance instNatCastPrimePowerCompletedCoeff : NatCast (PrimePowerCompletedCoeff ℓ G) where
  natCast n := ⟨fun i => (n : ZMod (ℓ ^ i.1)), by
    intro i j hij
    exact map_natCast
      (modNCompletedCoeffMap
        (n := ℓ ^ i.1) (m := ℓ ^ j.1)
        (primePow_dvd_primePow (ℓ := ℓ) hij.1)) n⟩
instance

instIntCastPrimePowerCompletedCoeff

L86 ↗
FoxDifferential.instIntCastPrimePowerCompletedCoeff
Documentation

Integer casts in the prime-power completed coefficient ring are computed coordinatewise from finite-stage integer casts.

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
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeff
Lean source · full declaration
instance instIntCastPrimePowerCompletedCoeff : IntCast (PrimePowerCompletedCoeff ℓ G) where
  intCast n := ⟨fun i => (n : ZMod (ℓ ^ i.1)), by
    intro i j hij
    exact map_intCast
      (modNCompletedCoeffMap
        (n := ℓ ^ i.1) (m := ℓ ^ j.1)
        (primePow_dvd_primePow (ℓ := ℓ) hij.1)) n⟩
def

instCommRingPrimePowerCompletedCoeffStage

L96 ↗
FoxDifferential.instCommRingPrimePowerCompletedCoeffStage
Documentation

Each finite prime-power coefficient stage is a commutative ring.

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
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeff
Lean source · statement
def instCommRingPrimePowerCompletedCoeffStage
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    CommRing ((primePowerCompletedCoeffSystem ℓ G).X i)
def

instCommRingPrimePowerCompletedCoeffFamily

L108 ↗
FoxDifferential.instCommRingPrimePowerCompletedCoeffFamily
Documentation

The family-level prime-power completed coefficient object is a commutative ring with operations computed coordinatewise.

Source context 11 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
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeff
attribute [local instance] instCommRingPrimePowerCompletedCoeffStage
Lean source · statement
def instCommRingPrimePowerCompletedCoeffFamily :
    CommRing
      ((i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedCoeffSystem ℓ G).X i)
instance

instPowPrimePowerCompletedCoeff

L119 ↗
FoxDifferential.instPowPrimePowerCompletedCoeff
Documentation

Powers in the prime-power completed coefficient ring are computed at every finite coefficient stage.

Source context 12 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
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeff
attribute [local instance] instCommRingPrimePowerCompletedCoeffStage
attribute [local instance] instCommRingPrimePowerCompletedCoeffFamily
Lean source · full declaration
instance instPowPrimePowerCompletedCoeff : Pow (PrimePowerCompletedCoeff ℓ G) ℕ where
  pow x n := ⟨fun i => (show ZMod (ℓ ^ i.1) from x.1 i) ^ n, 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) ^ n) =
      (show ZMod (ℓ ^ i.1) from x.1 i) ^ n
    rw [map_pow]
    exact congrArg (fun t => t ^ n) (x.2 i j hij)⟩
theorem

coe_one_primePowerCompletedCoeff

L136 ↗
FoxDifferential.coe_one_primePowerCompletedCoeff
Documentation

The multiplicative identity in the prime-power completed coefficient ring is computed coordinatewise.

Source context 13 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
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeff
attribute [local instance] instCommRingPrimePowerCompletedCoeffStage
attribute [local instance] instCommRingPrimePowerCompletedCoeffFamily
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
Lean source · statement
theorem coe_one_primePowerCompletedCoeff :
    ((1 : PrimePowerCompletedCoeff ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedCoeffSystem ℓ G).X i) =
      (1 :
        (i : PrimePowerCompletedGroupAlgebraIndex G) →
          (primePowerCompletedCoeffSystem ℓ G).X i)
theorem

coe_mul_primePowerCompletedCoeff

L149 ↗
FoxDifferential.coe_mul_primePowerCompletedCoeff
Documentation

Multiplication in the prime-power completed coefficient ring is computed coordinatewise.

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

coe_natCast_primePowerCompletedCoeff

L165 ↗
FoxDifferential.coe_natCast_primePowerCompletedCoeff
Documentation

Natural number casts in the prime-power completed coefficient ring are computed coordinatewise.

Source context 13 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
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeff
attribute [local instance] instCommRingPrimePowerCompletedCoeffStage
attribute [local instance] instCommRingPrimePowerCompletedCoeffFamily
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
Lean source · statement
theorem coe_natCast_primePowerCompletedCoeff
    (n : ℕ) :
    ((n : PrimePowerCompletedCoeff ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedCoeffSystem ℓ G).X i) =
      (n :
        (i : PrimePowerCompletedGroupAlgebraIndex G) →
          (primePowerCompletedCoeffSystem ℓ G).X i)
theorem

coe_intCast_primePowerCompletedCoeff

L179 ↗
FoxDifferential.coe_intCast_primePowerCompletedCoeff
Documentation

Integer casts in the prime-power completed coefficient ring are computed coordinatewise.

Source context 13 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
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeff
attribute [local instance] instCommRingPrimePowerCompletedCoeffStage
attribute [local instance] instCommRingPrimePowerCompletedCoeffFamily
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
Lean source · statement
theorem coe_intCast_primePowerCompletedCoeff
    (n : ℤ) :
    ((n : PrimePowerCompletedCoeff ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedCoeffSystem ℓ G).X i) =
      (n :
        (i : PrimePowerCompletedGroupAlgebraIndex G) →
          (primePowerCompletedCoeffSystem ℓ G).X i)
theorem

coe_pow_primePowerCompletedCoeff

L193 ↗
FoxDifferential.coe_pow_primePowerCompletedCoeff
Documentation

Powers in the prime-power completed coefficient ring are computed coordinatewise.

Source context 13 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
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeff
attribute [local instance] instCommRingPrimePowerCompletedCoeffStage
attribute [local instance] instCommRingPrimePowerCompletedCoeffFamily
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
Lean source · statement
theorem coe_pow_primePowerCompletedCoeff
    (x : PrimePowerCompletedCoeff ℓ G) (n : ℕ) :
    ((x ^ n : PrimePowerCompletedCoeff ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedCoeffSystem ℓ G).X i) =
      (x ^ n :
        (i : PrimePowerCompletedGroupAlgebraIndex G) →
          (primePowerCompletedCoeffSystem ℓ G).X i)
instance

instCommRingPrimePowerCompletedCoeff

L208 ↗
FoxDifferential.instCommRingPrimePowerCompletedCoeff
Documentation

The prime-power completed coefficient object is a commutative ring with operations computed coordinatewise.

Source context 12 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
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeff
attribute [local instance] instCommRingPrimePowerCompletedCoeffStage
attribute [local instance] instCommRingPrimePowerCompletedCoeffFamily
Lean source · statement
instance instCommRingPrimePowerCompletedCoeff :
    CommRing (PrimePowerCompletedCoeff ℓ G)

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