NYLL
Module

Multiplicative.lean

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

Module documentation

Fox differential: prime-power completed group algebra — system — ring — multiplicative

The principal declarations in this module are:

  • instRingPrimePowerCompletedGroupAlgebraStage

Each finite prime-power group-algebra stage carries its standard ring structure.

  • instRingPrimePowerCompletedGroupAlgebraFamily

The dependent family of finite prime-power group-algebra stages carries the pointwise ring structure.

  • coe_one_primePowerCompletedGroupAlgebra

The multiplicative identity in the prime-power completed group algebra is computed coordinatewise.

  • coe_mul_primePowerCompletedGroupAlgebra

Multiplication in the prime-power completed group algebra is computed coordinatewise.

Imports1
Imported by2

Declarations

instance

instOnePrimePowerCompletedGroupAlgebra

L42 ↗
FoxDifferential.instOnePrimePowerCompletedGroupAlgebra
Documentation

The prime-power completed group algebra has a coordinatewise multiplicative identity.

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] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebra
Lean source · full declaration
instance instOnePrimePowerCompletedGroupAlgebra : One (PrimePowerCompletedGroupAlgebra ℓ G) where
  one := ⟨fun i => (1 : PrimePowerCompletedGroupAlgebraStage ℓ G i), by
    intro i j hij
    change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
      (1 : PrimePowerCompletedGroupAlgebraStage ℓ G j) = 1
    exact map_one _⟩
instance

instMulPrimePowerCompletedGroupAlgebra

L53 ↗
FoxDifferential.instMulPrimePowerCompletedGroupAlgebra
Documentation

Multiplication on the completed group algebra is defined coordinatewise through the finite-stage group-algebra products.

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] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebra
Lean source · full declaration
instance instMulPrimePowerCompletedGroupAlgebra : Mul (PrimePowerCompletedGroupAlgebra ℓ G) where
  mul x y := ⟨fun i =>
      (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) *
        (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i), by
    intro i j hij
    calc
      primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
          ((show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) *
            (show PrimePowerCompletedGroupAlgebraStage ℓ G j from y.1 j))
        =
      primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
          (show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) *
        primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
          (show PrimePowerCompletedGroupAlgebraStage ℓ G j from y.1 j) := by
            rw [map_mul]
      _ =
      (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) *
        (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i) := by
            exact congrArg₂ HMul.hMul (x.2 i j hij) (y.2 i j hij)⟩
instance

instNatCastPrimePowerCompletedGroupAlgebra

L74 ↗
FoxDifferential.instNatCastPrimePowerCompletedGroupAlgebra
Documentation

Natural number casts in the prime-power completed group algebra are computed coordinatewise.

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] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebra
Lean source · full declaration
instance instNatCastPrimePowerCompletedGroupAlgebra :
    NatCast (PrimePowerCompletedGroupAlgebra ℓ G) where
  natCast n := ⟨fun i => (n : PrimePowerCompletedGroupAlgebraStage ℓ G i), by
    intro i j hij
    change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
      (n : PrimePowerCompletedGroupAlgebraStage ℓ G j) = n
    exact map_natCast _ _⟩
instance

instIntCastPrimePowerCompletedGroupAlgebra

L83 ↗
FoxDifferential.instIntCastPrimePowerCompletedGroupAlgebra
Documentation

Integer casts in the prime-power completed group algebra are computed coordinatewise.

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] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebra
Lean source · full declaration
instance instIntCastPrimePowerCompletedGroupAlgebra :
    IntCast (PrimePowerCompletedGroupAlgebra ℓ G) where
  intCast n := ⟨fun i => (n : PrimePowerCompletedGroupAlgebraStage ℓ G i), by
    intro i j hij
    change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
      (n : PrimePowerCompletedGroupAlgebraStage ℓ G j) = n
    exact map_intCast _ _⟩
def

instRingPrimePowerCompletedGroupAlgebraStage

L93 ↗
FoxDifferential.instRingPrimePowerCompletedGroupAlgebraStage
Documentation

Each finite prime-power group-algebra stage carries its standard ring structure.

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] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebra
Lean source · statement
def instRingPrimePowerCompletedGroupAlgebraStage
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    Ring ((primePowerCompletedGroupAlgebraSystem ℓ G).X i)
def

instRingPrimePowerCompletedGroupAlgebraFamily

L105 ↗
FoxDifferential.instRingPrimePowerCompletedGroupAlgebraFamily
Documentation

The dependent family of finite prime-power group-algebra stages carries the pointwise ring structure.

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] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebra
attribute [local instance] instRingPrimePowerCompletedGroupAlgebraStage
Lean source · statement
def instRingPrimePowerCompletedGroupAlgebraFamily :
    Ring
      ((i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraSystem ℓ G).X i)
instance

instPowPrimePowerCompletedGroupAlgebra

