The linearization kP of a ray table

kP has basis the rays, with products given by the table (set:projective-companion). We realize it inside Matrix R R k through the left regular representation, so that it is a Subalgebra with basis b r and b r * b s = b (rs) or 0.

A table morphism P → P' sends rays to rays or zero, compatibly with products, and sends the identities onto the identities, each hit once. It induces an algebra map kP → kP', surjective when every ray is hit; representation-finiteness passes along such maps (isRepresentationFinite_of_surjective).

theorem MultiplicativeBasisDeformations.isRepresentationFinite_of_surjective {k : Type u} [Field k] {A B : Type u} [Ring A] [Algebra k A] [Ring B] [Algebra k B] [FiniteDimensional k A] [FiniteDimensional k B] (φ : A →ₐ[k] B) (hφ : Function.Surjective ⇑φ) (hA : IsRepresentationFinite k A) : IsRepresentationFinite k B

Representation-finiteness passes to quotient algebras.

def MultiplicativeBasisDeformations.RaySys.Mult.rho {V R : Type} [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] (r : R) : Matrix R R k

The left regular action of a ray.

theorem MultiplicativeBasisDeformations.RaySys.Mult.rho_apply {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] [Nontrivial k] (r t s : R) : P.rho k r t s = if P.mul r s = some t then 1 else 0

