The opposite ray system

The paper proves many statements together with "the dual assertion", obtained "by passing to the opposite algebra". Tab.op reverses rays and products; its linearization is the opposite algebra of kP (linOpEquiv), so it is representation-finite when kP is (isRepresentationFinite_op); Sys.op carries Setting 8.4 over.

def MultiplicativeBasisDeformations.RaySys.Tab.op {V R L : Type} [AddCommGroup L] (P : Tab V R L) : Tab V R L

The opposite ray table.

@[simp]

theorem MultiplicativeBasisDeformations.RaySys.Tab.op_src {V R L : Type} [AddCommGroup L] (P : Tab V R L) : P.op.src = P.tgt

@[simp]

theorem MultiplicativeBasisDeformations.RaySys.Tab.op_tgt {V R L : Type} [AddCommGroup L] (P : Tab V R L) : P.op.tgt = P.src

@[simp]

theorem MultiplicativeBasisDeformations.RaySys.Tab.op_e {V R L : Type} [AddCommGroup L] (P : Tab V R L) : P.op.e = P.e

@[simp]

theorem MultiplicativeBasisDeformations.RaySys.Tab.op_mul {V R L : Type} [AddCommGroup L] (P : Tab V R L) (r s : R) : P.op.mul r s = P.mul s r

@[simp]

theorem MultiplicativeBasisDeformations.RaySys.Tab.op_wt {V R L : Type} [AddCommGroup L] (P : Tab V R L) : P.op.wt = P.wt

@[simp]

theorem MultiplicativeBasisDeformations.RaySys.Tab.op_deg {V R L : Type} [AddCommGroup L] (P : Tab V R L) : P.op.deg = P.deg

theorem MultiplicativeBasisDeformations.RaySys.Tab.op_emul {V R L : Type} [AddCommGroup L] (P : Tab V R L) (a b : Elt R) : P.op.emul a b = P.emul b a

def MultiplicativeBasisDeformations.RaySys.Tab.toOp {V R L : Type} [AddCommGroup L] (P : Tab V R L) (a : M P.toMult) : M P.op.toMult

Elements of the monoid with zero of the opposite table.

theorem MultiplicativeBasisDeformations.RaySys.Tab.toOp_mul {V R L : Type} [AddCommGroup L] (P : Tab V R L) (a b : M P.toMult) : P.toOp (a * b) = P.toOp b * P.toOp a

theorem MultiplicativeBasisDeformations.RaySys.Tab.toOp_one {V R L : Type} [AddCommGroup L] (P : Tab V R L) : P.toOp 1 = 1

theorem MultiplicativeBasisDeformations.RaySys.Tab.toOp_zero {V R L : Type} [AddCommGroup L] (P : Tab V R L) : P.toOp 0 = 0

theorem MultiplicativeBasisDeformations.RaySys.Tab.toOp_rr {V R L : Type} [AddCommGroup L] (P : Tab V R L) (r : R) : P.toOp (P.rr r) = P.op.rr r

theorem MultiplicativeBasisDeformations.RaySys.Tab.toOp_injective {V R L : Type} [AddCommGroup L] (P : Tab V R L) : Function.Injective P.toOp

theorem MultiplicativeBasisDeformations.RaySys.Tab.toOp_pow {V R L : Type} [AddCommGroup L] (P : Tab V R L) (a : M P.toMult) (n : ℕ) : P.toOp (a ^ n) = P.toOp a ^ n

theorem MultiplicativeBasisDeformations.RaySys.Tab.toOp_eq_zero {V R L : Type} [AddCommGroup L] (P : Tab V R L) {a : M P.toMult} : P.toOp a = 0 ↔ a = 0

noncomputable def MultiplicativeBasisDeformations.RaySys.Tab.linOpL {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] : ↥(P.op.Lin k) ≃ₗ[k] (↥(P.Lin k))ᵐᵒᵖ

The linear identification of k(P^op) with kP.

theorem MultiplicativeBasisDeformations.RaySys.Tab.linOpL_b {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] (r : R) : (P.linOpL k) (P.op.b k r) = MulOpposite.op (P.b k r)

theorem MultiplicativeBasisDeformations.RaySys.Tab.linOpL_mul {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] (x y : ↥(P.op.Lin k)) : (P.linOpL k) (x * y) = (P.linOpL k) x * (P.linOpL k) y

theorem MultiplicativeBasisDeformations.RaySys.Tab.linOpL_one {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] : (P.linOpL k) 1 = 1

noncomputable def MultiplicativeBasisDeformations.RaySys.Tab.linOpEquiv {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] : ↥(P.op.Lin k) ≃ₐ[k] (↥(P.Lin k))ᵐᵒᵖ

The linearization of the opposite table is the opposite algebra.

theorem MultiplicativeBasisDeformations.RaySys.Tab.op_isRepresentationFinite {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] (h : IsRepresentationFinite k ↥(P.Lin k)) : IsRepresentationFinite k ↥(P.op.Lin k)

The opposite table is representation-finite with kP.

theorem MultiplicativeBasisDeformations.RaySys.Sys.toOp_mul3 {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (a b c : M P.toMult) : P.toOp (a * b * c) = P.toOp c * P.toOp b * P.toOp a

@[reducible]

def MultiplicativeBasisDeformations.RaySys.Sys.op {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) : Sys V R L

The opposite ray system (Setting 8.4 for A₀ᵒᵖ).

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_rr {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r : R) : S.op.rr r = S.P.toOp (S.rr r)

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_q {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (x : V) : S.op.q x = S.P.toOp (S.q x)

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_P {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) : S.op.P = S.P.op

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_wtM {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (a : M S.P.toMult) : S.op.wtM (S.P.toOp a) = S.wtM a

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_χ {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (x : V) : S.op.χ x = S.χ x

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_cycL_iff {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (f : R) : S.op.CycL f ↔ S.CycR f

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_cycR_iff {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (f : R) : S.op.CycR f ↔ S.CycL f

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_inU_iff {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (s r : R) : S.op.InU s r ↔ S.InU s r

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_isGen_iff {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (f : R) : S.op.IsGen f ↔ S.IsGen f

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_rf_iff {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r s : R) : S.P.op.RF r s ↔ S.P.LF s r

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_lf_iff {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r s : R) : S.P.op.LF r s ↔ S.P.RF s r