Exactness of almost split sequences on radical layers

Proposition 2.6(1)(2) (prop:graded-realization, graded-category.tex), in filtered form, at the canonical right mesh of a vertex x of Γ_A: the minimal right almost split map E_x → x (with E_x decomposed into chosen indecomposables, and rad P → P at a projective vertex) and its kernel τx (zero at a projective vertex). For a family w_i : W → E_i of maps into the summands:

• (lowest degree) ∑ w_i β_i ∈ J² implies every w_i ∈ J;
• (exactness at the middle) if every w_i ∈ J^{n+1} and ∑ w_i β_i ∈ J^{n+3}, then w_i ≡ z α_i modulo J^{n+2} for one z ∈ J^n(W, τx);
• (injectivity) if every z α_i ∈ J^{n+2}, then z ∈ J^{n+1}.

Here α_i : τx → E_i and β_i : E_i → x are the components of the two maps. At a projective vertex the left term is zero, which gives Proposition 2.6(2). The statements are proved in mod A, from Lemma 2.5, and hold for every finitely generated W.

def MultiplicativeBasisDeformations.StrictLayers.approxOfRightTau {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {Y : C} (M : CategoryTheory.ShortComplex C) (hM : MBDVendor.QSE.Iyama.RightTauSequence M) (hmono : CategoryTheory.Mono M.f) (e : M.X₃ ≅ Y) : RightRadicalApprox Y

A right tau-sequence with monic first map is a right radical approximation of its right term.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.IndSkeleton.tau {k A : Type w} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) : MBDVendor.QSE.Iyama.FiniteTauCategoryData (MBDVendor.Magnitude.RightModule.FinitelyGeneratedCategory A) (Fin S.toVendor.n)

The vendored tau-category data of mod A.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.IndSkeleton.rightMesh {k A : Type w} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (x : Fin S.n) : CategoryTheory.ShortComplex (ModCat A)

The canonical right mesh ending at the vertex x.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.IndSkeleton.arity {k A : Type w} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (x : Fin S.n) : ℕ

The number of summands of the middle term of the right mesh at x.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.IndSkeleton.midLabel {k A : Type w} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (x : Fin S.n) (i : Fin (S.arity x)) : Fin S.n

The label of a summand of the middle term.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.IndSkeleton.midInc {k A : Type w} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (x : Fin S.n) (i : Fin (S.arity x)) : S.fg (S.midLabel x i) ⟶ (S.rightMesh x).X₂

Inclusion of a summand into the middle term.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.IndSkeleton.midProj {k A : Type w} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (x : Fin S.n) (i : Fin (S.arity x)) : (S.rightMesh x).X₂ ⟶ S.fg (S.midLabel x i)

Projection from the middle term onto a summand.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.IndSkeleton.beta {k A : Type w} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (x : Fin S.n) (i : Fin (S.arity x)) : S.fg (S.midLabel x i) ⟶ S.fg x

The component β_i : E_i → x of the right almost split map.

