Lemma 2.9 with the standard homological notions

The hypotheses of projectiveEvaluationCriterion are stated through what the proof uses: Ext¹-vanishing in Yoneda form (ExtVan) and gl.dim ≤ 2 as "kernels of maps between projectives are projective" (GlDimLeTwo). Here they are derived from Mathlib's notions:

• gl.dim R ≤ 2: every R-module has projective dimension at most two (GlobalDimLE2, Mathlib's HasProjectiveDimensionLE), gives GlDimLeTwo (glDimLeTwo_of_globalDim, from the two short exact sequences of a map between projectives);
• Ext¹_R(T, Q) = 0 for Mathlib's Ext (ExtOneVan) gives ExtVan (extVan_of_extOneVan, from the contravariant long exact sequence of Ext). So Lemma 2.9 holds with the hypotheses as stated (projectiveEvaluationCriterion_std), and the check on simples is van_of_simple_std.

def MultiplicativeBasisDeformations.EvalCriterion.GlobalDimLE2 (R : Type u) [Ring R] : Prop

gl.dim R ≤ 2: every R-module has projective dimension at most two.

theorem MultiplicativeBasisDeformations.EvalCriterion.glDimLeTwo_of_globalDim (k : Type u) [Field k] {R : Type u} [Ring R] [Algebra k R] (h : GlobalDimLE2 R) : GlDimLeTwo k

gl.dim R ≤ 2 gives the form used by the proof: the kernel of a map between projective modules is projective.

def MultiplicativeBasisDeformations.EvalCriterion.ExtOneVan {k : Type u} [Field k] {R : Type u} [Ring R] [Algebra k R] (ε : R) (Q : Type u) [AddCommGroup Q] [Module R Q] : Prop

Ext¹_R(T, Q) = 0 (Mathlib's Ext) for every finite-dimensional T killed by ε.

theorem MultiplicativeBasisDeformations.EvalCriterion.splitsFor_of_ext {k : Type u} [Field k] {R : Type u} [Ring R] [Algebra k R] {T Q : Type u} [AddCommGroup T] [Module R T] [AddCommGroup Q] [Module R Q] (h : ∀ (e : CategoryTheory.Abelian.Ext (ModuleCat.of R T) (ModuleCat.of R Q) 1), e = 0) : SplitsFor k R T Q

Vanishing of Ext¹ gives the Yoneda form: every extension 0 → Q → E → T → 0 splits.

theorem MultiplicativeBasisDeformations.EvalCriterion.extVan_of_extOneVan {k : Type u} [Field k] {R : Type u} [Ring R] [Algebra k R] {ε : R} {Q : Type u} [AddCommGroup Q] [Module R Q] (h : ExtOneVan ε Q) : ExtVan k ε Q

ExtOneVan gives ExtVan.

theorem MultiplicativeBasisDeformations.EvalCriterion.projectiveEvaluationCriterion_std (k : Type u) [Field k] {R : Type u} [Ring R] [Algebra k R] [FiniteDimensional k R] {ε : R} (hε : IsIdempotentElem ε) (h0 : HomVan k ε R) (h1 : ExtOneVan ε R) : (∀ (M Q : Type u) [inst : AddCommGroup M] [inst_1 : Module k M] [inst_2 : Module R M] [IsScalarTower k R M] [FiniteDimensional k M] [inst_5 : AddCommGroup Q] [inst_6 : Module k Q] [inst_7 : Module R Q] [IsScalarTower k R Q] [FiniteDimensional k Q] [Module.Projective R Q], Function.Bijective fun (f : M →ₗ[R] Q) => EPmap hε f) ∧ (GlobalDimLE2 R → InjLift k hε → (∀ (X : Type u) [inst : AddCommGroup X] [inst_1 : Module k X] [inst_2 : Module hε.Corner X] [IsScalarTower k hε.Corner X] [FiniteDimensional k X], ∃ (P : Type u) (x : AddCommGroup P) (x_1 : Module k P) (x_2 : Module R P) (_ : IsScalarTower k R P) (_ : FiniteDimensional k P) (_ : Module.Projective R P), Nonempty (EP hε P ≃ₗ[hε.Corner] X)) ∧ ∃ (n : ℕ) (L : Fin n → Submodule R R), ∀ (X : Type u) [inst : AddCommGroup X] [inst_1 : Module k X] [inst_2 : Module hε.Corner X] [IsScalarTower k hε.Corner X] [FiniteDimensional k X], MBDVendor.QSE.Foundation.IsIndecomposableModule hε.Corner X → ∃ (i : Fin n), Nonempty (EP hε ↥(L i) ≃ₗ[hε.Corner] X))

Lemma 2.9 (lem:projective-evaluation-criterion) with the standard notions: assume Hom_R(T, R) = 0 and Ext¹_R(T, R) = 0 (Mathlib's Ext) for all finite-dimensional T with εT = 0. Then (1) P ↦ εP is fully faithful on finite-dimensional projectives; (2) if moreover gl.dim R ≤ 2 (every module has projective dimension ≤ 2) and every finite-dimensional injective Λ_e-module is εQ for a finite-dimensional projective Q, it is essentially surjective onto finite-dimensional Λ_e-modules and Λ_e is representation-finite.

theorem MultiplicativeBasisDeformations.EvalCriterion.van_of_simple_std (k : Type u) [Field k] {R : Type u} [Ring R] [Algebra k R] [FiniteDimensional k R] {ε : R} (h : ∀ (S : Type u) [inst : AddCommGroup S] [inst_1 : Module k S] [inst_2 : Module R S] [IsScalarTower k R S] [FiniteDimensional k S], IsSimpleModule R S → Killed ε S → (∀ (f : S →ₗ[R] R), f = 0) ∧ ∀ (e : CategoryTheory.Abelian.Ext (ModuleCat.of R S) (ModuleCat.of R R) 1), e = 0) : HomVan k ε R ∧ ExtVan k ε R

It suffices to check the two vanishings on the simple modules killed by ε (with Mathlib's Ext¹): they give the hypotheses of projectiveEvaluationCriterion, hence its conclusions.