Multiplicative bases

MultiplicativeBasisDeformations.Foundations.DeletionBrickAbstract

Lemma 5.2 in its abstract form #

mesh-deformations.tex (lem:deletion-brick): "Let π’Ÿ be a full additive subcategory of a finite-length k-linear abelian category, closed under images and direct summands. Assume finite-dimensional Hom spaces and Krull–Schmidt decomposition. For any set Ξ£ of indecomposable isomorphism classes, every nonempty quotient ind π’Ÿ/[Ξ£] has an object whose endomorphism ring is a division algebra. If all residue division algebras are k, the quotient has a brick."

Proof (as in the source): among the objects of ind π’Ÿ outside Ξ£, take one, X, minimal among subobjects of a fixed object (the descending chain condition, IsArtinianObject). A radical endomorphism f of X is not epi (an epi endomorphism of an object with finite-dimensional endomorphisms is invertible, isUnit_of_epi), so it factors through its proper image; the indecomposable summands of the image are smaller, lie in π’Ÿ by image-closure, hence in Ξ£. Conversely a map through Ξ£ is a radical endomorphism: an invertible one would make X a summand of an indecomposable object of Ξ£ (not_isUnit_through). Hence End(X)/[Ξ£](X, X) = End(X)/rad, the residue division algebra (deletionBrick). Indecomposable objects are those with local endomorphism rings (Krull–Schmidt); closure under summands is not needed.

source
def MultiplicativeBasisDeformations.AbstractBrick.Through {π’œ : Type v} [CategoryTheory.Category.{w, v} π’œ] [CategoryTheory.Abelian π’œ] (Sg : π’œ β†’ Prop) {X Y : π’œ} (f : X ⟢ Y) :
Prop

Morphisms factoring through a finite family of objects of Ξ£ (the ideal [Ξ£]).

Instances For
    source
    theorem MultiplicativeBasisDeformations.AbstractBrick.isIso_of_epi_end {k : Type u} [Field k] {π’œ : Type v} [CategoryTheory.Category.{w, v} π’œ] [CategoryTheory.Abelian π’œ] [CategoryTheory.Linear k π’œ] [βˆ€ (X Y : π’œ), FiniteDimensional k (X ⟢ Y)] {X : π’œ} (f : X ⟢ X) [CategoryTheory.Epi f] :
    CategoryTheory.IsIso f

    An epi endomorphism of an object with finite-dimensional endomorphisms is invertible.

    source
    theorem MultiplicativeBasisDeformations.AbstractBrick.nontrivial_end {π’œ : Type v} [CategoryTheory.Category.{w, v} π’œ] [CategoryTheory.Abelian π’œ] {X : π’œ} [IsLocalRing (CategoryTheory.End X)] :
    CategoryTheory.CategoryStruct.id X β‰  0
    source
    theorem MultiplicativeBasisDeformations.AbstractBrick.not_isIso_comp {π’œ : Type v} [CategoryTheory.Category.{w, v} π’œ] [CategoryTheory.Abelian π’œ] {X Z : π’œ} [IsLocalRing (CategoryTheory.End X)] [hZ : IsLocalRing (CategoryTheory.End Z)] (g : X ⟢ Z) (h : Z ⟢ X) (hnot : Β¬Nonempty (X β‰… Z)) :
    Β¬CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp g h)

    An isomorphism cannot factor through an indecomposable object not isomorphic to X.

    source
    theorem MultiplicativeBasisDeformations.AbstractBrick.not_isIso_through {π’œ : Type v} [CategoryTheory.Category.{w, v} π’œ] [CategoryTheory.Abelian π’œ] {Sg : π’œ β†’ Prop} (hSloc : βˆ€ (X : π’œ), Sg X β†’ IsLocalRing (CategoryTheory.End X)) (hSiso : βˆ€ {X Y : π’œ} (a : X β‰… Y), Sg Y β†’ Sg X) {X : π’œ} [IsLocalRing (CategoryTheory.End X)] (hX : Β¬Sg X) {f : X ⟢ X} (hf : Through Sg f) :
    Β¬CategoryTheory.IsIso f

    Maps through Ξ£ are radical, when X is not isomorphic to an object of Ξ£.

    source
    theorem MultiplicativeBasisDeformations.AbstractBrick.isLocalRing_of_iso {π’œ : Type v} [CategoryTheory.Category.{w, v} π’œ] [CategoryTheory.Abelian π’œ] {X Y : π’œ} (e : X β‰… Y) [IsLocalRing (CategoryTheory.End Y)] :
    IsLocalRing (CategoryTheory.End X)

    Local endomorphism rings are invariant under isomorphism.

    source
    theorem MultiplicativeBasisDeformations.AbstractBrick.deletionBrick {k : Type u} [Field k] {π’œ : Type v} [CategoryTheory.Category.{w, v} π’œ] [CategoryTheory.Abelian π’œ] [CategoryTheory.Linear k π’œ] [βˆ€ (X Y : π’œ), FiniteDimensional k (X ⟢ Y)] [βˆ€ (X : π’œ), CategoryTheory.IsArtinianObject X] [CategoryTheory.Limits.HasFiniteBiproducts π’œ] (D : π’œ β†’ Prop) (hDiso : βˆ€ {X Y : π’œ} (a : X β‰… Y), D Y β†’ D X) (hDim : βˆ€ {X Y : π’œ} (f : X ⟢ Y), D X β†’ D Y β†’ D (CategoryTheory.Limits.image f)) (hKS : βˆ€ (X : π’œ), D X β†’ βˆƒ (n : β„•) (Y : Fin n β†’ π’œ), (βˆ€ (i : Fin n), D (Y i) ∧ IsLocalRing (CategoryTheory.End (Y i))) ∧ Nonempty (X β‰… ⨁ Y)) (Sg : π’œ β†’ Prop) (hSloc : βˆ€ (X : π’œ), Sg X β†’ IsLocalRing (CategoryTheory.End X)) (hSiso : βˆ€ {X Y : π’œ} (a : X β‰… Y), Sg Y β†’ Sg X) (hne : βˆƒ (X : π’œ), D X ∧ IsLocalRing (CategoryTheory.End X) ∧ Β¬Sg X) :
    βˆƒ (X : π’œ), D X ∧ IsLocalRing (CategoryTheory.End X) ∧ Β¬Sg X ∧ (βˆ€ (f : X ⟢ X), Through Sg f ↔ Β¬CategoryTheory.IsIso f) ∧ ((βˆ€ (f : X ⟢ X), βˆƒ (c : k), Β¬CategoryTheory.IsIso (f - c β€’ CategoryTheory.CategoryStruct.id X)) β†’ βˆ€ (f : X ⟢ X), βˆƒ (c : k), Through Sg (f - c β€’ CategoryTheory.CategoryStruct.id X))

    Lemma 5.2 (lem:deletion-brick), abstract form. In a k-linear abelian category with finite-dimensional Hom spaces in which every object is Artinian, let π’Ÿ be a subcategory closed under isomorphisms and images, in which every object is a finite direct sum of objects with local endomorphism rings (Krull–Schmidt), and let Ξ£ be a set of objects with local endomorphism rings, closed under isomorphisms. If some indecomposable object of π’Ÿ lies outside Ξ£, there is one, X, such that the endomorphisms of X factoring through Ξ£ are exactly the non-invertible ones: the endomorphism ring of X in ind π’Ÿ/[Ξ£] is the residue division algebra End(X)/rad. If that residue algebra is k, X is a brick of the quotient.