Ray products

Lemma 3.6 (projective-rays.tex): "Every unit of R_y is a nonzero scalar times 1 + n with n ∈ rad R_y. Thus changing representatives replaces their product, up to a nonzero scalar and endpoint units, by fh + fnh. The subbimodule M(f,h) is unchanged. If fh ∉ M(f,h), the chain property forces M(f,h) ⊊ U(fh) […] so M(f,h) ⊆ R(fh). Thus the changed product remains in U(fh) ∖ R(fh), is nonzero and has ray [fh]. If fh ∈ M(f,h), the changed product is still in M(f,h)."

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.e_not_mem_radical {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) (y : Fin F.m) : F.e y ∉ algebraRadical k A

e_y ∉ rad A.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.exists_unit_decomp {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {y : Fin F.m} {v : A} (hv : F.IsCornerUnit y v) : ∃ (c : k), c ≠ 0 ∧ v - c • F.e y ∈ F.cornerRadical y

A unit of R_y is c e_y + n, c ≠ 0, n ∈ rad R_y.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.insertionSpan_isEndpoint {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {x y z : Fin F.m} {f h : A} (hf : f ∈ F.corner x y) (hh : h ∈ F.corner y z) : F.IsEndpointSubbimodule x z (F.insertionSpan x y z f h)

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.insertionSpan_le_of_mem_ray {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {x y z : Fin F.m} {f h f' h' : A} (hf' : f' ∈ F.ray x y f) (hh' : h' ∈ F.ray y z h) : F.insertionSpan x y z f' h' ≤ F.insertionSpan x y z f h

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.insertionSpan_eq_of_mem_ray {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {x y z : Fin F.m} {f h f' h' : A} (hf : f ∈ F.corner x y) (hh : h ∈ F.corner y z) (hf' : f' ∈ F.ray x y f) (hh' : h' ∈ F.ray y z h) : F.insertionSpan x y z f' h' = F.insertionSpan x y z f h

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.exists_product_decomp {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {x y z : Fin F.m} {f h f' h' : A} (hf : f ∈ F.corner x y) (hf' : f' ∈ F.ray x y f) (hh' : h' ∈ F.ray y z h) : ∃ (u : A) (w : A) (c : k) (n : A), F.IsCornerUnit x u ∧ F.IsCornerUnit z w ∧ c ≠ 0 ∧ n ∈ F.cornerRadical y ∧ f' * h' = u * (c • (f * h) + f * n * h) * w

Changing representatives: f'h' = u (c fh + f n h) w with units u, w, c ≠ 0 and n ∈ rad R_y.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.mul_mem_insertionSpan {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {x y z : Fin F.m} {f h n : A} (hf : f ∈ F.corner x y) (hh : h ∈ F.corner y z) (hn : n ∈ F.cornerRadical y) : f * n * h ∈ F.insertionSpan x y z f h

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.mem_insertionSpan_of_mem_ray {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {x y z : Fin F.m} {f h f' h' : A} (hf : f ∈ F.corner x y) (hh : h ∈ F.corner y z) (hf' : f' ∈ F.ray x y f) (hh' : h' ∈ F.ray y z h) (hM : f * h ∈ F.insertionSpan x y z f h) : f' * h' ∈ F.insertionSpan x y z f' h'

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.rayProduct_independent_of {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) (hA : IsRepresentationFinite k A) {x y z : Fin F.m} {f f' h h' : A} (hf : f ∈ F.corner x y) (hf0 : f ≠ 0) (hh : h ∈ F.corner y z) (hh0 : h ≠ 0) (hf' : f' ∈ F.ray x y f) (hh' : h' ∈ F.ray y z h) : (f * h ∈ F.insertionSpan x y z f h ↔ f' * h' ∈ F.insertionSpan x y z f' h') ∧ (f * h ∉ F.insertionSpan x y z f h → f' * h' ≠ 0 ∧ F.ray x z (f * h) = F.ray x z (f' * h'))

Lemma 3.6.

def MultiplicativeBasisDeformations.PrimitiveIdempotents.rayProduct {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (F : PrimitiveIdempotents A) (x y z : Fin F.m) (f h : A) : Set A

Definition 3.4, the ray product: [f][h] = [fh] if fh ∉ M(f, h), and the zero ray {0} otherwise.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.rayProduct_eq_of_mem {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) (hA : IsRepresentationFinite k A) {x y z : Fin F.m} {f f' h h' : A} (hf : f ∈ F.corner x y) (hf0 : f ≠ 0) (hh : h ∈ F.corner y z) (hh0 : h ≠ 0) (hf' : f' ∈ F.ray x y f) (hh' : h' ∈ F.ray y z h) : F.rayProduct x y z f h = F.rayProduct x y z f' h'

Lemma 3.6, first part: the ray product does not depend on the representatives.