theorem Frourio.pbw_mul_single_single {A : Type u_1} [Ring A] {m : ℕ} (σ : ZmAction A m) (v₁ v₂ : Fin m → ℤ) (a₁ a₂ : A) : PBWModule.mul σ (Finsupp.single v₁ a₁) (Finsupp.single v₂ a₂) = Finsupp.single (v₁ + v₂) (a₁ * σ.act v₁ a₂)

単項式同士の積

theorem Frourio.pbw_mul_zero_left {A : Type u_1} [Ring A] {m : ℕ} (σ : ZmAction A m) (x : PBWModule A m) : PBWModule.mul σ 0 x = 0

ゼロ元との積（左）

theorem Frourio.pbw_mul_zero_right {A : Type u_1} [Ring A] {m : ℕ} (σ : ZmAction A m) (x : PBWModule A m) : PBWModule.mul σ x 0 = 0

ゼロ元との積（右）

theorem Frourio.sum_zero_coeff {A : Type u_1} [Ring A] {m : ℕ} (σ : ZmAction A m) (v : Fin m → ℤ) (y : PBWModule A m) : (Finsupp.sum y fun (v₂ : Fin m → ℤ) (a₂ : A) => Finsupp.single (v + v₂) (0 * σ.act v a₂)) = 0

補助：ゼロ係数の和はゼロ

theorem Frourio.pbw_left_distrib_single_manual {A : Type u_1} [Ring A] {m : ℕ} (σ : ZmAction A m) (v : Fin m → ℤ) (a : A) (y z : PBWModule A m) : PBWModule.mul σ (Finsupp.single v a) (y + z) = PBWModule.mul σ (Finsupp.single v a) y + PBWModule.mul σ (Finsupp.single v a) z

手動展開による左分配（単項式の場合）

theorem Frourio.pbw_left_distrib {A : Type u_1} [Ring A] {m : ℕ} (σ : ZmAction A m) (x y z : PBWModule A m) : PBWModule.mul σ x (y + z) = PBWModule.mul σ x y + PBWModule.mul σ x z

一般の左分配律

theorem Frourio.pbw_right_distrib {A : Type u_1} [Ring A] {m : ℕ} (σ : ZmAction A m) (x y z : PBWModule A m) : PBWModule.mul σ (x + y) z = PBWModule.mul σ x z + PBWModule.mul σ y z

右分配律

PBWModule Associativity and Unit

theorem Frourio.pbw_mul_assoc_single3 {A : Type u_1} [Ring A] {m : ℕ} (σ : ZmAction A m) (v₁ v₂ v₃ : Fin m → ℤ) (a₁ a₂ a₃ : A) : PBWModule.mul σ (PBWModule.mul σ (Finsupp.single v₁ a₁) (Finsupp.single v₂ a₂)) (Finsupp.single v₃ a₃) = PBWModule.mul σ (Finsupp.single v₁ a₁) (PBWModule.mul σ (Finsupp.single v₂ a₂) (Finsupp.single v₃ a₃))

単項式3つに対する結合律

theorem Frourio.pbw_assoc_single_left {A : Type u_1} [Ring A] {m : ℕ} (σ : ZmAction A m) (v : Fin m → ℤ) (a : A) (y z : PBWModule A m) : PBWModule.mul σ (PBWModule.mul σ (Finsupp.single v a) y) z = PBWModule.mul σ (Finsupp.single v a) (PBWModule.mul σ y z)

単項式を左に固定したときの結合律（一般元に拡張）

theorem Frourio.pbw_mul_assoc {A : Type u_1} [Ring A] {m : ℕ} (σ : ZmAction A m) (x y z : PBWModule A m) : PBWModule.mul σ (PBWModule.mul σ x y) z = PBWModule.mul σ x (PBWModule.mul σ y z)

Associativity of PBWModule.mul

noncomputable def Frourio.pbwOne {A : Type u_1} [Ring A] (m : ℕ) : PBWModule A m

The unit element for PBWModule.mul

Equations

• Frourio.pbwOne m = Finsupp.single 0 1

theorem Frourio.pbw_one_mul {A : Type u_1} [Ring A] {m : ℕ} (σ : ZmAction A m) (x : PBWModule A m) : PBWModule.mul σ (pbwOne m) x = x

Left unit property

theorem Frourio.pbw_mul_one {A : Type u_1} [Ring A] {m : ℕ} (σ : ZmAction A m) (x : PBWModule A m) : PBWModule.mul σ x (pbwOne m) = x

Right unit property