Module

Multiplicative.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.Multiplicative

11 declarations indexed from sourceView source ↗

Module documentation

Fox differential: in class — system — ring — multiplicative

The principal declarations in this module are:

coe_one_primePowerCompletedGroupAlgebraInClass

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

coe_mul_primePowerCompletedGroupAlgebraInClass

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

coe_natCast_primePowerCompletedGroupAlgebraInClass

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

coe_intCast_primePowerCompletedGroupAlgebraInClass

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

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.AddCommGroup

Imported by2

instance

instOnePrimePowerCompletedGroupAlgebraInClass

L45 ↗

FoxDifferential.instOnePrimePowerCompletedGroupAlgebraInClass

Documentation

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

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] instAddCommGroupPrimePowerCompletedGroupAlgebraInClass

Lean source · full declaration

instance instOnePrimePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    One (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
  one := ⟨fun i => (1 : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i), by
    intro i j hij
    change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
      (1 : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j) = 1
    exact map_one _⟩

instance

instMulPrimePowerCompletedGroupAlgebraInClass

L58 ↗

FoxDifferential.instMulPrimePowerCompletedGroupAlgebraInClass

Documentation

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

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] instAddCommGroupPrimePowerCompletedGroupAlgebraInClass

Lean source · full declaration

instance instMulPrimePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    Mul (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
  mul x y := ⟨fun i =>
      (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) *
        (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from y.1 i), by
    intro i j hij
    calc
      primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
          ((show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j) *
            (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from y.1 j))
        =
      primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
          (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j) *
        primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
          (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from y.1 j) := by
            rw [map_mul]
      _ =
      (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) *
        (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from y.1 i) := by
            exact congrArg₂ HMul.hMul (x.2 i j hij) (y.2 i j hij)⟩

instance

instNatCastPrimePowerCompletedGroupAlgebraInClass

L84 ↗

FoxDifferential.instNatCastPrimePowerCompletedGroupAlgebraInClass

Documentation

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

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] instAddCommGroupPrimePowerCompletedGroupAlgebraInClass

Lean source · full declaration

instance instNatCastPrimePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    NatCast (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
  natCast n := ⟨fun i => (n : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i), by
    intro i j hij
    change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
      (n : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j) = n
    exact map_natCast _ _⟩

instance

instIntCastPrimePowerCompletedGroupAlgebraInClass

L97 ↗

FoxDifferential.instIntCastPrimePowerCompletedGroupAlgebraInClass

Documentation

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

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] instAddCommGroupPrimePowerCompletedGroupAlgebraInClass

Lean source · full declaration

instance instIntCastPrimePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    IntCast (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
  intCast n := ⟨fun i => (n : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i), by
    intro i j hij
    change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
      (n : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j) = n
    exact map_intCast _ _⟩

instance

instPowPrimePowerCompletedGroupAlgebraInClass

L107 ↗

FoxDifferential.instPowPrimePowerCompletedGroupAlgebraInClass

Documentation

Powers in the class-indexed prime-power completed group algebra are computed coordinatewise.

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] instAddCommGroupPrimePowerCompletedGroupAlgebraInClass

Lean source · full declaration

instance instPowPrimePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    Pow (PrimePowerCompletedGroupAlgebraInClass ℓ G C) ℕ where
  pow x n := ⟨fun i =>
      (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) ^ n, by
    intro i j hij
    change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
        ((show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j) ^ n) =
      (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) ^ n
    rw [map_pow]
    exact congrArg (fun t => t ^ n) (x.2 i j hij)⟩

theorem

coe_one_primePowerCompletedGroupAlgebraInClass

L125 ↗

FoxDifferential.coe_one_primePowerCompletedGroupAlgebraInClass

Documentation

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

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] instAddCommGroupPrimePowerCompletedGroupAlgebraInClass
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem coe_one_primePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    ((1 : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
      (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
        PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) =
      (1 :
        (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
          PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i)

theorem

coe_mul_primePowerCompletedGroupAlgebraInClass

L142 ↗

FoxDifferential.coe_mul_primePowerCompletedGroupAlgebraInClass

Documentation

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

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] instAddCommGroupPrimePowerCompletedGroupAlgebraInClass
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem coe_mul_primePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (x y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
    ((x * y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
      (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
        PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) =
      (x * y :
        (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
          PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i)

theorem

coe_natCast_primePowerCompletedGroupAlgebraInClass

L160 ↗

FoxDifferential.coe_natCast_primePowerCompletedGroupAlgebraInClass

Documentation

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

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] instAddCommGroupPrimePowerCompletedGroupAlgebraInClass
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem coe_natCast_primePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (n : ℕ) :
    ((n : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
      (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
        PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) =
      (n :
        (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
          PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i)

theorem

coe_intCast_primePowerCompletedGroupAlgebraInClass

L177 ↗

FoxDifferential.coe_intCast_primePowerCompletedGroupAlgebraInClass

Documentation

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

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] instAddCommGroupPrimePowerCompletedGroupAlgebraInClass
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem coe_intCast_primePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (n : ℤ) :
    ((n : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
      (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
        PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) =
      (n :
        (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
          PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i)

theorem

coe_pow_primePowerCompletedGroupAlgebraInClass

L191 ↗

FoxDifferential.coe_pow_primePowerCompletedGroupAlgebraInClass

Documentation

Powers in the class-indexed prime-power completed group algebra are computed coordinatewise.

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] instAddCommGroupPrimePowerCompletedGroupAlgebraInClass
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem coe_pow_primePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) (n : ℕ) :
    ((x ^ n : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
      (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
        PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) =
      (x ^ n :
        (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
          PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i)

instance

instRingPrimePowerCompletedGroupAlgebraInClass

L207 ↗

FoxDifferential.instRingPrimePowerCompletedGroupAlgebraInClass

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 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] instAddCommGroupPrimePowerCompletedGroupAlgebraInClass

Lean source · statement

instance instRingPrimePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    Ring (PrimePowerCompletedGroupAlgebraInClass ℓ G C)

Module documentation

Fox differential: in class — system — ring — multiplicative

Declarations