def Frourio.IsPBWBasis {A : Type u_1} [Ring A] {m : ℕ} (basis : Set (CrossedProduct A m)) : Prop

Equations

• Frourio.IsPBWBasis basis = (basis = Set.range fun (v : Fin m → ℤ) => Frourio.monomial v)

theorem Frourio.pbw_basis {A : Type u_1} [Ring A] (m : ℕ) : ∃ (basis : Set (CrossedProduct A m)), IsPBWBasis basis

PBW基底の存在定理（スケルトン）。

PBWの自由加群表示（Option A）

@[reducible, inline]

noncomputable abbrev Frourio.PBWModule (A : Type u_1) [Semiring A] (m : ℕ) : Type u_1

PBWモジュール：指数ベクトルに係数を割り当てる有限和表示

Equations

• Frourio.PBWModule A m = ((Fin m → ℤ) →₀ A)

noncomputable def Frourio.pbwMonomial {A : Type u_1} [Semiring A] (m : ℕ) (v : Fin m → ℤ) (a : A) : PBWModule A m

係数付きPBW単項式（finsupp上）

Equations

• Frourio.pbwMonomial m v a = Finsupp.single v a

noncomputable def Frourio.pbwFamily {A : Type u_1} [Semiring A] (m : ℕ) : (Fin m → ℤ) → PBWModule A m

係数1のPBWファミリー

Equations

• Frourio.pbwFamily m v = Finsupp.single v 1

強形式のPBW基底（軽量版）： LinearIndependent や Basis を直接使わず、finsupp の性質のみで （1）一次独立相当、（2）生成相当 を定義・証明する。

def Frourio.PBWLinearIndependent (A : Type u_1) [Semiring A] (m : ℕ) : Prop

PBWの標準族 pbwFamily が一次独立であることを表す（finsupp版）。

Equations

• Frourio.PBWLinearIndependent A m = ∀ (l : (Fin m → ℤ) →₀ A), (l.sum fun (v : Fin m → ℤ) (a : A) => Finsupp.single v a) = 0 → l = 0

def Frourio.PBWSpans (A : Type u_1) [Semiring A] (m : ℕ) : Prop

PBWの標準族 pbwFamily が生成すること（任意の元が有限和で書けること）。

Equations

• Frourio.PBWSpans A m = ∀ (f : Frourio.PBWModule A m), ∃ (l : (Fin m → ℤ) →₀ A), f = l.sum fun (v : Fin m → ℤ) (a : A) => Finsupp.single v a

structure Frourio.StrongIsPBWBasis (A : Type u_1) [Semiring A] (m : ℕ) : Prop

強形式のPBW基底（軽量版）：一次独立相当と生成相当の両立。

• linIndep : PBWLinearIndependent A m
• spans : PBWSpans A m

theorem Frourio.sum_single_eq_self {A : Type u_1} [Semiring A] {m : ℕ} (l : (Fin m → ℤ) →₀ A) : (l.sum fun (v : Fin m → ℤ) (a : A) => Finsupp.single v a) = l

一次独立相当：係数finsuppの和が0なら係数が0。

theorem Frourio.pbw_linearIndependent_basic {A : Type u_1} [Semiring A] (m : ℕ) : PBWLinearIndependent A m

theorem Frourio.pbw_spans_basic {A : Type u_1} [Semiring A] (m : ℕ) : PBWSpans A m

生成相当：任意の finsupp はそのまま単項式の有限和。

theorem Frourio.pbw_basis_strong {A : Type u_1} [Semiring A] (m : ℕ) : StrongIsPBWBasis A m

強形式PBW基底（軽量版）の存在。

関係付け: CrossedProduct ↔ PBWModule（単項式レベル）

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

CrossedProduct の単項式を PBWModule に埋め込む。

Equations

• Frourio.toPBW x = Finsupp.single x.scales x.base

@[simp]

theorem Frourio.toPBW_def {A : Type u_1} [Ring A] {m : ℕ} (a : A) (v : Fin m → ℤ) : toPBW { base := a, scales := v } = Finsupp.single v a

def Frourio.fromPBW_of_eq_single {A : Type u_1} [Ring A] {m : ℕ} {f : PBWModule A m} {v : Fin m → ℤ} {a : A} (_hv : f = Finsupp.single v a) : CrossedProduct A m

PBWの単項式等式から CrossedProduct を構成する（明示的な証明引数を取る形）。

Equations

• Frourio.fromPBW_of_eq_single _hv = { base := a, scales := v }

@[simp]

theorem Frourio.from_toPBW {A : Type u_1} [Ring A] {m : ℕ} (x : CrossedProduct A m) : fromPBW_of_eq_single ⋯ = x

@[simp]