theorem MultiplicativeBasisDeformations.RaySys.Mult.rho_mul {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] [Nontrivial k] (r r' : R) : P.rho k r * P.rho k r' = (P.mul r r').elim 0 (P.rho k)

theorem MultiplicativeBasisDeformations.RaySys.Mult.sum_rho_e {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] [Nontrivial k] : ∑ x : V, P.rho k (P.e x) = 1

def MultiplicativeBasisDeformations.RaySys.Mult.linSpan {V R : Type} [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] : Submodule k (Matrix R R k)

The span of the rays.

theorem MultiplicativeBasisDeformations.RaySys.Mult.rho_mem {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] [Nontrivial k] (r : R) : P.rho k r ∈ P.linSpan k

theorem MultiplicativeBasisDeformations.RaySys.Mult.one_mem_linSpan {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] [Nontrivial k] : 1 ∈ P.linSpan k

theorem MultiplicativeBasisDeformations.RaySys.Mult.mul_mem_linSpan {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] [Nontrivial k] (a b : Matrix R R k) (ha : a ∈ P.linSpan k) (hb : b ∈ P.linSpan k) : a * b ∈ P.linSpan k

def MultiplicativeBasisDeformations.RaySys.Mult.Lin {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] [Nontrivial k] : Subalgebra k (Matrix R R k)

The linearization kP.

def MultiplicativeBasisDeformations.RaySys.Mult.b {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] [Nontrivial k] (r : R) : ↥(P.Lin k)

The basis vector of a ray.

theorem MultiplicativeBasisDeformations.RaySys.Mult.b_mul {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] [Nontrivial k] (r s : R) : P.b k r * P.b k s = (P.mul r s).elim 0 (P.b k)

theorem MultiplicativeBasisDeformations.RaySys.Mult.b_mul_of_some {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] [Nontrivial k] {r s t : R} (h : P.mul r s = some t) : P.b k r * P.b k s = P.b k t

theorem MultiplicativeBasisDeformations.RaySys.Mult.b_mul_of_none {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] [Nontrivial k] {r s : R} (h : P.mul r s = none) : P.b k r * P.b k s = 0

theorem MultiplicativeBasisDeformations.RaySys.Mult.sum_b_e {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] [Nontrivial k] : ∑ x : V, P.b k (P.e x) = 1

theorem MultiplicativeBasisDeformations.RaySys.Mult.rho_apply_e {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] [Nontrivial k] (r r' : R) : P.rho k r' r (P.e (P.tgt r)) = if r' = r then 1 else 0

The coordinate of a matrix at a ray: its entry at (r, e (tgt r)).

theorem MultiplicativeBasisDeformations.RaySys.Mult.linearIndependent_b {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] [Nontrivial k] : LinearIndependent k (P.b k)

theorem MultiplicativeBasisDeformations.RaySys.Mult.span_b {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] [Nontrivial k] : Submodule.span k (Set.range (P.b k)) = ⊤

noncomputable def MultiplicativeBasisDeformations.RaySys.Mult.basis {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] [Nontrivial k] : Module.Basis R k ↥(P.Lin k)

The ray basis of kP.

theorem MultiplicativeBasisDeformations.RaySys.Mult.basis_apply {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] [Nontrivial k] (r : R) : (P.basis k) r = P.b k r

instance MultiplicativeBasisDeformations.RaySys.Mult.instFiniteSubtypeMatrixMemSubalgebraLin {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] [Nontrivial k] : Module.Finite k ↥(P.Lin k)

theorem MultiplicativeBasisDeformations.RaySys.Mult.mul_e_none {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) {x : V} {r : R} (h : x ≠ P.src r) : P.mul (P.e x) r = none

theorem MultiplicativeBasisDeformations.RaySys.Mult.mul_none_e {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) {x : V} {r : R} (h : x ≠ P.tgt r) : P.mul r (P.e x) = none

theorem MultiplicativeBasisDeformations.RaySys.Mult.b_e_mul {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] [Nontrivial k] (x : V) (r : R) : P.b k (P.e x) * P.b k r = if x = P.src r then P.b k r else 0

theorem MultiplicativeBasisDeformations.RaySys.Mult.b_mul_e {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] [Nontrivial k] (r : R) (x : V) : P.b k r * P.b k (P.e x) = if x = P.tgt r then P.b k r else 0

theorem MultiplicativeBasisDeformations.RaySys.Mult.b_ne_zero {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] [Nontrivial k] (r : R) : P.b k r ≠ 0

theorem MultiplicativeBasisDeformations.RaySys.Mult.basis_repr_b {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [CommRing k] [Nontrivial k] (r r' : R) : ((P.basis k).repr (P.b k r)) r' = if r = r' then 1 else 0

Table morphisms

structure MultiplicativeBasisDeformations.RaySys.NMor {V R V' R' : Type} (P : Mult V R) (P' : Mult V' R') : Type

A (not necessarily unital) morphism of tables: rays go to rays or zero, compatibly with products, and identities go to identities or zero.

• f : R → Option R'
• hmul (r s : R) : ((self.f r).bind fun (a : R') => (self.f s).bind fun (c : R') => P'.mul a c) = (P.mul r s).bind self.f
• hid (x : V) : self.f (P.e x) = none ∨ ∃ (x' : V'), self.f (P.e x) = some (P'.e x')

structure MultiplicativeBasisDeformations.RaySys.Mor {V R V' R' : Type} (P : Mult V R) (P' : Mult V' R') extends MultiplicativeBasisDeformations.RaySys.NMor P P' : Type

A morphism of tables: the identities go onto the identities, each hit once.

• f : R → Option R'
• hmul (r s : R) : ((self.f r).bind fun (a : R') => (self.f s).bind fun (c : R') => P'.mul a c) = (P.mul r s).bind self.f
• hid (x : V) : self.f (P.e x) = none ∨ ∃ (x' : V'), self.f (P.e x) = some (P'.e x')
• hid' (x' : V') : ∃! x : V, self.f (P.e x) = some (P'.e x')

noncomputable def MultiplicativeBasisDeformations.RaySys.NMor.lin {V R V' R' : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] [Fintype V'] [DecidableEq V'] [Fintype R'] [DecidableEq R'] {P : Mult V R} {P' : Mult V' R'} (m : NMor P P') (k : Type u) [CommRing k] [Nontrivial k] : ↥(P.Lin k) →ₗ[k] ↥(P'.Lin k)

The induced linear map.

theorem MultiplicativeBasisDeformations.RaySys.NMor.lin_b {V R V' R' : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] [Fintype V'] [DecidableEq V'] [Fintype R'] [DecidableEq R'] {P : Mult V R} {P' : Mult V' R'} (m : NMor P P') (k : Type u) [CommRing k] [Nontrivial k] (r : R) : (m.lin k) (P.b k r) = (m.f r).elim 0 (P'.b k)

theorem MultiplicativeBasisDeformations.RaySys.NMor.lin_mul {V R V' R' : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] [Fintype V'] [DecidableEq V'] [Fintype R'] [DecidableEq R'] {P : Mult V R} {P' : Mult V' R'} (m : NMor P P') (k : Type u) [CommRing k] [Nontrivial k] (x y : ↥(P.Lin k)) : (m.lin k) (x * y) = (m.lin k) x * (m.lin k) y

theorem MultiplicativeBasisDeformations.RaySys.Mor.lin_one {V R V' R' : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] [Fintype V'] [DecidableEq V'] [Fintype R'] [DecidableEq R'] {P : Mult V R} {P' : Mult V' R'} (m : Mor P P') (k : Type u) [CommRing k] [Nontrivial k] : (m.lin k) 1 = 1

noncomputable def MultiplicativeBasisDeformations.RaySys.Mor.alg {V R V' R' : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] [Fintype V'] [DecidableEq V'] [Fintype R'] [DecidableEq R'] {P : Mult V R} {P' : Mult V' R'} (m : Mor P P') (k : Type u) [CommRing k] [Nontrivial k] : ↥(P.Lin k) →ₐ[k] ↥(P'.Lin k)

The algebra map of a table morphism.

theorem MultiplicativeBasisDeformations.RaySys.Mor.alg_b {V R V' R' : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] [Fintype V'] [DecidableEq V'] [Fintype R'] [DecidableEq R'] {P : Mult V R} {P' : Mult V' R'} (m : Mor P P') (k : Type u) [CommRing k] [Nontrivial k] (r : R) : (m.alg k) (P.b k r) = (m.f r).elim 0 (P'.b k)

theorem MultiplicativeBasisDeformations.RaySys.Mor.alg_surjective {V R V' R' : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] [Fintype V'] [DecidableEq V'] [Fintype R'] [DecidableEq R'] {P : Mult V R} {P' : Mult V' R'} (m : Mor P P') (k : Type u) [CommRing k] [Nontrivial k] (hs : ∀ (r' : R'), ∃ (r : R), m.f r = some r') : Function.Surjective ⇑(m.alg k)

theorem MultiplicativeBasisDeformations.RaySys.Mor.isRepresentationFinite {V R V' R' : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] [Fintype V'] [DecidableEq V'] [Fintype R'] [DecidableEq R'] {P : Mult V R} {P' : Mult V' R'} (m : Mor P P') (k : Type u) [Field k] (hs : ∀ (r' : R'), ∃ (r : R), m.f r = some r') (h : IsRepresentationFinite k ↥(P.Lin k)) : IsRepresentationFinite k ↥(P'.Lin k)

Representation-finiteness passes along surjective table morphisms.