Independent statement of Theorems A and B

These definitions use only Mathlib. They state the two main theorems of Multiplicative bases and deformations of representation-finite algebras:

• Theorem A. Every finite-dimensional representation-finite algebra over an algebraically closed field has a normed multiplicative basis.
• Theorem B. Every basic finite-dimensional representation-finite algebra over an algebraically closed field of characteristic different from two is standard.

Modules are right modules, that is, modules over the opposite algebra. Connections to the proof library are proved in separate modules.

Representation-finite algebras

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

One representative of each isomorphism class of finite-dimensional indecomposable right modules. Existence of such a family expresses finite representation type.

• size : ℕ
• obj : Fin self.size → ModuleCat Aᵐᵒᵖ
• finite (i : Fin self.size) : Module.Finite k ↑(self.obj i)
• indecomposable (i : Fin self.size) : CategoryTheory.Indecomposable (self.obj i)
• distinct {i j : Fin self.size} : Nonempty (self.obj i ≅ self.obj j) → i = j
• complete (M : ModuleCat Aᵐᵒᵖ) : Module.Finite k ↑M → CategoryTheory.Indecomposable M → ∃ (i : Fin self.size), Nonempty (M ≅ self.obj i)

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

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

Normed multiplicative bases

def MultiplicativeBasisDeformations.Statement.radicalPow (k A : Type u) [Field k] [Ring A] [Algebra k A] (n : ℕ) : Submodule k A

The power (rad A)^n of the Jacobson radical, as a k-subspace of A.

def MultiplicativeBasisDeformations.Statement.IsPrimitiveIdempotent {A : Type u} [Ring A] (e : A) : Prop

A primitive idempotent: a nonzero idempotent e such that the only idempotents of the corner eAe are 0 and e.

structure MultiplicativeBasisDeformations.Statement.IsNormedMultiplicativeBasis {k A : Type u} [Field k] [Ring A] [Algebra k A] {ι : Type u_1} (b : Module.Basis ι k A) : Prop

A normed multiplicative basis: products of basis elements are zero or basis elements; the basis contains a complete set of primitive orthogonal idempotents; and it meets every radical power (rad A)^n, n ≥ 1, in a basis of that power.

• multiplicative (i j : ι) : b i * b j = 0 ∨ ∃ (l : ι), b i * b j = b l
• idempotents : ∃ (E : Finset ι), (CompleteOrthogonalIdempotents fun (i : ↥E) => b ↑i) ∧ ∀ i ∈ E, IsPrimitiveIdempotent (b i)
• radicalPow (n : ℕ) : 1 ≤ n → Submodule.span k (⇑b '' {i : ι | b i ∈ Statement.radicalPow k A n}) = Statement.radicalPow k A n

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

A has a normed multiplicative basis.

def MultiplicativeBasisDeformations.Statement.TheoremA (k A : Type u) [Field k] [Ring A] [Algebra k A] [IsAlgClosed k] [FiniteDimensional k A] : Prop

Theorem A, as a proposition: a finite-dimensional representation-finite algebra over an algebraically closed field has a normed multiplicative basis.

Basic algebras

def MultiplicativeBasisDeformations.Statement.IsBasic (A : Type u) [Ring A] : Prop

A is basic: it has a complete set of primitive orthogonal idempotents e_i whose principal right ideals e_i A are pairwise nonisomorphic. Here e_i A ≅ e_j A is expressed by elements x ∈ e_i A e_j, y ∈ e_j A e_i with xy = e_i and yx = e_j.

The Auslander–Reiten quiver

@[reducible, inline]

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

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