theorem Frourio.to_fromPBW {A : Type u_1} [Ring A] {m : ℕ} {v : Fin m → ℤ} {a : A} : toPBW (fromPBW_of_eq_single ⋯) = Finsupp.single v a

toPBW Properties

@[simp]

theorem Frourio.toPBW_zero {A : Type u_1} [Ring A] {m : ℕ} : toPBW 0 = 0

theorem Frourio.toPBW_add_zero_scales {A : Type u_1} [Ring A] {m : ℕ} (x y : CrossedProduct A m) (hx : x.scales = 0) (hy : y.scales = 0) : toPBW (x + y) = toPBW x + toPBW y

toPBW preserves addition only when both have zero scales

theorem Frourio.toPBW_neg_scale_zero {A : Type u_1} [Ring A] {m : ℕ} (x : CrossedProduct A m) (h : x.scales = 0) : toPBW (-x) = -toPBW x

toPBW preserves negation only when scales are zero

instance Frourio.instSubCrossedProduct {A : Type u_1} [Ring A] {m : ℕ} : Sub (CrossedProduct A m)

Equations

• Frourio.instSubCrossedProduct = { sub := fun (x y : Frourio.CrossedProduct A m) => x + -y }

theorem Frourio.toPBW_sub_same_zero_scales {A : Type u_1} [Ring A] {m : ℕ} (x y : CrossedProduct A m) (hx : x.scales = 0) (hy : y.scales = 0) : toPBW (x - y) = toPBW x - toPBW y

toPBW preserves subtraction only when scales are the same and equal to zero

Normal Form and Identity Lemmas

@[simp]

theorem Frourio.single_eq_single_iff {A : Type u_1} [Ring A] {m : ℕ} {v w : Fin m → ℤ} {a b : A} : Finsupp.single v a = Finsupp.single w b ↔ v = w ∧ a = b ∨ a = 0 ∧ b = 0

theorem Frourio.toPBW_injective_on_single {A : Type u_1} [Ring A] {m : ℕ} {v : Fin m → ℤ} {a : A} (ha : a ≠ 0) (x : CrossedProduct A m) : toPBW x = Finsupp.single v a → x = { base := a, scales := v }

theorem Frourio.eq_of_toPBW_eq_on_single {A : Type u_1} [Ring A] {m : ℕ} (x y : CrossedProduct A m) (hx : x.base ≠ 0) (hy : y.base ≠ 0) : toPBW x = toPBW y → x = y

noncomputable def Frourio.pbwSum {A : Type u_1} [Semiring A] (m : ℕ) (s : Finset (Fin m → ℤ)) (c : (Fin m → ℤ) → A) : PBWModule A m

Equations

• Frourio.pbwSum m s c = ∑ v ∈ s, Finsupp.single v (c v)

noncomputable def Frourio.PBWModule.mul {A : Type u_1} [Ring A] {m : ℕ} (σ : ZmAction A m) (x y : PBWModule A m) : PBWModule A m

ねじれ畳み込みによるPBWModule上の乗法

Equations

• Frourio.PBWModule.mul σ x y = Finsupp.sum x fun (v₁ : Fin m → ℤ) (a₁ : A) => Finsupp.sum y fun (v₂ : Fin m → ℤ) (a₂ : A) => Finsupp.single (v₁ + v₂) (a₁ * σ.act v₁ a₂)

structure Frourio.FrourioCrossedProduct (A : Type u_1) [Ring A] (m : ℕ) : Type u_1

• elem : PBWModule A m

noncomputable instance Frourio.instMulFrourioCrossedProduct {A : Type u_1} [Ring A] {m : ℕ} (σ : ZmAction A m) : Mul (FrourioCrossedProduct A m)

Equations

• Frourio.instMulFrourioCrossedProduct σ = { mul := fun (x y : Frourio.FrourioCrossedProduct A m) => { elem := Frourio.PBWModule.mul σ x.elem y.elem } }

Product Compatibility Lemmas (After PBWModule.mul Definition)

theorem Frourio.toPBW_mul_single_right {A : Type u_1} [Ring A] {m : ℕ} (σ : ZmAction A m) (x : CrossedProduct A m) (v : Fin m → ℤ) (a : A) : toPBW (CrossedProduct.mul σ x { base := a, scales := v }) = PBWModule.mul σ (toPBW x) (Finsupp.single v a)

theorem Frourio.toPBW_mul_single_left {A : Type u_1} [Ring A] {m : ℕ} (σ : ZmAction A m) (v : Fin m → ℤ) (a : A) (y : CrossedProduct A m) : toPBW (CrossedProduct.mul σ { base := a, scales := v } y) = PBWModule.mul σ (Finsupp.single v a) (toPBW y)

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