L113 ↗
FoxDifferential.instPowPrimePowerCompletedGroupAlgebra
Documentation

Powers in the prime-power completed group algebra are 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] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebra
attribute [local instance] instRingPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instRingPrimePowerCompletedGroupAlgebraFamily
Lean source · full declaration
instance instPowPrimePowerCompletedGroupAlgebra : Pow (PrimePowerCompletedGroupAlgebra ℓ G) ℕ where
  pow x n := ⟨fun i => (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) ^ n, by
    intro i j hij
    change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
        ((show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) ^ n) =
      (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) ^ n
    rw [map_pow]
    exact congrArg (fun t => t ^ n) (x.2 i j hij)⟩
theorem

coe_one_primePowerCompletedGroupAlgebra

L128 ↗
FoxDifferential.coe_one_primePowerCompletedGroupAlgebra
Documentation

The multiplicative identity in the prime-power completed group algebra 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] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebra
attribute [local instance] instRingPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instRingPrimePowerCompletedGroupAlgebraFamily
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem coe_one_primePowerCompletedGroupAlgebra :
    ((1 : PrimePowerCompletedGroupAlgebra ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraSystem ℓ G).X i) =
      (1 :
        (i : PrimePowerCompletedGroupAlgebraIndex G) →
          (primePowerCompletedGroupAlgebraSystem ℓ G).X i)
theorem

coe_mul_primePowerCompletedGroupAlgebra

L141 ↗
FoxDifferential.coe_mul_primePowerCompletedGroupAlgebra
Documentation

Multiplication in the prime-power completed group algebra 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] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebra
attribute [local instance] instRingPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instRingPrimePowerCompletedGroupAlgebraFamily
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem coe_mul_primePowerCompletedGroupAlgebra
    (x y : PrimePowerCompletedGroupAlgebra ℓ G) :
    ((x * y : PrimePowerCompletedGroupAlgebra ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraSystem ℓ G).X i) =
      (x * y :
        (i : PrimePowerCompletedGroupAlgebraIndex G) →
          (primePowerCompletedGroupAlgebraSystem ℓ G).X i)
theorem

coe_natCast_primePowerCompletedGroupAlgebra

L155 ↗
FoxDifferential.coe_natCast_primePowerCompletedGroupAlgebra
Documentation

Natural number casts in the prime-power completed group algebra 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] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebra
attribute [local instance] instRingPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instRingPrimePowerCompletedGroupAlgebraFamily
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem coe_natCast_primePowerCompletedGroupAlgebra
    (n : ℕ) :
    ((n : PrimePowerCompletedGroupAlgebra ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraSystem ℓ G).X i) =
      (n :
        (i : PrimePowerCompletedGroupAlgebraIndex G) →
          (primePowerCompletedGroupAlgebraSystem ℓ G).X i)
theorem

coe_intCast_primePowerCompletedGroupAlgebra

L169 ↗
FoxDifferential.coe_intCast_primePowerCompletedGroupAlgebra
Documentation

Integer casts in the prime-power completed group algebra 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] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebra
attribute [local instance] instRingPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instRingPrimePowerCompletedGroupAlgebraFamily
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem coe_intCast_primePowerCompletedGroupAlgebra
    (n : ℤ) :
    ((n : PrimePowerCompletedGroupAlgebra ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraSystem ℓ G).X i) =
      (n :
        (i : PrimePowerCompletedGroupAlgebraIndex G) →
          (primePowerCompletedGroupAlgebraSystem ℓ G).X i)
theorem

coe_pow_primePowerCompletedGroupAlgebra

L183 ↗
FoxDifferential.coe_pow_primePowerCompletedGroupAlgebra
Documentation

Powers in the prime-power completed group algebra 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] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebra
attribute [local instance] instRingPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instRingPrimePowerCompletedGroupAlgebraFamily
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem coe_pow_primePowerCompletedGroupAlgebra
    (x : PrimePowerCompletedGroupAlgebra ℓ G) (n : ℕ) :
    ((x ^ n : PrimePowerCompletedGroupAlgebra ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraSystem ℓ G).X i) =
      (x ^ n :
        (i : PrimePowerCompletedGroupAlgebraIndex G) →
          (primePowerCompletedGroupAlgebraSystem ℓ G).X i)
instance

instRingPrimePowerCompletedGroupAlgebra

L198 ↗
FoxDifferential.instRingPrimePowerCompletedGroupAlgebra
Documentation

The completed group algebra is a ring because all ring operations and ring axioms are inherited coordinatewise from the finite-stage group algebras.

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] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebra
attribute [local instance] instRingPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instRingPrimePowerCompletedGroupAlgebraFamily
Lean source · statement
instance instRingPrimePowerCompletedGroupAlgebra :
    Ring (PrimePowerCompletedGroupAlgebra ℓ G)

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