Projective--injective coordinates in the standard mesh category

In the contravariant standard-mesh module category used by the Bongartz--Gabriel recovery argument, Riedtmann condition (c) identifies the injective D Hom(p,-) at a projective vertex with a contravariant representable. Hence this injective coordinate is projective. Its canonical simple socle is an essential submodule.

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRiedtmannDualityQuiver {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.standardFormRiedtmannDualityArrowFintype {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)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormVertexMeshHomFinite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : Fin S.n) : FiniteDimensional k (MeshCategory.obj S.standardFormRightMeshData x ⟶ MeshCategory.obj S.standardFormRightMeshData y)

The raw standard-mesh Hom spaces between vertices are finite-dimensional.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormFiniteContravariantDualCorepresentables {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.dualLinearYonedaLinearModule X)

All dual corepresentables in the contravariant standard-mesh module category are finite-dimensional.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormOppositeVertex {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.standardFormRightMeshData.VertexCategoryᵒᵖ

A standard-form vertex regarded as an object of the opposite strict vertex category.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormContravariantDualSocle {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 canonical simple socle of D Hom(x,-) in the contravariant standard-mesh module category.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormContravariantDualSocleInclusion {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.standardFormContravariantDualSocle x ⟶ CoveringHom.finiteDimensionalDualLinearYoneda (S.standardFormOppositeVertex x) ⋯

The canonical socle inclusion into D Hom(x,-).

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormContravariantDualSocle_simple {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.Simple (S.standardFormContravariantDualSocle x)

The canonical contravariant standard-mesh socle coordinate is simple.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormContravariantDualSocleInclusion_ne_zero {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.standardFormContravariantDualSocleInclusion x ≠ 0

The canonical contravariant standard-mesh socle inclusion is nonzero.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormContravariantDualSocleIsoSimple {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.standardFormContravariantDualSocle x ≅ S.standardFormRightMeshData.simpleFiniteModule x

The canonical socle of D Hom(x,-) is the mesh simple supported at x.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormContravariantDualSocleInclusion_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.standardFormContravariantDualSocleInclusion x)

The canonical simple socle is essential in its indecomposable injective dual corepresentable.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveDualityData {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.StandardFormProjectiveVertex) : S.StandardFormRiedtmannProjectiveDualityData ↑p

The canonical condition-(c) datum chosen at a projective standard-form vertex.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveContravariantDualityFiniteModuleIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.StandardFormProjectiveVertex) : CoveringHom.finiteDimensionalDualLinearYoneda (S.standardFormOppositeVertex ↑p) ⋯ ≅ S.standardFormRightMeshData.contravariantRepresentableFiniteModule ⋯ (S.standardFormProjectiveDualityData p).dualVertex

Condition (c), in the orientation used by the recovery proof, identifies D Hom(p,-) with the contravariant representable at the paired vertex.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveContravariantDualLinearYoneda_projective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.StandardFormProjectiveVertex) : CategoryTheory.Projective (CoveringHom.finiteDimensionalDualLinearYoneda (S.standardFormOppositeVertex ↑p) ⋯)

The injective D Hom(p,-) based at a projective standard-form vertex is projective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormFiniteContravariantInjective_projective_of_conditionC_coordinates {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) [CategoryTheory.Injective M] (hcoordinates : ∀ (N : CoveringHom.FiniteDimensionalModuleCategory k), CategoryTheory.Indecomposable N → CategoryTheory.Injective N → ∀ (i : N ⟶ M) (r : M ⟶ N), CategoryTheory.CategoryStruct.comp i r = CategoryTheory.CategoryStruct.id N → ∃ (p : S.StandardFormProjectiveVertex), Nonempty (CoveringHom.finiteDimensionalDualLinearYoneda (S.standardFormOppositeVertex ↑p) ⋯ ≅ N)) : CategoryTheory.Projective M

A finite injective contravariant standard-mesh module is projective once each indecomposable retract is identified with D Hom(p,-) for a projective vertex p.