The basic algebra as a full corner

Lemma 2.1 (graded-category.tex) works with "the basic algebra B₀ = eAe of A, where e = e_1 + ⋯ + e_n is a sum of primitive orthogonal idempotents, one from each isomorphism class of indecomposable projectives". Here: take a complete set f_s of primitive orthogonal idempotents, one representative f_r in each class of f_s A ≅ f_t A, and e = Σ f_r. Then AeA = A (full_basicCorner) and eAe is basic (isBasicAlgebra_basicCorner).

def MultiplicativeBasisDeformations.BasicCorner.IsoData {A : Type v} [Ring A] (a b : A) : Prop

aA ≅ bA, by elements x ∈ aAb, y ∈ bAa with xy = a, yx = b.

theorem MultiplicativeBasisDeformations.BasicCorner.isoData_refl {A : Type v} [Ring A] {a : A} (ha : IsIdempotentElem a) : IsoData a a

theorem MultiplicativeBasisDeformations.BasicCorner.IsoData.symm {A : Type v} [Ring A] {a b : A} (h : IsoData a b) : IsoData b a

theorem MultiplicativeBasisDeformations.BasicCorner.left_of_sandwich {A : Type v} [Ring A] {a b x : A} (ha : IsIdempotentElem a) (h : a * x * b = x) : a * x = x

theorem MultiplicativeBasisDeformations.BasicCorner.right_of_sandwich {A : Type v} [Ring A] {a b x : A} (hb : IsIdempotentElem b) (h : a * x * b = x) : x * b = x

theorem MultiplicativeBasisDeformations.BasicCorner.IsoData.trans {A : Type v} [Ring A] {a b c : A} (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) (hc : IsIdempotentElem c) (h : IsoData a b) (h' : IsoData b c) : IsoData a c

noncomputable def MultiplicativeBasisDeformations.BasicCorner.rep {A : Type v} [Ring A] {n : ℕ} {f : Fin n → A} (hf : CompleteOrthogonalIdempotents f) (s : Fin n) : Fin n

The representative of the class of f_s: the least t with f_t A ≅ f_s A.

theorem MultiplicativeBasisDeformations.BasicCorner.rep_spec {A : Type v} [Ring A] {n : ℕ} {f : Fin n → A} (hf : CompleteOrthogonalIdempotents f) (s : Fin n) : IsoData (f (rep hf s)) (f s)

theorem MultiplicativeBasisDeformations.BasicCorner.rep_eq {A : Type v} [Ring A] {n : ℕ} {f : Fin n → A} (hf : CompleteOrthogonalIdempotents f) {s t : Fin n} (h : IsoData (f s) (f t)) : rep hf s = rep hf t

theorem MultiplicativeBasisDeformations.BasicCorner.rep_rep {A : Type v} [Ring A] {n : ℕ} {f : Fin n → A} (hf : CompleteOrthogonalIdempotents f) (s : Fin n) : rep hf (rep hf s) = rep hf s

noncomputable def MultiplicativeBasisDeformations.BasicCorner.reps {A : Type v} [Ring A] {n : ℕ} {f : Fin n → A} (hf : CompleteOrthogonalIdempotents f) : Finset (Fin n)

The representatives.

noncomputable def MultiplicativeBasisDeformations.BasicCorner.eB {A : Type v} [Ring A] {n : ℕ} {f : Fin n → A} (hf : CompleteOrthogonalIdempotents f) : A

e = Σ_{r} f_r.

theorem MultiplicativeBasisDeformations.BasicCorner.eB_idem {A : Type v} [Ring A] {n : ℕ} {f : Fin n → A} (hf : CompleteOrthogonalIdempotents f) : IsIdempotentElem (eB hf)

theorem MultiplicativeBasisDeformations.BasicCorner.f_mul_eB {A : Type v} [Ring A] {n : ℕ} {f : Fin n → A} (hf : CompleteOrthogonalIdempotents f) {r : Fin n} (hr : r ∈ reps hf) : f r * eB hf = f r

theorem MultiplicativeBasisDeformations.BasicCorner.eB_mul_f {A : Type v} [Ring A] {n : ℕ} {f : Fin n → A} (hf : CompleteOrthogonalIdempotents f) {r : Fin n} (hr : r ∈ reps hf) : eB hf * f r = f r

theorem MultiplicativeBasisDeformations.BasicCorner.full_eB {A : Type v} [Ring A] {k : Type u} [Field k] [Algebra k A] [FiniteDimensional k A] {n : ℕ} {f : Fin n → A} (hf : CompleteOrthogonalIdempotents f) (a : A) : a ∈ Submodule.span k {x : A | ∃ (p : A) (q : A), x = p * eB hf * q}

AeA = A.

theorem MultiplicativeBasisDeformations.BasicCorner.rep_of_mem {A : Type v} [Ring A] {n : ℕ} {f : Fin n → A} (hf : CompleteOrthogonalIdempotents f) {r : Fin n} (hr : r ∈ reps hf) : rep hf r = r

noncomputable def MultiplicativeBasisDeformations.BasicCorner.gB {A : Type v} [Ring A] {n : ℕ} {f : Fin n → A} (hf : CompleteOrthogonalIdempotents f) (j : Fin (reps hf).card) : ⋯.Corner

The idempotents f_r of the corner eAe.

theorem MultiplicativeBasisDeformations.BasicCorner.gB_val {A : Type v} [Ring A] {n : ℕ} {f : Fin n → A} (hf : CompleteOrthogonalIdempotents f) (j : Fin (reps hf).card) : cornerVal ⋯ (gB hf j) = f ↑((reps hf).equivFin.symm j)

theorem MultiplicativeBasisDeformations.BasicCorner.gB_complete {A : Type v} [Ring A] (k : Type u) [Field k] [Algebra k A] [FiniteDimensional k A] {n : ℕ} {f : Fin n → A} (hf : CompleteOrthogonalIdempotents f) : CompleteOrthogonalIdempotents (gB hf)

theorem MultiplicativeBasisDeformations.BasicCorner.gB_primitive {A : Type v} [Ring A] (k : Type u) [Field k] [Algebra k A] [FiniteDimensional k A] {n : ℕ} {f : Fin n → A} (hf : CompleteOrthogonalIdempotents f) (hprim : ∀ (s : Fin n), IsPrimitiveIdempotent (f s)) (j : Fin (reps hf).card) : IsPrimitiveIdempotent (gB hf j)

theorem MultiplicativeBasisDeformations.BasicCorner.gB_basic {A : Type v} [Ring A] {n : ℕ} {f : Fin n → A} (hf : CompleteOrthogonalIdempotents f) (i j : Fin (reps hf).card) (h : ∃ (x : ⋯.Corner) (y : ⋯.Corner), gB hf i * x * gB hf j = x ∧ gB hf j * y * gB hf i = y ∧ x * y = gB hf i ∧ y * x = gB hf j) : i = j

theorem MultiplicativeBasisDeformations.exists_basic_full_corner (k : Type u) [Field k] (A : Type v) [Ring A] [Algebra k A] [FiniteDimensional k A] : ∃ (e : A) (he : IsIdempotentElem e), (∀ (a : A), a ∈ Submodule.span k {x : A | ∃ (p : A) (q : A), x = p * e * q}) ∧ IsBasicAlgebra he.Corner

The basic algebra is a full corner: there is an idempotent e with AeA = A and eAe basic.