Endpoint subbimodules form chains

Lemma 3.1(3) (lem:endpoint-chains, projective-rays.tex). For a representation-finite algebra A over an algebraically closed field with primitive idempotents e_x, put R_x = e_xAe_x.

• Each R_x is local with residue field k: R_x = k e_x + rad R_x, with rad R_x = R_x ∩ rad A nilpotent.
• An R_x--R_y-subbimodule N of A(x, y) is recovered from the ideal it generates, e_x(ANA)e_y = N; so there are finitely many.
• Two incomparable subbimodules would give k² in the socle of (N₁ + N₂)/(N₁ ∩ N₂), whose infinitely many lines lift to distinct subbimodules; so the subbimodules form a chain, with one-dimensional successive quotients.
• For f ≠ 0, R_xfR_y = R_xf or fR_y.

theorem MultiplicativeBasisDeformations.isUnit_one_sub_mul_of_comm {R : Type u_1} [Ring R] {a b : R} (h : IsUnit (1 - b * a)) : IsUnit (1 - a * b)

Jacobson's lemma.

theorem MultiplicativeBasisDeformations.mem_jacobson_of_forall_isUnit {R : Type u_1} [Ring R] {x : R} (h : ∀ (y : R), IsUnit (1 - y * x)) : x ∈ Ring.jacobson R

An element x with 1 - yx invertible for all y lies in the Jacobson radical.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.corner_isLocalRing (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) : IsLocalRing ⋯.Corner

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.mem_corner_iff' {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} : a ∈ F.corner x y ↔ F.e x * a * F.e y = a

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.corner_mem_sub {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) : a ∈ Subsemigroup.corner (F.e x)

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.exists_sub_smul_mem_radical (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) : ∃ (c : k), a - c • F.e x ∈ algebraRadical k A

R_x = k e_x + rad R_x.

theorem MultiplicativeBasisDeformations.algebraRadical_pow_eq_bot {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] : ∃ (K : ℕ), algebraRadical k A ^ K = ⊥

The radical of a finite-dimensional algebra is nilpotent.

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

The two-sided ideal generated by a subspace: the span of all a n b.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.mem_genIdeal_iff {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] {N : Submodule k A} {z : A} : z ∈ genIdeal N ↔ z ∈ Submodule.span k {z : A | ∃ (a : A) (b : A), ∃ n ∈ N, z = a * n * b}

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.mem_genIdeal {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] {N : Submodule k A} {n : A} (hn : n ∈ N) : n ∈ genIdeal N

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.corner_mul_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} {n : A} (hn : n ∈ F.corner x y) : F.e x * n = n ∧ n * F.e y = n

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.eAe_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) : F.e x * a * F.e x ∈ F.corner x x

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.genIdeal_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} {N : Submodule k A} (hN : F.IsEndpointSubbimodule x y N) {z : A} (hz : z ∈ genIdeal N) : F.e x * z * F.e y ∈ N

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.finite_subbimodules {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 | F.IsEndpointSubbimodule x y N}.Finite

Finitely many endpoint subbimodules: each is recovered from the ideal it generates.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.cornerRadical_le_corner {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.cornerRadical x ≤ F.corner x x

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.cornerRadical_le_radical {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.cornerRadical x ≤ algebraRadical k A

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.cornerRadical_pow_eq_bot {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) : ∃ (K : ℕ), ∀ (x : Fin F.m), F.cornerRadical x ^ K = ⊥

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.le_of_le_rad {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} {P L : Submodule k A} (hL₁ : F.cornerRadical x * L ≤ L) (hL₂ : L * F.cornerRadical y ≤ L) (hP : P ≤ F.cornerRadical x * P ⊔ P * F.cornerRadical y ⊔ L) : P ≤ L

Nakayama's lemma for subbimodules. If P ≤ (rad R_x) P + P (rad R_y) + L for a subbimodule L, then P ≤ L.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.e_mem_corner {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.e x ∈ F.corner x x

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.isEndpoint_sup {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 N' : Submodule k A} (h : F.IsEndpointSubbimodule x y N) (h' : F.IsEndpointSubbimodule x y N') : F.IsEndpointSubbimodule x y (N ⊔ N')

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.isEndpoint_inf {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 N' : Submodule k A} (h : F.IsEndpointSubbimodule x y N) (h' : F.IsEndpointSubbimodule x y N') : F.IsEndpointSubbimodule x y (N ⊓ N')

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.radL_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 r : A} (ha : a ∈ F.corner x x) (hr : r ∈ F.cornerRadical x) : a * r ∈ F.cornerRadical x

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.radR_mem {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} {b r : A} (hb : b ∈ F.corner y y) (hr : r ∈ F.cornerRadical y) : r * b ∈ F.cornerRadical y

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.isEndpoint_rad {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} (h : F.IsEndpointSubbimodule x y N) : F.IsEndpointSubbimodule x y (F.cornerRadical x * N ⊔ N * F.cornerRadical y)

(rad R_x) N + N (rad R_y) is a subbimodule.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.isEndpoint_between {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 N' P : Submodule k A} (hN : F.IsEndpointSubbimodule x y N) (h1 : N' ≤ P) (h2 : P ≤ N) (hr : F.cornerRadical x * N ⊔ N * F.cornerRadical y ≤ N') : F.IsEndpointSubbimodule x y P

Subspaces between N' and N, where N/N' is killed by the radicals, are subbimodules.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.exists_socle_layer {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} {L N : Submodule k A} (hL : F.IsEndpointSubbimodule x y L) (hN : F.IsEndpointSubbimodule x y N) (hLN : L < N) : ∃ (P : Submodule k A), F.IsEndpointSubbimodule x y P ∧ L < P ∧ P ≤ N ∧ F.cornerRadical x * P ⊔ P * F.cornerRadical y ≤ L

A subbimodule properly above L ≤ N inside N has a minimal member P with (rad R_x) P + P (rad R_y) ≤ L.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.isChain_subbimodules {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) : IsChain (fun (x1 x2 : Submodule k A) => x1 ≤ x2) {N : Submodule k A | F.IsEndpointSubbimodule x y N}

Lemma 3.1(3): the endpoint subbimodules form a chain.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.finrank_succ_of_consecutive {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 N' : Submodule k A} (hN : F.IsEndpointSubbimodule x y N) (hN' : F.IsEndpointSubbimodule x y N') (hlt : N < N') (hcons : ∀ (N'' : Submodule k A), F.IsEndpointSubbimodule x y N'' → N ≤ N'' → N'' ≤ N' → N'' = N ∨ N'' = N') : Module.finrank k ↥N' = Module.finrank k ↥N + 1

Consecutive endpoint subbimodules have one-dimensional quotient.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.endpointSpan_one_sided {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) : F.endpointSpan x y f = Submodule.span k {g : A | ∃ a ∈ F.corner x x, g = a * f} ∨ F.endpointSpan x y f = Submodule.span k {g : A | ∃ b ∈ F.corner y y, g = f * b}

Lemma 3.1(3), last part: R_x f R_y = R_x f or f R_y.