Rays of an algebra

Section 3 of the manuscript (projective-rays.tex). Fix a complete set of primitive orthogonal idempotents e_x and put A(x, y) = e_x A e_y and R_x = e_x A e_x.

• Definition 3.2 (def:rays): the ray of 0 ≠ f ∈ A(x, y) is the orbit [f] = {u f v : u ∈ R_x^*, v ∈ R_y^*}; U(f) = R_x f R_y and R(f) = (rad R_x) f R_y + R_x f (rad R_y).
• Definition 3.4 (def:ray-product): M(f, h) = R_x f (rad R_y) h R_z; the ray product [f][h] is [fh] if fh ∉ M(f, h) and 0 otherwise.

Formal choices: the units of R_x are the elements of R_x with a two-sided inverse in R_x (identity e_x); rad R_x is R_x ∩ rad A, which is the radical of R_x = e_x A e_x; subbimodules generated by sets are k-spans.

structure MultiplicativeBasisDeformations.PrimitiveIdempotents (A : Type v) [Ring A] : Type v

A chosen complete set of primitive orthogonal idempotents e_x.

• m : ℕ

  The number of idempotents.

• e : Fin self.m → A

  The idempotents.

• complete : CompleteOrthogonalIdempotents self.e
• primitive (x : Fin self.m) : IsPrimitiveIdempotent (self.e x)

def MultiplicativeBasisDeformations.PrimitiveIdempotents.corner {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (F : PrimitiveIdempotents A) (x y : Fin F.m) : Submodule k A

The corner A(x, y) = e_x A e_y, as a k-subspace.

def MultiplicativeBasisDeformations.PrimitiveIdempotents.cornerRadical {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (F : PrimitiveIdempotents A) (x : Fin F.m) : Submodule k A

rad R_x = R_x ∩ rad A.

def MultiplicativeBasisDeformations.PrimitiveIdempotents.IsCornerUnit {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (F : PrimitiveIdempotents A) (x : Fin F.m) (u : A) : Prop

u is a unit of the local corner R_x.

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

Definition 3.2: the ray [f] = {u f v} of f ∈ A(x, y).

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

Definition 3.2: the endpoint subbimodule U(f) = R_x f R_y.

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

Definition 3.2: R(f) = (rad R_x) f R_y + R_x f (rad R_y).

def MultiplicativeBasisDeformations.PrimitiveIdempotents.insertionSpan {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) : Submodule k A

Definition 3.4: M(f, h) = R_x f (rad R_y) h R_z.

def MultiplicativeBasisDeformations.PrimitiveIdempotents.IsEndpointSubbimodule {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (F : PrimitiveIdempotents A) (x y : Fin F.m) (N : Submodule k A) : Prop

An R_x--R_y-subbimodule of the corner A(x, y).

def MultiplicativeBasisDeformations.PrimitiveIdempotents.IsNonzeroRay {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (F : PrimitiveIdempotents A) (s : Set A) : Prop

A nonzero ray: the ray of some nonzero element of a corner.

def MultiplicativeBasisDeformations.PrimitiveIdempotents.NonzeroRay (k : Type u) [Field k] {A : Type v} [Ring A] [Algebra k A] (F : PrimitiveIdempotents A) : Type v

The set of nonzero rays.

def MultiplicativeBasisDeformations.PrimitiveIdempotents.IsRayTransversal {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (F : PrimitiveIdempotents A) (b : NonzeroRay k F → A) : Prop

A choice of one element of every nonzero ray, using e_x for the identity ray [e_x].

def MultiplicativeBasisDeformations.PrimitiveIdempotents.KillsZeroRayProducts {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (F : PrimitiveIdempotents A) (b : NonzeroRay k F → A) : Prop

The representatives b induce an algebra isomorphism k ray A ≅ A (Theorem 11.7(3)): products of representatives whose ray product is zero, that is, which lie in M(f, h), vanish. Together with a multiplicative ray transversal this says that b_r b_s = b_{rs} when rs ≠ 0 and b_r b_s = 0 otherwise.