Right modules, representation-finite algebras, and the radical of ind(mod A)

Conventions of the manuscript (main.tex): modules are finite-dimensional right modules, and maps compose from left to right, so the manuscript's fg is Lean's f ≫ g.

• Right A-modules are modelled as ModuleCat Aᵐᵒᵖ.
• IsRepresentationFinite k A: finitely many isomorphism classes of finite-dimensional indecomposable right modules. Borrowed from the magnitude-conjecture formalization, MagnitudeConjecture/Algebra/RightModuleFiniteType.lean (commit 3ac9f6a22).
• IndSkeleton k A: one representative of each isomorphism class of finite-dimensional indecomposable right modules, indexed by Fin n; the full subcategory on them is ind(mod A).
• The categorical radical J of ind(mod A) and its powers: J(X, Y) is spanned by the radical morphisms f (those with 1 - f g invertible for all g : Y ⟶ X), and J^{n+1}(X, Y) is spanned by composites f g with f radical and g ∈ J^n, all intermediate objects being indecomposable (graded-category.tex).
• Irr(X, Y) = J(X, Y) / J²(X, Y).
• Almost split sequences.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.RightModuleCat (A : Type v) [Ring A] : Type (v + 1)

Right A-modules: left modules over Aᵐᵒᵖ.

def MultiplicativeBasisDeformations.IsFiniteIndecomposable (k : Type u) [Field k] (A : Type v) [Ring A] [Algebra k A] (M : RightModuleCat A) : Prop

A finite-dimensional indecomposable right A-module.

def MultiplicativeBasisDeformations.IsRepresentationFinite (k : Type u) [Field k] (A : Type v) [Ring A] [Algebra k A] : Prop

A is representation-finite: there are finitely many isomorphism classes of finite-dimensional indecomposable right A-modules.

structure MultiplicativeBasisDeformations.IndSkeleton (k : Type u) [Field k] (A : Type v) [Ring A] [Algebra k A] : Type (v + 1)

A complete irredundant list of finite-dimensional indecomposable right A-modules.

• n : ℕ

  The number of isomorphism classes.

• obj : Fin self.n → RightModuleCat A

  The chosen representatives.

• isFiniteIndecomposable (i : Fin self.n) : IsFiniteIndecomposable k A (self.obj i)
• pairwise (i j : Fin self.n) : Nonempty (self.obj i ≅ self.obj j) → i = j
• complete (M : RightModuleCat A) : IsFiniteIndecomposable k A M → ∃ (i : Fin self.n), Nonempty (M ≅ self.obj i)

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.IndSkeleton.Ind {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : IndSkeleton k A) : Type

ind(mod A): the full subcategory on the chosen representatives.

def MultiplicativeBasisDeformations.IndSkeleton.ind {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : IndSkeleton k A) (x : Fin S.n) : S.Ind

The object of ind(mod A) with a given index.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.IndSkeleton.incl {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : IndSkeleton k A) : CategoryTheory.Functor S.Ind (RightModuleCat A)

The inclusion of ind(mod A) into right modules.

def MultiplicativeBasisDeformations.IndSkeleton.IsRadical {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : IndSkeleton k A) {X Y : S.Ind} (f : X ⟶ Y) : Prop

A radical morphism of ind(mod A): 1 - f ≫ g is invertible for every g in the opposite direction.

def MultiplicativeBasisDeformations.IndSkeleton.radPow {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : IndSkeleton k A) : ℕ → (X Y : S.Ind) → Submodule k (X ⟶ Y)

The radical powers J^n(X, Y) of ind(mod A).

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.IndSkeleton.layer {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : IndSkeleton k A) (d : ℕ) (X Y : S.Ind) : Type v

The radical layer J^d(X, Y) / J^{d+1}(X, Y), the degree-d part of the radical grading gr_J ind(mod A).

def MultiplicativeBasisDeformations.IndSkeleton.layerClass {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : IndSkeleton k A) {d : ℕ} {X Y : S.Ind} (f : X ⟶ Y) (hf : f ∈ S.radPow d X Y) : S.layer d X Y

The class in J^d / J^{d+1} of a morphism in J^d.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.IndSkeleton.Irr {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : IndSkeleton k A) (X Y : S.Ind) : Type v

The space of irreducible maps Irr(X, Y) = J(X, Y) / J²(X, Y).

def MultiplicativeBasisDeformations.IndSkeleton.irrClass {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : IndSkeleton k A) {X Y : S.Ind} (f : X ⟶ Y) (hf : f ∈ S.radPow 1 X Y) : S.Irr X Y

The class in Irr(X, Y) of a morphism in J(X, Y).

structure MultiplicativeBasisDeformations.IsRightAlmostSplit {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {E Z : C} (f : E ⟶ Z) : Prop

A right almost split morphism: not a split epimorphism, and every morphism into its target that is not a split epimorphism factors through it. The same definition appears in the vendored library as MBDVendor.QSE.IsRightAlmostSplit.

• not_isSplitEpi : ¬CategoryTheory.IsSplitEpi f
• factors {X : C} (g : X ⟶ Z) : ¬CategoryTheory.IsSplitEpi g → ∃ (h : X ⟶ E), CategoryTheory.CategoryStruct.comp h f = g

structure MultiplicativeBasisDeformations.IsLeftAlmostSplit {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Z E : C} (f : Z ⟶ E) : Prop

The dual notion of a left almost split morphism.

• not_isSplitMono : ¬CategoryTheory.IsSplitMono f
• factors {X : C} (g : Z ⟶ X) : ¬CategoryTheory.IsSplitMono g → ∃ (h : E ⟶ X), CategoryTheory.CategoryStruct.comp f h = g

structure MultiplicativeBasisDeformations.IsAlmostSplitSequence {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {U E V : C} (f : U ⟶ E) (g : E ⟶ V) : Prop

An almost split sequence 0 → U → E → V → 0: a short exact sequence whose first map is left almost split and whose second map is right almost split.

• comp_eq_zero : CategoryTheory.CategoryStruct.comp f g = 0
• shortExact : { X₁ := U, X₂ := E, X₃ := V, f := f, g := g, zero := ⋯ }.ShortExact
• left : IsLeftAlmostSplit f
• right : IsRightAlmostSplit g