The multiplication table of a multiplicative basis

For an algebra Λ with a multiplicative basis b containing a complete set of orthogonal idempotents b (E v), every basis vector lying in one corner, the products of basis vectors define a ray table (multOfBasis): the table of Construction 3.? / Definition 3.9(2) read off from the basis (projective-rays.tex, "b_r b_s = b_{rs} or 0"). Its associativity comes from that of Λ, and its linearization is isomorphic to Λ (linEquiv).

noncomputable def MultiplicativeBasisDeformations.RaySys.OfBasis.mulB {k : Type u} [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] {R : Type} [Fintype R] (b : Module.Basis R k Λ) (r s : R) : Option R

The product of two basis indices.

theorem MultiplicativeBasisDeformations.RaySys.OfBasis.b_mul_b {k : Type u} [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] {R : Type} [Fintype R] [DecidableEq R] (b : Module.Basis R k Λ) (hmul : IsMultiplicativeBasis b) (r s : R) : b r * b s = (mulB b r s).elim 0 ⇑b

theorem MultiplicativeBasisDeformations.RaySys.OfBasis.mulB_eq_some {k : Type u} [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] {R : Type} [Fintype R] [DecidableEq R] (b : Module.Basis R k Λ) {r s t : R} : mulB b r s = some t ↔ b r * b s = b t

