Retractions of ray tables (Lemma 8.9 at ray level)

lem:representation-transfer: a table S embedded in a table T by a unital morphism that is injective on rays, such that a ray of T whose product with an embedded ray is embedded is itself embedded (on either side). The projection of kT onto the embedded rays is then an S-bimodule retraction, and Lemma 4.6 shows that kS is representation-finite when kT is.

noncomputable def MultiplicativeBasisDeformations.RaySys.Mor.retr {V R V' R' : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] [Fintype V'] [DecidableEq V'] [Fintype R'] [DecidableEq R'] (S : Mult V R) (T : Mult V' R') (g : R → R') (k : Type u) [Field k] : ↥(T.Lin k) →ₗ[k] ↥(S.Lin k)

The projection onto the embedded rays.

theorem MultiplicativeBasisDeformations.RaySys.Mor.retr_b {V R V' R' : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] [Fintype V'] [DecidableEq V'] [Fintype R'] [DecidableEq R'] (S : Mult V R) (T : Mult V' R') (g : R → R') (k : Type u) [Field k] (t : R') : (retr S T g k) (T.b k t) = if h : ∃ (s : R), g s = t then S.b k h.choose else 0

theorem MultiplicativeBasisDeformations.RaySys.Mor.retr_b_g {V R V' R' : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] [Fintype V'] [DecidableEq V'] [Fintype R'] [DecidableEq R'] (S : Mult V R) (T : Mult V' R') (g : R → R') (hginj : Function.Injective g) (k : Type u) [Field k] (s : R) : (retr S T g k) (T.b k (g s)) = S.b k s

theorem MultiplicativeBasisDeformations.RaySys.Mor.retr_b_not {V R V' R' : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] [Fintype V'] [DecidableEq V'] [Fintype R'] [DecidableEq R'] (S : Mult V R) (T : Mult V' R') (g : R → R') (k : Type u) [Field k] (t : R') (h : ¬∃ (s : R), g s = t) : (retr S T g k) (T.b k t) = 0

theorem MultiplicativeBasisDeformations.RaySys.Mor.alg_b_g {V R V' R' : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] [Fintype V'] [DecidableEq V'] [Fintype R'] [DecidableEq R'] {S : Mult V R} {T : Mult V' R'} (m : Mor S T) (g : R → R') (hg : ∀ (r : R), m.f r = some (g r)) (k : Type u) [Field k] (s : R) : (m.alg k) (S.b k s) = T.b k (g s)

theorem MultiplicativeBasisDeformations.RaySys.Mor.mul_g {V R V' R' : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] [Fintype V'] [DecidableEq V'] [Fintype R'] [DecidableEq R'] {S : Mult V R} {T : Mult V' R'} (m : Mor S T) (g : R → R') (hg : ∀ (r : R), m.f r = some (g r)) (s s' : R) : T.mul (g s) (g s') = Option.map g (S.mul s s')

theorem MultiplicativeBasisDeformations.RaySys.Mor.retr_alg {V R V' R' : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] [Fintype V'] [DecidableEq V'] [Fintype R'] [DecidableEq R'] {S : Mult V R} {T : Mult V' R'} (m : Mor S T) (g : R → R') (hg : ∀ (r : R), m.f r = some (g r)) (hginj : Function.Injective g) (k : Type u) [Field k] (x : ↥(S.Lin k)) : (retr S T g k) ((m.alg k) x) = x

theorem MultiplicativeBasisDeformations.RaySys.Mor.retr_left {V R V' R' : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] [Fintype V'] [DecidableEq V'] [Fintype R'] [DecidableEq R'] {S : Mult V R} {T : Mult V' R'} (m : Mor S T) (g : R → R') (hg : ∀ (r : R), m.f r = some (g r)) (hginj : Function.Injective g) (hL : ∀ (s : R) (t : R') (t' : R), T.mul (g s) t = some (g t') → ∃ (s' : R), g s' = t) (k : Type u) [Field k] (d : ↥(S.Lin k)) (x : ↥(T.Lin k)) : (retr S T g k) ((m.alg k) d * x) = d * (retr S T g k) x

theorem MultiplicativeBasisDeformations.RaySys.Mor.retr_right {V R V' R' : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] [Fintype V'] [DecidableEq V'] [Fintype R'] [DecidableEq R'] {S : Mult V R} {T : Mult V' R'} (m : Mor S T) (g : R → R') (hg : ∀ (r : R), m.f r = some (g r)) (hginj : Function.Injective g) (hR : ∀ (s : R) (t : R') (t' : R), T.mul t (g s) = some (g t') → ∃ (s' : R), g s' = t) (k : Type u) [Field k] (x : ↥(T.Lin k)) (d : ↥(S.Lin k)) : (retr S T g k) (x * (m.alg k) d) = (retr S T g k) x * d

theorem MultiplicativeBasisDeformations.RaySys.Mor.alg_injective {V R V' R' : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] [Fintype V'] [DecidableEq V'] [Fintype R'] [DecidableEq R'] {S : Mult V R} {T : Mult V' R'} (m : Mor S T) (g : R → R') (hg : ∀ (r : R), m.f r = some (g r)) (hginj : Function.Injective g) (k : Type u) [Field k] : Function.Injective ⇑(m.alg k)

theorem MultiplicativeBasisDeformations.RaySys.Mor.retract_isRepresentationFinite {V R V' R' : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] [Fintype V'] [DecidableEq V'] [Fintype R'] [DecidableEq R'] {S : Mult V R} {T : Mult V' R'} (m : Mor S T) (g : R → R') (hg : ∀ (r : R), m.f r = some (g r)) (hginj : Function.Injective g) (hL : ∀ (s : R) (t : R') (t' : R), T.mul (g s) t = some (g t') → ∃ (s' : R), g s' = t) (hR : ∀ (s : R) (t : R') (t' : R), T.mul t (g s) = some (g t') → ∃ (s' : R), g s' = t) (k : Type u) [Field k] (h : IsRepresentationFinite k ↥(T.Lin k)) : IsRepresentationFinite k ↥(S.Lin k)

Lemma 8.9 for ray tables (lem:representation-transfer).