Lemma 5.2: object quotients have bricks

lem:deletion-brick (mesh-deformations.tex): "Among the objects outside Σ, choose X of least composition length. Every radical endomorphism of X factors through its proper image. Each indecomposable summand of that image has smaller length, belongs to D by image-closure, and therefore belongs to Σ. Hence the radical of End(X) becomes zero in the quotient. Its identity remains nonzero … Thus its quotient endomorphism ring is its residue division algebra." "By Proposition 2.10, this applies to C as ind(mod A₀)."

We run this argument for C through the evaluation ev : add C ≃ mod A₀ (full faithfulness and essential surjectivity, Lemma 2.9 and Proposition 2.10): the length of X is dim ev(X), the image of ev(r) is ev(W) for a family W of smaller labels, and r factors through W.

def MultiplicativeBasisDeformations.CatAlg.MeshData.matMul {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} {F : ι → 𝒞} {κ κ' κ'' : Type} [Fintype κ'] {Z : κ → ι} {Z' : κ' → ι} {Z'' : κ'' → ι} (α : Mat F Z Z') (β : Mat F Z' Z'') : Mat F Z Z''

Composition of matrices (first α, then β).

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.evMap_comp {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) {κ κ' κ'' : Type} [Fintype κ] [DecidableEq κ] [Fintype κ'] [DecidableEq κ'] [Fintype κ''] [DecidableEq κ''] {Z : κ → ι} {Z' : κ' → ι} {Z'' : κ'' → ι} (α : Mat F Z Z') (β : Mat F Z' Z'') : D.evMap β ∘ₗ D.evMap α = D.evMap (matMul α β)

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.evMap_sub {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) {κ κ' : Type} [Fintype κ] [DecidableEq κ] [Fintype κ'] [DecidableEq κ'] {Z : κ → ι} {Z' : κ' → ι} (f g : Mat F Z Z') : D.evMap (f - g) = D.evMap f - D.evMap g

def MultiplicativeBasisDeformations.CatAlg.MeshData.through {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} (F : ι → 𝒞) (Sg : Set ι) (x y : ι) : Submodule k (F x ⟶ F y)

The maps through objects of Σ.

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.through_le_rad {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (Sg : Set ι) {x : ι} (hx : x ∉ Sg) : through F Sg x x ≤ L.rad x x

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.brick {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] (J : D.InjData) (Sg : Set ι) (hne : ∃ (x : ι), x ∉ Sg) : ∃ x ∉ Sg, L.rad x x ≤ through F Sg x x

Lemma 5.2 for C: a label outside Σ of least evaluation dimension has all its radical endomorphisms factoring through Σ.