Minimal injective resolutions over the standard mesh category

Every finite contravariant module over the standard mesh category has a two-step minimal injective presentation. In particular, each contravariant representable has a chosen exact complex Pₓ ⟶ I₀ ⟶ I₁ whose two injective maps are essential. These are the objects whose indecomposable summands are identified by the Bongartz--Gabriel socle and degree-one Ext arguments.

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormInjectiveResolutionQuiver {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Quiver (Fin S.n)

@[instance_reducible]

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormInjectiveResolutionArrowFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : Fin S.n) : Fintype (x ⟶ y)

@[instance_reducible]

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormInjectiveResolutionDoubleOppositeFintype {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Fintype S.standardFormRightMeshData.VertexCategoryᵒᵖᵒᵖ

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormFiniteDoubleOppositeRepresentables {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : S.standardFormRightMeshData.VertexCategoryᵒᵖᵒᵖ) : CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule X)

Representables on the opposite of the opposite vertex category are finite-dimensional. This is the hypothesis needed to construct injective envelopes in the category of contravariant standard-mesh modules.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormFiniteContravariantModule_twoStepMinimalInjectivePresentation_nonempty {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (M : CoveringHom.FiniteDimensionalModuleCategory k) : Nonempty (TwoStepMinimalInjectivePresentation M)

Every finite contravariant standard-mesh module admits a two-step minimal injective presentation.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormContravariantRepresentableMinimalInjectivePresentation {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : TwoStepMinimalInjectivePresentation (S.standardFormRightMeshData.contravariantRepresentableFiniteModule ⋯ x)

A chosen minimal two-step injective presentation of the contravariant representable at a standard-mesh vertex.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormContravariantRepresentableInjectiveTermZero {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : CoveringHom.FiniteDimensionalModuleCategory k

The degree-zero injective term in the chosen minimal presentation.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormContravariantRepresentableInjectiveTermOne {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : CoveringHom.FiniteDimensionalModuleCategory k

The degree-one injective term in the chosen minimal presentation.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormContravariantRepresentableInjectiveTermZero_injective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : CategoryTheory.Injective (S.standardFormContravariantRepresentableInjectiveTermZero x)

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormContravariantRepresentableInjectiveTermOne_injective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : CategoryTheory.Injective (S.standardFormContravariantRepresentableInjectiveTermOne x)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormContravariantRepresentableInjectiveTermZero_essential {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : IsEssentialMono (S.standardFormContravariantRepresentableMinimalInjectivePresentation x).augmentation.f

The chosen representable-to-injective map is an essential monomorphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormContravariantRepresentableInjectiveTermOne_essential {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : IsEssentialMono (S.standardFormContravariantRepresentableMinimalInjectivePresentation x).cosyzygyPresentation.f

The chosen first-cosyzygy-to-injective map is an essential monomorphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormContravariantRepresentableMinimalInjectivePresentation_exact {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : (S.standardFormContravariantRepresentableMinimalInjectivePresentation x).presentationComplex.Exact

The chosen complex Pₓ ⟶ I₀ ⟶ I₁ is exact.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardForm_mem_projective_of_nonzero_map_simple_to_contravariantRepresentable {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {z y : Fin S.n} (f : S.standardFormRightMeshData.simpleFiniteModule z ⟶ S.standardFormRightMeshData.contravariantRepresentableFiniteModule ⋯ y) (hf : f ≠ 0) : z ∈ S.standardFormProjectiveSet

A nonzero map from a mesh simple into a standard contravariant representable can only start at a projective vertex.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormContravariantRepresentableInjectiveTermZero_projective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : CategoryTheory.Projective (S.standardFormContravariantRepresentableInjectiveTermZero x)

The degree-zero injective term in the minimal injective presentation of a contravariant representable is projective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormContravariantRepresentableInjectiveTermOne_projective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : CategoryTheory.Projective (S.standardFormContravariantRepresentableInjectiveTermOne x)

The degree-one injective term in the minimal injective presentation of a contravariant representable is projective.