theorem MultiplicativeBasisDeformations.IndSkeleton.midInc_midProj_self {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (x : Fin S.n) (i : Fin (S.arity x)) : CategoryTheory.CategoryStruct.comp (S.midInc x i) (S.midProj x i) = CategoryTheory.CategoryStruct.id (S.fg (S.midLabel x i))

theorem MultiplicativeBasisDeformations.IndSkeleton.midInc_midProj_ne {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (x : Fin S.n) {i j : Fin (S.arity x)} (h : i ≠ j) : CategoryTheory.CategoryStruct.comp (S.midInc x i) (S.midProj x j) = 0

theorem MultiplicativeBasisDeformations.IndSkeleton.sum_midProj_midInc {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (x : Fin S.n) : ∑ i : Fin (S.arity x), CategoryTheory.CategoryStruct.comp (S.midProj x i) (S.midInc x i) = CategoryTheory.CategoryStruct.id (S.rightMesh x).X₂

theorem MultiplicativeBasisDeformations.IndSkeleton.rightMesh_f_mono {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (x : Fin S.n) : CategoryTheory.Mono (S.rightMesh x).f

The first map of the right mesh is monic.

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.vertexApprox {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (x : Fin S.n) : StrictLayers.RightRadicalApprox (S.fg x)

The right radical approximation of the vertex x, from its canonical right mesh.

theorem MultiplicativeBasisDeformations.IndSkeleton.vertexApprox_p {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (x : Fin S.n) : (S.vertexApprox x).p = CategoryTheory.CategoryStruct.comp (S.rightMesh x).g (S.tau.rightTermIso (S.tau.obj x)).hom

theorem MultiplicativeBasisDeformations.IndSkeleton.beta_eq {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (x : Fin S.n) (i : Fin (S.arity x)) : S.beta x i = CategoryTheory.CategoryStruct.comp (S.midInc x i) (S.vertexApprox x).p

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.midLift {k A : Type w} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) {W : ModCat A} (x : Fin S.n) (w : (i : Fin (S.arity x)) → W ⟶ S.fg (S.midLabel x i)) : W ⟶ (S.rightMesh x).X₂

The map into the middle term with components w_i.

theorem MultiplicativeBasisDeformations.IndSkeleton.midLift_midProj {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) {W : ModCat A} (x : Fin S.n) (w : (i : Fin (S.arity x)) → W ⟶ S.fg (S.midLabel x i)) (j : Fin (S.arity x)) : CategoryTheory.CategoryStruct.comp (S.midLift x w) (S.midProj x j) = w j

theorem MultiplicativeBasisDeformations.IndSkeleton.midLift_p {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) {W : ModCat A} (x : Fin S.n) (w : (i : Fin (S.arity x)) → W ⟶ S.fg (S.midLabel x i)) : CategoryTheory.CategoryStruct.comp (S.midLift x w) (S.vertexApprox x).p = ∑ i : Fin (S.arity x), CategoryTheory.CategoryStruct.comp (w i) (S.beta x i)

theorem MultiplicativeBasisDeformations.IndSkeleton.midLift_mem {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) {W : ModCat A} (x : Fin S.n) (w : (i : Fin (S.arity x)) → W ⟶ S.fg (S.midLabel x i)) {n : ℕ} (hw : ∀ (i : Fin (S.arity x)), w i ∈ (StrictLayers.Ipow n).hom W (S.fg (S.midLabel x i))) : S.midLift x w ∈ (StrictLayers.Ipow n).hom W (S.rightMesh x).X₂

theorem MultiplicativeBasisDeformations.IndSkeleton.layer_exact_zero {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) {W : ModCat A} (x : Fin S.n) (w : (i : Fin (S.arity x)) → W ⟶ S.fg (S.midLabel x i)) (hsum : ∑ i : Fin (S.arity x), CategoryTheory.CategoryStruct.comp (w i) (S.beta x i) ∈ (StrictLayers.Ipow 2).hom W (S.fg x)) (i : Fin (S.arity x)) : w i ∈ (StrictLayers.Ipow 1).hom W (S.fg (S.midLabel x i))

Proposition 2.6(1)(2), lowest degree: ∑ w_i β_i ∈ J² implies w_i ∈ J for every summand.

theorem MultiplicativeBasisDeformations.IndSkeleton.layer_exact {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) {W : ModCat A} (x : Fin S.n) (w : (i : Fin (S.arity x)) → W ⟶ S.fg (S.midLabel x i)) {n : ℕ} (hw : ∀ (i : Fin (S.arity x)), w i ∈ (StrictLayers.Ipow (n + 1)).hom W (S.fg (S.midLabel x i))) (hsum : ∑ i : Fin (S.arity x), CategoryTheory.CategoryStruct.comp (w i) (S.beta x i) ∈ (StrictLayers.Ipow (n + 3)).hom W (S.fg x)) : ∃ z ∈ (StrictLayers.Ipow n).hom W (S.rightMesh x).X₁, ∀ (i : Fin (S.arity x)), w i - CategoryTheory.CategoryStruct.comp z (CategoryTheory.CategoryStruct.comp (S.rightMesh x).f (S.midProj x i)) ∈ (StrictLayers.Ipow (n + 2)).hom W (S.fg (S.midLabel x i))

Proposition 2.6(1)(2), exactness at the middle term: if every w_i ∈ J^{n+1} and ∑ w_i β_i ∈ J^{n+3}, then there is z ∈ J^n(W, τx) with w_i - z α_i ∈ J^{n+2} for every summand. Here α_i = f ≫ π_i are the components of the first map f of the mesh.

theorem MultiplicativeBasisDeformations.IndSkeleton.layer_injective {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) {W : ModCat A} (x : Fin S.n) {n : ℕ} (z : W ⟶ (S.rightMesh x).X₁) (hz : ∀ (i : Fin (S.arity x)), CategoryTheory.CategoryStruct.comp z (CategoryTheory.CategoryStruct.comp (S.rightMesh x).f (S.midProj x i)) ∈ (StrictLayers.Ipow (n + 2)).hom W (S.fg (S.midLabel x i))) : z ∈ (StrictLayers.Ipow (n + 1)).hom W (S.rightMesh x).X₁

Proposition 2.6(1), injectivity of the first map on layers.