Global dimension at most two (proof of Proposition 2.10)

graded-category.tex: "At a nonprojective label X, the exact right mesh … give 0 → R_{τX} → ⊕_{Y→X} R_Y → R_X → L_X → 0. At a projective label P, the same lemma gives a resolution 0 → R_{rad P} → R_P → L_P → 0 of length at most one. Hence gl.dim Λ ≤ 2." The proof of Lemma 2.9 uses this in the form "its kernel is a second syzygy and hence projective".

We derive this consequence: every finite-dimensional module has a projective resolution of length two by modules R_Z (the simple resolutions and the horseshoe construction, along a composition series); by Schanuel's lemma every second syzygy is projective; a finite-dimensional projective module is some R_W (tops and Nakayama's lemma).

def MultiplicativeBasisDeformations.CatAlg.colAlgL {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (x : ι) : Rep F (F x) →ₗ[Alg F] Alg F

r ↦ (column algebra element), a section of a ↦ a 1_x.

instance MultiplicativeBasisDeformations.CatAlg.projective_rep {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (x : ι) : Module.Projective (Alg F) (Rep F (F x))

R_x is projective: a retract of Λ.

instance MultiplicativeBasisDeformations.CatAlg.projective_pi {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {κ : Type} [Fintype κ] [DecidableEq κ] (Z : κ → ι) : Module.Projective (Alg F) ((j : κ) → Rep F (F (Z j)))

noncomputable def MultiplicativeBasisDeformations.CatAlg.splitEquiv {R : Type u_1} [Ring R] {P : Type u_3} [AddCommGroup P] [Module R P] {X : Type u_5} [AddCommGroup X] [Module R X] [Module.Projective R P] (π : X →ₗ[R] P) (hπ : Function.Surjective ⇑π) : X ≃ₗ[R] ↥π.ker × P

A surjection onto a projective module splits: X ≅ ker π × P.

theorem MultiplicativeBasisDeformations.CatAlg.schanuel {R : Type u_1} [Ring R] {M : Type u_2} {P : Type u_3} {P' : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] [AddCommGroup P'] [Module R P'] [Module.Projective R P] [Module.Projective R P'] (e : P →ₗ[R] M) (e' : P' →ₗ[R] M) (he : Function.Surjective ⇑e) (he' : Function.Surjective ⇑e') : Nonempty ((↥e.ker × P') ≃ₗ[R] ↥e'.ker × P)

Schanuel's lemma: for surjections e : P → M, e' : P' → M from projective modules, ker e × P' ≅ ker e' × P.

theorem MultiplicativeBasisDeformations.CatAlg.horseshoe_step {R : Type u_1} [Ring R] {P : Type u_3} {P' : Type u_4} [AddCommGroup P] [Module R P] [AddCommGroup P'] [Module R P'] {A' : Type u_5} {A : Type u_6} {A'' : Type u_7} [AddCommGroup A'] [Module R A'] [AddCommGroup A] [Module R A] [AddCommGroup A''] [Module R A''] [Module.Projective R P'] (i : A' →ₗ[R] A) (p : A →ₗ[R] A'') (hi : Function.Injective ⇑i) (hp : Function.Surjective ⇑p) (hex : p.ker = i.range) (e' : P →ₗ[R] A') (e'' : P' →ₗ[R] A'') (he' : Function.Surjective ⇑e') (he'' : Function.Surjective ⇑e'') : ∃ (e : P × P' →ₗ[R] A), Function.Surjective ⇑e ∧ ∃ (j : ↥e'.ker →ₗ[R] ↥e.ker) (q : ↥e.ker →ₗ[R] ↥e''.ker), Function.Injective ⇑j ∧ Function.Surjective ⇑q ∧ q.ker = j.range

One horseshoe step. Let 0 → A' → A → A'' → 0 be exact (i injective, p surjective, ker p = range i) and let e' : P' → A', e'' : P'' → A'' be surjections with P'' projective. Then e : P' × P'' → A, (a, b) ↦ i (e' a) + λ b with p λ = e'', is surjective, and its kernel is an extension of ker e'' by ker e'.

theorem MultiplicativeBasisDeformations.CatAlg.projective_of_ses {R : Type u_1} [Ring R] {A' : Type u_2} {A : Type u_3} {A'' : Type u_4} [AddCommGroup A'] [Module R A'] [AddCommGroup A] [Module R A] [AddCommGroup A''] [Module R A''] [Module.Projective R A'] [Module.Projective R A''] (i : A' →ₗ[R] A) (p : A →ₗ[R] A'') (hi : Function.Injective ⇑i) (hp : Function.Surjective ⇑p) (hex : p.ker = i.range) : Module.Projective R A

An extension of a projective module by a projective module is projective.

def MultiplicativeBasisDeformations.CatAlg.ExRes (R : Type w) [Ring R] (M : Type w) [AddCommGroup M] [Module R M] : Prop

A resolution of length two: P₁ → P₀ → M → 0 with projective P₀, P₁ and projective kernel of P₁ → ker (P₀ → M).

theorem MultiplicativeBasisDeformations.CatAlg.ExRes.of_equiv {R : Type w} [Ring R] {M N : Type w} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) (h : ExRes R M) : ExRes R N

theorem MultiplicativeBasisDeformations.CatAlg.ExRes.extension {R : Type w} [Ring R] {M' M M'' : Type w} [AddCommGroup M'] [Module R M'] [AddCommGroup M] [Module R M] [AddCommGroup M''] [Module R M''] (i : M' →ₗ[R] M) (p : M →ₗ[R] M'') (hi : Function.Injective ⇑i) (hp : Function.Surjective ⇑p) (hex : p.ker = i.range) (h' : ExRes R M') (h'' : ExRes R M'') : ExRes R M

Horseshoe: resolutions of length two pass to extensions.

theorem MultiplicativeBasisDeformations.CatAlg.projective_of_subsingleton {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] [Subsingleton M] : Module.Projective R M

theorem MultiplicativeBasisDeformations.CatAlg.ExRes.of_subsingleton {R : Type w} [Ring R] {M : Type w} [AddCommGroup M] [Module R M] [Subsingleton M] : ExRes R M

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.exRes_top {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) (x : ι) : ExRes (Alg F) (L.Top x)

The simple tops have resolutions of length two (the exact right meshes).

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.exRes_of_finiteDimensional {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)] (M : Type w) [AddCommGroup M] [Module k M] [Module (Alg F) M] [IsScalarTower k (Alg F) M] [FiniteDimensional k M] : ExRes (Alg F) M

Every finite-dimensional module has a resolution of length two.

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.syzygy_projective {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)] (M : Type w) [AddCommGroup M] [Module k M] [Module (Alg F) M] [IsScalarTower k (Alg F) M] [FiniteDimensional k M] {P₀ P₁ : Type w} [AddCommGroup P₀] [Module (Alg F) P₀] [Module.Projective (Alg F) P₀] [AddCommGroup P₁] [Module (Alg F) P₁] [Module.Projective (Alg F) P₁] (e₀ : P₀ →ₗ[Alg F] M) (he₀ : Function.Surjective ⇑e₀) (e₁ : P₁ →ₗ[Alg F] ↥e₀.ker) (he₁ : Function.Surjective ⇑e₁) : Module.Projective (Alg F) ↥e₁.ker

Second syzygies are projective (gl.dim Λ ≤ 2).

theorem MultiplicativeBasisDeformations.CatAlg.LocalFamily.bijective_of_top {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (L : LocalFamily F) [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] {x : ι} (ψ : Rep F (F x) →ₗ[Alg F] Rep F (F x)) (hψ : (L.radRep x).mkQ ∘ₗ ψ = (L.radRep x).mkQ) : Function.Bijective ⇑ψ

An endomorphism of R_x inducing the identity on the top is invertible.

def MultiplicativeBasisDeformations.CatAlg.LocalFamily.splitEquivOf {R : Type u_1} [Ring R] {P : Type u_2} {Q : Type u_3} [AddCommGroup P] [Module R P] [AddCommGroup Q] [Module R Q] (r : P →ₗ[R] Q) (h : Q →ₗ[R] P) (hrh : ∀ (q : Q), r (h q) = q) : P ≃ₗ[R] ↥r.ker × Q

A split surjection: P ≅ ker r × Q for r ∘ h = id.

theorem MultiplicativeBasisDeformations.CatAlg.LocalFamily.exists_equiv_RZ {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (L : LocalFamily F) [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] (P : Type w) [AddCommGroup P] [Module k P] [Module (Alg F) P] [IsScalarTower k (Alg F) P] [FiniteDimensional k P] [Module.Projective (Alg F) P] : ∃ (κ : Type) (x : Fintype κ) (x : DecidableEq κ) (W : κ → ι), Nonempty (P ≃ₗ[Alg F] (j : κ) → Rep F (F (W j)))

A finite-dimensional projective module is R_W for a family W.

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.ker_bigMap_equiv {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)] {κ κ' : Type} [Fintype κ] [DecidableEq κ] [Fintype κ'] [DecidableEq κ'] {Z : κ → ι} {Z' : κ' → ι} (f : Mat F Z Z') : ∃ (μ : Type) (x : Fintype μ) (x : DecidableEq μ) (W : μ → ι), Nonempty (↥(bigMap f).ker ≃ₗ[Alg F] RZ F W)

Kernels of maps between families are families (gl.dim Λ ≤ 2).