Rays and ray transversals

Definition 3.2 and Corollary 3.3 (projective-rays.tex). For 0 ≠ f ∈ A(x, y), U(f) = R_x f R_y is uniserial with radical R(f), its unique maximal subbimodule (le_endpointRadical), and "[f] = U(f) ∖ R(f)" (eq:ray-layer; here mem_ray_iff). Corollary 3.3: "In each corner, the chosen vectors represent the consecutive one-dimensional quotients of a finite chain. They therefore form a basis adapted to every member of that chain."

Units of the local corners

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.isCornerUnit_e {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) (x : Fin F.m) : F.IsCornerUnit x (F.e x)

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.cornerUnit_mul {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {x : Fin F.m} {u w : A} (hu : F.IsCornerUnit x u) (hw : F.IsCornerUnit x w) : F.IsCornerUnit x (u * w)

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.cornerUnit_inv {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {x : Fin F.m} {u : A} (hu : F.IsCornerUnit x u) : ∃ (u' : A), F.IsCornerUnit x u' ∧ u * u' = F.e x ∧ u' * u = F.e x

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.cornerVal_pow_succ {A : Type v} [Ring A] {e : A} (he : IsIdempotentElem e) (z : he.Corner) (n : ℕ) : cornerVal he (z ^ (n + 1)) = cornerVal he z ^ (n + 1)

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.isCornerUnit_of_not_mem {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {x : Fin F.m} {a : A} (ha : a ∈ F.corner x x) (ha' : a ∉ F.cornerRadical x) : F.IsCornerUnit x a

An element of R_x outside rad R_x is a unit.

Rays

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.mem_ray_self {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {x y : Fin F.m} {f : A} (hf : f ∈ F.corner x y) : f ∈ F.ray x y f

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.ray_subset_corner {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {x y : Fin F.m} {f g : A} (hf : f ∈ F.corner x y) (hg : g ∈ F.ray x y f) : g ∈ F.corner x y

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.ray_eq_of_mem {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {x y : Fin F.m} {f g : A} (hf : f ∈ F.corner x y) (hg : g ∈ F.ray x y f) : F.ray x y g = F.ray x y f

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.ne_zero_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 : Fin F.m} {f g : A} (hf : f ∈ F.corner x y) (hf0 : f ≠ 0) (hg : g ∈ F.ray x y f) : g ≠ 0

Cyclic subbimodules

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.endpointSpan_le {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {x y : Fin F.m} {N : Submodule k A} (hN : F.IsEndpointSubbimodule x y N) {g : A} (hg : g ∈ N) : F.endpointSpan x y g ≤ N

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.endpointRadical_le {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {x y : Fin F.m} {g : A} (hg : g ∈ F.corner x y) : F.endpointRadical x y g ≤ F.cornerRadical x * F.endpointSpan x y g ⊔ F.endpointSpan x y g * F.cornerRadical y

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.not_mem_endpointRadical {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {x y : Fin F.m} {g : A} (hg : g ∈ F.corner x y) (hg0 : g ≠ 0) : g ∉ F.endpointRadical x y g

f ∉ R(f) for f ≠ 0, by Nakayama's lemma.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.le_endpointRadical {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 : Fin F.m} {g : A} (hg : g ∈ F.corner x y) {N : Submodule k A} (hN : F.IsEndpointSubbimodule x y N) (hNU : N ≤ F.endpointSpan x y g) (hgN : g ∉ N) : N ≤ F.endpointRadical x y g

R(f) is the unique maximal subbimodule of U(f).

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.mem_ray_iff {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 : Fin F.m} {f : A} (hf : f ∈ F.corner x y) (hf0 : f ≠ 0) (g : A) : g ∈ F.ray x y f ↔ g ∈ F.endpointSpan x y f ∧ g ∉ F.endpointRadical x y f

[f] = U(f) ∖ R(f) (eq:ray-layer).

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.ray_eq_of_endpointSpan_eq {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 : Fin F.m} {f g : A} (hf : f ∈ F.corner x y) (hf0 : f ≠ 0) (hg : g ∈ F.corner x y) (h : F.endpointSpan x y g = F.endpointSpan x y f) : F.ray x y g = F.ray x y f

A ray is determined by its subbimodule.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.endpointSpan_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 : Fin F.m} {f g : A} (hf : f ∈ F.corner x y) (hg : g ∈ F.ray x y f) : F.endpointSpan x y g = F.endpointSpan x y f

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.exists_cyclic {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 : Fin F.m} {N : Submodule k A} (hN : F.IsEndpointSubbimodule x y N) (hN0 : N ≠ ⊥) : ∃ g ∈ N, g ≠ 0 ∧ N = F.endpointSpan x y g

Every nonzero subbimodule is cyclic: N = U(g), g taken outside the largest subbimodule below N.

Ray transversals

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.corner_unique {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {x y x' y' : Fin F.m} {f : A} (hf : f ∈ F.corner x y) (hf' : f ∈ F.corner x' y') (hf0 : f ≠ 0) : x = x' ∧ y = y'

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.proj_corner_of_mem {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {x y x' y' : Fin F.m} {f : A} (hf : f ∈ F.corner x' y') : F.e x * f * F.e y = if f ∈ F.corner x y then f else 0

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.transversal_spec {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {b : NonzeroRay k F → A} (hb : F.IsRayTransversal b) (s : NonzeroRay k F) : ∃ (x : Fin F.m) (y : Fin F.m), b s ∈ F.corner x y ∧ b s ≠ 0 ∧ ↑s = F.ray x y (b s)

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.transversal_ray {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {b : NonzeroRay k F → A} (hb : F.IsRayTransversal b) {x y : Fin F.m} (s : NonzeroRay k F) (hs : b s ∈ F.corner x y) : ↑s = F.ray x y (b s)

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.transversal_ext {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {b : NonzeroRay k F → A} (hb : F.IsRayTransversal b) (hA : IsRepresentationFinite k A) {x y : Fin F.m} {s s' : NonzeroRay k F} (hs : b s ∈ F.corner x y) (hs' : b s' ∈ F.corner x y) (h : F.endpointSpan x y (b s) = F.endpointSpan x y (b s')) : s = s'

Distinct rays of a corner have distinct subbimodules.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.le_span_transversal {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {b : NonzeroRay k F → A} (hb : F.IsRayTransversal b) (hA : IsRepresentationFinite k A) {x y : Fin F.m} (n : ℕ) (N : Submodule k A) : Module.finrank k ↥N = n → F.IsEndpointSubbimodule x y N → N ≤ Submodule.span k (b '' {s : NonzeroRay k F | b s ∈ N})

The transversal spans every subbimodule of a corner.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.eq_sum_corners {A : Type v} [Ring A] (F : PrimitiveIdempotents A) (a : A) : a = ∑ x : Fin F.m, ∑ y : Fin F.m, F.e x * a * F.e y

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.corner_isEndpoint {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) (x y : Fin F.m) : F.IsEndpointSubbimodule x y (F.corner x y)

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.eAe_mem_corner {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) (x y : Fin F.m) (a : A) : F.e x * a * F.e y ∈ F.corner x y

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.span_transversal {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {b : NonzeroRay k F → A} (hb : F.IsRayTransversal b) (hA : IsRepresentationFinite k A) : Submodule.span k (Set.range b) = ⊤

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.linearIndependent_transversal {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {b : NonzeroRay k F → A} (hb : F.IsRayTransversal b) (hA : IsRepresentationFinite k A) : LinearIndependent k b

def MultiplicativeBasisDeformations.PrimitiveIdempotents.idealSubmodule {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (I : TwoSidedIdeal A) : Submodule k A

A two-sided ideal as a k-subspace.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.rayTransversal_isBasis {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {b : NonzeroRay k F → A} (hb : F.IsRayTransversal b) (hA : IsRepresentationFinite k A) : LinearIndependent k b ∧ Submodule.span k (Set.range b) = ⊤ ∧ ∀ (I : TwoSidedIdeal A) (a : A), a ∈ I ↔ a ∈ Submodule.span k (b '' {r : NonzeroRay k F | b r ∈ I})

Corollary 3.3.