def MultiplicativeBasisDeformations.Statement.IsRadical {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) {X Y : Ind S} (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.Statement.radPow {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) : ℕ → (X Y : Ind S) → Submodule k (X ⟶ Y)

The powers J^n(X, Y) of the radical of ind(mod A): J⁰ = Hom, and J^{n+1}(X, Y) is spanned by the composites f ≫ g of a radical morphism f : X ⟶ Z and some g ∈ J^n(Z, Y).

@[reducible, inline]

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

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

def MultiplicativeBasisDeformations.Statement.Vertex {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) : Type

The vertices of the Auslander–Reiten quiver Γ_A.

@[instance_reducible]

instance MultiplicativeBasisDeformations.Statement.arQuiver {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) : Quiver (Vertex S)

The Auslander–Reiten quiver Γ_A: the arrows i ⟶ j are indexed by a basis of Irr(X_i, X_j).

@[instance_reducible]

instance MultiplicativeBasisDeformations.Statement.instFintypeVertex {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) : Fintype (Vertex S)

@[instance_reducible]

noncomputable instance MultiplicativeBasisDeformations.Statement.instFintypeHomVertex {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) (i j : Vertex S) : Fintype (i ⟶ j)

structure MultiplicativeBasisDeformations.Statement.IsAlmostSplitSequence (k : Type u) {A : Type u} [Field k] [Ring A] [Algebra k A] {U E V : ModuleCat Aᵐᵒᵖ} (f : U ⟶ E) (g : E ⟶ V) : Prop

An almost split sequence 0 → U → E → V → 0 of right modules: a short exact sequence whose first map is left almost split and whose second map is right almost split, among finite-dimensional modules.

• comp_eq_zero : CategoryTheory.CategoryStruct.comp f g = 0
• shortExact : { X₁ := U, X₂ := E, X₃ := V, f := f, g := g, zero := ⋯ }.ShortExact
• not_isSplitMono : ¬CategoryTheory.IsSplitMono f
• not_isSplitEpi : ¬CategoryTheory.IsSplitEpi g
• left (X : ModuleCat Aᵐᵒᵖ) : Module.Finite k ↑X → ∀ (h : U ⟶ X), ¬CategoryTheory.IsSplitMono h → ∃ (h' : E ⟶ X), CategoryTheory.CategoryStruct.comp f h' = h
• right (X : ModuleCat Aᵐᵒᵖ) : Module.Finite k ↑X → ∀ (h : X ⟶ V), ¬CategoryTheory.IsSplitEpi h → ∃ (h' : X ⟶ E), CategoryTheory.CategoryStruct.comp h' g = h

def MultiplicativeBasisDeformations.Statement.IsTranslate {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) (t i : Vertex S) : Prop

The Auslander–Reiten translate: X_t = τ X_i when there is an almost split sequence 0 → X_t → E → X_i → 0.

The mesh category k(Γ_A)

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.Statement.PathCategory {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) : Type

The k-linear path category of Γ_A: morphisms i ⟶ j are finite linear combinations of paths from i to j, composed by concatenation.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.Statement.pathObj {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) (i : Vertex S) : PathCategory S

The vertex i as an object of the path category.

noncomputable def MultiplicativeBasisDeformations.Statement.path {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) {i j : Vertex S} (p : Quiver.Path i j) : pathObj S i ⟶ pathObj S j

A path as a morphism of the path category.

noncomputable def MultiplicativeBasisDeformations.Statement.meshRelation {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) (t i : Vertex S) : pathObj S t ⟶ pathObj S i

The mesh relation ∑ (σ a) a from τ X_i = X_t to X_i: the sum of all paths t → j → i of length two.

def MultiplicativeBasisDeformations.Statement.meshRelations {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) (X Y : PathCategory S) : Set (X ⟶ Y)

The family of all mesh relations, indexed by their endpoints.

noncomputable def MultiplicativeBasisDeformations.Statement.meshIdeal {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) (X Y : PathCategory S) : Submodule k (X ⟶ Y)

The two-sided ideal of the path category linearly generated by the mesh relations.

theorem MultiplicativeBasisDeformations.Statement.meshIdeal_precomp {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) {X Y Z : PathCategory S} (f : X ⟶ Y) {g : Y ⟶ Z} (hg : g ∈ meshIdeal S Y Z) : CategoryTheory.CategoryStruct.comp f g ∈ meshIdeal S X Z

theorem MultiplicativeBasisDeformations.Statement.meshIdeal_postcomp {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) {X Y Z : PathCategory S} {f : X ⟶ Y} (g : Y ⟶ Z) (hf : f ∈ meshIdeal S X Y) : CategoryTheory.CategoryStruct.comp f g ∈ meshIdeal S X Z

def MultiplicativeBasisDeformations.Statement.meshRel {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) : HomRel (PathCategory S)

Equality modulo the mesh ideal.

instance MultiplicativeBasisDeformations.Statement.instCongruencePathCategoryMeshRel {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) : CategoryTheory.Congruence (meshRel S)

theorem MultiplicativeBasisDeformations.Statement.meshRel_add {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) {X Y : PathCategory S} (f₁ f₂ g₁ g₂ : X ⟶ Y) (hf : meshRel S f₁ f₂) (hg : meshRel S g₁ g₂) : meshRel S (f₁ + g₁) (f₂ + g₂)

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.Statement.MeshCategory {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) : Type

The mesh category k(Γ_A): the path category of Γ_A modulo the mesh relations.

@[instance_reducible]

noncomputable instance MultiplicativeBasisDeformations.Statement.instPreadditiveMeshCategory {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) : CategoryTheory.Preadditive (MeshCategory S)

instance MultiplicativeBasisDeformations.Statement.instAdditivePathCategoryQuotientMeshRelFunctor {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) : (CategoryTheory.Quotient.functor (meshRel S)).Additive

@[instance_reducible]

noncomputable instance MultiplicativeBasisDeformations.Statement.instLinearMeshCategory {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) : CategoryTheory.Linear k (MeshCategory S)

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.Statement.meshObj {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) (i : Vertex S) : MeshCategory S

The vertex i as an object of the mesh category.

def MultiplicativeBasisDeformations.Statement.IsStandardFor {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) : Prop

A is standard with respect to the family: every space of irreducible maps has dimension at most one, so that Γ_A has at most one arrow between two vertices and the mesh relations above are those of Γ_A, and there is a k-linear equivalence k(Γ_A) ≃ ind(mod A) sending each vertex to its module.

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

A is standard: it is standard with respect to every complete family of indecomposable right modules.

def MultiplicativeBasisDeformations.Statement.TheoremB (k A : Type u) [Field k] [Ring A] [Algebra k A] [IsAlgClosed k] [FiniteDimensional k A] : Prop

Theorem B, as a proposition: a basic finite-dimensional representation-finite algebra over an algebraically closed field of characteristic different from two is standard.