Fibre algebras of deformation families (toward Proposition 12.8)

A scalar fibre of a family m + Σ_i t_i μ_i (characteristic-two-construction.tex) is the underlying space of Λ with an associative unital bilinear product. Fib A is that algebra (AssocMul). When the product agrees with that of Λ up to terms raising the length degree, the length filtration of Λ makes Fib A a positive filtered deformation of Λ (Fib.posFiltration, Definition 6.2).

structure MultiplicativeBasisDeformations.AssocMul (k : Type u) [Field k] (Λ : Type v) [Ring Λ] [Algebra k Λ] : Type v

An associative unital k-bilinear product on Λ.

• mm : Λ →ₗ[k] Λ →ₗ[k] Λ
• assoc (a b c : Λ) : (self.mm ((self.mm a) b)) c = (self.mm a) ((self.mm b) c)
• one_left (a : Λ) : (self.mm 1) a = a
• one_right (a : Λ) : (self.mm a) 1 = a

def MultiplicativeBasisDeformations.Fib {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (_A : AssocMul k Λ) : Type v

The fibre algebra: Λ with the product A.mm.

@[instance_reducible]

instance MultiplicativeBasisDeformations.Fib.instAddCommGroup {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (A : AssocMul k Λ) : AddCommGroup (Fib A)

@[instance_reducible]

instance MultiplicativeBasisDeformations.Fib.instModule {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (A : AssocMul k Λ) : Module k (Fib A)

def MultiplicativeBasisDeformations.Fib.toΛ {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (A : AssocMul k Λ) : Fib A ≃ₗ[k] Λ

The identification with Λ as a k-module.

@[instance_reducible]

instance MultiplicativeBasisDeformations.Fib.instRing {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (A : AssocMul k Λ) : Ring (Fib A)

theorem MultiplicativeBasisDeformations.Fib.toΛ_mul {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (A : AssocMul k Λ) (a b : Fib A) : (toΛ A) (a * b) = (A.mm ((toΛ A) a)) ((toΛ A) b)

theorem MultiplicativeBasisDeformations.Fib.toΛ_one {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (A : AssocMul k Λ) : (toΛ A) 1 = 1

@[instance_reducible]

instance MultiplicativeBasisDeformations.Fib.instAlgebra {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (A : AssocMul k Λ) : Algebra k (Fib A)

theorem MultiplicativeBasisDeformations.Fib.ge_mm_sub_hom {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {A : AssocMul k Λ} (G : LenGrading k Λ) (hdef : ∀ (d e : ℕ) (a b : Λ), G.IsHom d a → G.IsHom e b → G.Ge (d + e + 1) ((A.mm a) b - a * b)) {d e : ℕ} {a b : Λ} (ha : G.Ge d a) (hb : G.Ge e b) : G.Ge (d + e + 1) ((A.mm a) b - a * b)

theorem MultiplicativeBasisDeformations.Fib.ge_mm {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {A : AssocMul k Λ} (G : LenGrading k Λ) (hdef : ∀ (d e : ℕ) (a b : Λ), G.IsHom d a → G.IsHom e b → G.Ge (d + e + 1) ((A.mm a) b - a * b)) {d e : ℕ} {a b : Λ} (ha : G.Ge d a) (hb : G.Ge e b) : G.Ge (d + e) ((A.mm a) b)

theorem MultiplicativeBasisDeformations.Fib.proj_mm {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {A : AssocMul k Λ} (G : LenGrading k Λ) (hdef : ∀ (d e : ℕ) (a b : Λ), G.IsHom d a → G.IsHom e b → G.Ge (d + e + 1) ((A.mm a) b - a * b)) {d e : ℕ} {a b : Λ} (ha : G.Ge d a) (hb : G.Ge e b) : (G.proj (d + e)) ((A.mm a) b) = (G.proj d) a * (G.proj e) b

def MultiplicativeBasisDeformations.Fib.posFiltration {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {A : AssocMul k Λ} (G : LenGrading k Λ) (hdef : ∀ (d e : ℕ) (a b : Λ), G.IsHom d a → G.IsHom e b → G.Ge (d + e + 1) ((A.mm a) b - a * b)) : PosFiltration G (Fib A)

A fibre is a positive filtered deformation (Definition 6.2), filtered by length.