theorem MultiplicativeBasisDeformations.RaySys.OfBasis.e_mul_b {k : Type u} [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (b : Module.Basis R k Λ) (E : V → R) (hE : CompleteOrthogonalIdempotents fun (v : V) => b (E v)) (src tgt : R → V) (hcor : ∀ (r : R), b (E (src r)) * b r * b (E (tgt r)) = b r) (r : R) : b (E (src r)) * b r = b r

theorem MultiplicativeBasisDeformations.RaySys.OfBasis.b_mul_e {k : Type u} [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (b : Module.Basis R k Λ) (E : V → R) (hE : CompleteOrthogonalIdempotents fun (v : V) => b (E v)) (src tgt : R → V) (hcor : ∀ (r : R), b (E (src r)) * b r * b (E (tgt r)) = b r) (r : R) : b r * b (E (tgt r)) = b r

theorem MultiplicativeBasisDeformations.RaySys.OfBasis.src_of_mul {k : Type u} [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (b : Module.Basis R k Λ) (E : V → R) (hE : CompleteOrthogonalIdempotents fun (v : V) => b (E v)) (src tgt : R → V) (hcor : ∀ (r : R), b (E (src r)) * b r * b (E (tgt r)) = b r) {r s t : R} (h : b r * b s = b t) : src t = src r

theorem MultiplicativeBasisDeformations.RaySys.OfBasis.tgt_of_mul {k : Type u} [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (b : Module.Basis R k Λ) (E : V → R) (hE : CompleteOrthogonalIdempotents fun (v : V) => b (E v)) (src tgt : R → V) (hcor : ∀ (r : R), b (E (src r)) * b r * b (E (tgt r)) = b r) {r s t : R} (h : b r * b s = b t) : tgt t = tgt s

theorem MultiplicativeBasisDeformations.RaySys.OfBasis.mid_of_mul {k : Type u} [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (b : Module.Basis R k Λ) (E : V → R) (hE : CompleteOrthogonalIdempotents fun (v : V) => b (E v)) (src tgt : R → V) (hcor : ∀ (r : R), b (E (src r)) * b r * b (E (tgt r)) = b r) {r s t : R} (h : b r * b s = b t) : tgt r = src s

theorem MultiplicativeBasisDeformations.RaySys.OfBasis.elim_mul {k : Type u} [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] {R : Type} [Fintype R] [DecidableEq R] (b : Module.Basis R k Λ) (hmul : IsMultiplicativeBasis b) (o : Option R) (u : R) : o.elim 0 ⇑b * b u = (o.bind fun (t : R) => mulB b t u).elim 0 ⇑b

theorem MultiplicativeBasisDeformations.RaySys.OfBasis.mul_elim {k : Type u} [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] {R : Type} [Fintype R] [DecidableEq R] (b : Module.Basis R k Λ) (hmul : IsMultiplicativeBasis b) (r : R) (o : Option R) : b r * o.elim 0 ⇑b = (o.bind fun (t : R) => mulB b r t).elim 0 ⇑b

theorem MultiplicativeBasisDeformations.RaySys.OfBasis.elim_injective {k : Type u} [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] {R : Type} [Fintype R] [DecidableEq R] (b : Module.Basis R k Λ) {o o' : Option R} (h : o.elim 0 ⇑b = o'.elim 0 ⇑b) : o = o'

theorem MultiplicativeBasisDeformations.RaySys.OfBasis.assocB {k : Type u} [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] {R : Type} [Fintype R] [DecidableEq R] (b : Module.Basis R k Λ) (hmul : IsMultiplicativeBasis b) (r s u : R) : ((mulB b r s).bind fun (t : R) => mulB b t u) = (mulB b s u).bind fun (t : R) => mulB b r t

noncomputable def MultiplicativeBasisDeformations.RaySys.OfBasis.multOfBasis {k : Type u} [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (b : Module.Basis R k Λ) (hmul : IsMultiplicativeBasis b) (E : V → R) (hE : CompleteOrthogonalIdempotents fun (v : V) => b (E v)) (src tgt : R → V) (hcor : ∀ (r : R), b (E (src r)) * b r * b (E (tgt r)) = b r) (hEs : ∀ (v : V), src (E v) = v) (hEt : ∀ (v : V), tgt (E v) = v) : Mult V R

The multiplication table of the basis.

noncomputable def MultiplicativeBasisDeformations.RaySys.OfBasis.linLin {k : Type u} [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (b : Module.Basis R k Λ) (hmul : IsMultiplicativeBasis b) (E : V → R) (hE : CompleteOrthogonalIdempotents fun (v : V) => b (E v)) (src tgt : R → V) (hcor : ∀ (r : R), b (E (src r)) * b r * b (E (tgt r)) = b r) (hEs : ∀ (v : V), src (E v) = v) (hEt : ∀ (v : V), tgt (E v) = v) : ↥((multOfBasis b hmul E hE src tgt hcor hEs hEt).Lin k) ≃ₗ[k] Λ

The basis equivalence kP ≃ Λ.

theorem MultiplicativeBasisDeformations.RaySys.OfBasis.linLin_b {k : Type u} [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (b : Module.Basis R k Λ) (hmul : IsMultiplicativeBasis b) (E : V → R) (hE : CompleteOrthogonalIdempotents fun (v : V) => b (E v)) (src tgt : R → V) (hcor : ∀ (r : R), b (E (src r)) * b r * b (E (tgt r)) = b r) (hEs : ∀ (v : V), src (E v) = v) (hEt : ∀ (v : V), tgt (E v) = v) (r : R) : (linLin b hmul E hE src tgt hcor hEs hEt) ((multOfBasis b hmul E hE src tgt hcor hEs hEt).b k r) = b r

theorem MultiplicativeBasisDeformations.RaySys.OfBasis.linLin_mul {k : Type u} [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (b : Module.Basis R k Λ) (hmul : IsMultiplicativeBasis b) (E : V → R) (hE : CompleteOrthogonalIdempotents fun (v : V) => b (E v)) (src tgt : R → V) (hcor : ∀ (r : R), b (E (src r)) * b r * b (E (tgt r)) = b r) (hEs : ∀ (v : V), src (E v) = v) (hEt : ∀ (v : V), tgt (E v) = v) (x y : ↥((multOfBasis b hmul E hE src tgt hcor hEs hEt).Lin k)) : (linLin b hmul E hE src tgt hcor hEs hEt) (x * y) = (linLin b hmul E hE src tgt hcor hEs hEt) x * (linLin b hmul E hE src tgt hcor hEs hEt) y

noncomputable def MultiplicativeBasisDeformations.RaySys.OfBasis.linEquiv {k : Type u} [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (b : Module.Basis R k Λ) (hmul : IsMultiplicativeBasis b) (E : V → R) (hE : CompleteOrthogonalIdempotents fun (v : V) => b (E v)) (src tgt : R → V) (hcor : ∀ (r : R), b (E (src r)) * b r * b (E (tgt r)) = b r) (hEs : ∀ (v : V), src (E v) = v) (hEt : ∀ (v : V), tgt (E v) = v) : ↥((multOfBasis b hmul E hE src tgt hcor hEs hEt).Lin k) ≃ₐ[k] Λ

The linearization of the table is Λ.

theorem MultiplicativeBasisDeformations.RaySys.OfBasis.linEquiv_b {k : Type u} [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (b : Module.Basis R k Λ) (hmul : IsMultiplicativeBasis b) (E : V → R) (hE : CompleteOrthogonalIdempotents fun (v : V) => b (E v)) (src tgt : R → V) (hcor : ∀ (r : R), b (E (src r)) * b r * b (E (tgt r)) = b r) (hEs : ∀ (v : V), src (E v) = v) (hEt : ∀ (v : V), tgt (E v) = v) (r : R) : (linEquiv b hmul E hE src tgt hcor hEs hEt) ((multOfBasis b hmul E hE src tgt hcor hEs hEt).b k r) = b r