Finite mesh-simple presentations

The objectwise mesh calculations assemble into categorical exact sequences of contravariant mesh modules. When the mesh representables are finite- dimensional, the simple, the incoming coefficient module, and all displayed maps restrict to the existing finite-dimensional linear-module category.

The use of the opposite vertex category is deliberate: a contravariant mesh module is a covariant linear module on the opposite category, so this file reuses the package's established covariant module API rather than introducing a parallel convention.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.MeshCategory.RightMeshData.vertexCategoryFintype {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) : Fintype T.VertexCategory

@[instance_reducible]

noncomputable instance MagnitudeConjecture.MeshCategory.RightMeshData.oppositeVertexCategoryFintype {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) : Fintype T.VertexCategoryᵒᵖ

instance MagnitudeConjecture.MeshCategory.RightMeshData.simpleFunctor_additive {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (z : Q) : (T.simpleFunctor z).Additive

instance MagnitudeConjecture.MeshCategory.RightMeshData.simpleFunctor_linear {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (z : Q) : CategoryTheory.Functor.Linear k (T.simpleFunctor z)

instance MagnitudeConjecture.MeshCategory.RightMeshData.incomingCoefficientFunctor_additive {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (z : Q) : (T.incomingCoefficientFunctor z).Additive

instance MagnitudeConjecture.MeshCategory.RightMeshData.incomingCoefficientFunctor_linear {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (z : Q) : CategoryTheory.Functor.Linear k (T.incomingCoefficientFunctor z)

instance MagnitudeConjecture.MeshCategory.RightMeshData.contravariantRepresentableFunctor_linear {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (y : Q) : CategoryTheory.Functor.Linear k ((CategoryTheory.linearYoneda k T.VertexCategory).obj y)

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.incomingSummandInclusion {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (z : Q) (a : IncomingArrow z) : (CategoryTheory.linearYoneda k T.VertexCategory).obj a.fst ⟶ T.incomingCoefficientFunctor z

Insert one contravariant representable as the coefficient belonging to an incoming arrow.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.incomingSummandProjection {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (z : Q) (a : IncomingArrow z) : T.incomingCoefficientFunctor z ⟶ (CategoryTheory.linearYoneda k T.VertexCategory).obj a.fst

Project an incoming coefficient family to the contravariant representable indexed by one incoming arrow.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.incomingSummandInclusion_comp_projection_self {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (z : Q) (a : IncomingArrow z) : CategoryTheory.CategoryStruct.comp (T.incomingSummandInclusion z a) (T.incomingSummandProjection z a) = CategoryTheory.CategoryStruct.id ((CategoryTheory.linearYoneda k T.VertexCategory).obj a.fst)

theorem MagnitudeConjecture.MeshCategory.RightMeshData.incomingSummandInclusion_comp_projection_eq_zero {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (z : Q) {a b : IncomingArrow z} (h : a ≠ b) : CategoryTheory.CategoryStruct.comp (T.incomingSummandInclusion z a) (T.incomingSummandProjection z b) = 0

theorem MagnitudeConjecture.MeshCategory.RightMeshData.sum_incomingSummandProjection_comp_inclusion {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (z : Q) : ∑ a : IncomingArrow z, CategoryTheory.CategoryStruct.comp (T.incomingSummandProjection z a) (T.incomingSummandInclusion z a) = CategoryTheory.CategoryStruct.id (T.incomingCoefficientFunctor z)

Summing the coordinate projection-inclusion endomorphisms recovers an incoming coefficient family.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.incomingSummandInclusion_comp_incomingMap {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (z : Q) (a : IncomingArrow z) : CategoryTheory.CategoryStruct.comp (T.incomingSummandInclusion z a) (T.incomingMap z) = (CategoryTheory.linearYoneda k T.VertexCategory).map (CategoryTheory.InducedCategory.homMk (T.incomingArrowHom a))

Restricting the incoming-arrow map to one representable summand is the Yoneda image of that incoming arrow.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.translationMap_eq_sum_paired_incoming {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (z : { z : Q // z ∉ T.projective }) : T.translationMap z = ∑ a : IncomingArrow ↑z, CategoryTheory.CategoryStruct.comp ((CategoryTheory.linearYoneda k T.VertexCategory).map (CategoryTheory.InducedCategory.homMk (T.incomingArrowHom ⟨T.tau z, (T.arrowEquiv z a.fst) a.snd⟩))) (T.incomingSummandInclusion (↑z) a)

The translation differential is the sum of the Yoneda maps represented by the polarized partners, followed by the corresponding summand inclusions.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.contravariantRepresentableLinearModule {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (y : Q) : CoveringHom.LinearModuleCategory k

The literal contravariant mesh representable used by the mesh maps, bundled as a covariant linear module on the opposite vertex category.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.simpleLinearModule {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (z : Q) : CoveringHom.LinearModuleCategory k

The mesh simple as a covariant linear module on the opposite vertex category.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.incomingCoefficientLinearModule {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (z : Q) : CoveringHom.LinearModuleCategory k

The incoming coefficient functor as a covariant linear module on the opposite vertex category.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.simpleLinearModule_isFiniteDimensional {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (z : Q) : CoveringHom.IsFiniteDimensionalModule k (T.simpleLinearModule z)

Every mesh simple is finite-dimensional and supported only at its named vertex. This does not require finite-dimensional mesh Hom spaces.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.simpleFiniteModule {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (z : Q) : CoveringHom.FiniteDimensionalModuleCategory k

The mesh simple bundled in the finite-dimensional linear-module category.

instance MagnitudeConjecture.MeshCategory.RightMeshData.simpleFiniteModule_simple {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (z : Q) : CategoryTheory.Simple (T.simpleFiniteModule z)

The mesh simple supported at a vertex is a simple object of the finite-dimensional module category.

@[reducible, inline]

abbrev MagnitudeConjecture.MeshCategory.RightMeshData.FiniteContravariantRepresentables {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) : Prop

Finite-dimensionality of all contravariant vertex representables, expressed in the package's covariant-on-the-opposite convention.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.contravariantRepresentableValueLinearEquiv {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (X : T.VertexCategoryᵒᵖ) (y : Q) : ↑((CoveringHom.linearCoyonedaLinearModule (Opposite.op y)).obj.obj X) ≃ₗ[k] obj T (Opposite.unop X) ⟶ obj T y

Evaluation of the covariant representable on the opposite vertex category is the expected contravariant raw mesh Hom space.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.contravariantRepresentableRawIso {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (y : Q) : (CategoryTheory.linearCoyoneda k T.VertexCategoryᵒᵖ).obj (Opposite.op (Opposite.op y)) ≅ (CategoryTheory.linearYoneda k T.VertexCategory).obj y

The opposite-category covariant representable and the literal contravariant mesh representable are naturally isomorphic.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.contravariantRepresentableLinearIso {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (y : Q) : CoveringHom.linearCoyonedaLinearModule (Opposite.op y) ≅ T.contravariantRepresentableLinearModule y

Linear-module form of the identification between the package's standard opposite-category representable and the literal mesh representable.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.contravariantRepresentableLinearModule_isFiniteDimensional {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (y : Q) : CoveringHom.IsFiniteDimensionalModule k (T.contravariantRepresentableLinearModule y)

A literal contravariant mesh representable is finite-dimensional whenever the corresponding opposite-category covariant representable is.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.contravariantRepresentableFiniteModule {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (y : Q) : CoveringHom.FiniteDimensionalModuleCategory k

The literal contravariant mesh representable bundled in the finite-dimensional linear-module category.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.contravariantRepresentableFiniteIso {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (y : Q) : CoveringHom.finiteDimensionalLinearCoyoneda (Opposite.op y) ⋯ ≅ T.contravariantRepresentableFiniteModule hP y

Finite-module form of the identification with the package's standard opposite-category projective representable.

instance MagnitudeConjecture.MeshCategory.RightMeshData.contravariantRepresentableFiniteModule_projective {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (y : Q) : CategoryTheory.Projective (T.contravariantRepresentableFiniteModule hP y)

theorem MagnitudeConjecture.MeshCategory.RightMeshData.incomingCoefficientLinearModule_isFiniteDimensional {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : Q) : CoveringHom.IsFiniteDimensionalModule k (T.incomingCoefficientLinearModule z)

Under finite-dimensionality of the mesh representables, the incoming coefficient module is finite-dimensional.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.incomingCoefficientFiniteModule {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : Q) : CoveringHom.FiniteDimensionalModuleCategory k

The incoming coefficient module bundled in the finite-dimensional linear-module category.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.incomingSummandInclusionFinite {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : Q) (a : IncomingArrow z) : T.contravariantRepresentableFiniteModule hP a.fst ⟶ T.incomingCoefficientFiniteModule hP z

Finite-dimensional lift of one coordinate inclusion into the incoming coefficient module.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.incomingSummandProjectionFinite {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : Q) (a : IncomingArrow z) : T.incomingCoefficientFiniteModule hP z ⟶ T.contravariantRepresentableFiniteModule hP a.fst

Finite-dimensional lift of one coordinate projection from the incoming coefficient module.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.incomingSummandInclusionFinite_comp_projection_self {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : Q) (a : IncomingArrow z) : CategoryTheory.CategoryStruct.comp (T.incomingSummandInclusionFinite hP z a) (T.incomingSummandProjectionFinite hP z a) = CategoryTheory.CategoryStruct.id (T.contravariantRepresentableFiniteModule hP a.fst)

theorem MagnitudeConjecture.MeshCategory.RightMeshData.incomingSummandInclusionFinite_comp_projection_eq_zero {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : Q) {a b : IncomingArrow z} (h : a ≠ b) : CategoryTheory.CategoryStruct.comp (T.incomingSummandInclusionFinite hP z a) (T.incomingSummandProjectionFinite hP z b) = 0

theorem MagnitudeConjecture.MeshCategory.RightMeshData.sum_incomingSummandProjectionFinite_comp_inclusion {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : Q) : ∑ a : IncomingArrow z, CategoryTheory.CategoryStruct.comp (T.incomingSummandProjectionFinite hP z a) (T.incomingSummandInclusionFinite hP z a) = CategoryTheory.CategoryStruct.id (T.incomingCoefficientFiniteModule hP z)

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.incomingArrowEquivFin {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (z : Q) : IncomingArrow z ≃ Fin (Fintype.card (IncomingArrow z))

A fixed finite enumeration of the arrows into a vertex.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.incomingRepresentableBiproductIso {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : Q) : (⨁ fun (i : Fin (Fintype.card (IncomingArrow z))) => T.contravariantRepresentableFiniteModule hP ((incomingArrowEquivFin z).symm i).fst) ≅ T.incomingCoefficientFiniteModule hP z

The incoming coefficient module is the finite biproduct of the contravariant representables indexed by arrows into the vertex.

instance MagnitudeConjecture.MeshCategory.RightMeshData.incomingRepresentableBiproduct_projective {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : Q) : CategoryTheory.Projective (⨁ fun (i : Fin (Fintype.card (IncomingArrow z))) => T.contravariantRepresentableFiniteModule hP ((incomingArrowEquivFin z).symm i).fst)

instance MagnitudeConjecture.MeshCategory.RightMeshData.incomingCoefficientFiniteModule_projective {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : Q) : CategoryTheory.Projective (T.incomingCoefficientFiniteModule hP z)

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.simpleProjectionFinite {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : Q) : T.contravariantRepresentableFiniteModule hP z ⟶ T.simpleFiniteModule z

Finite-dimensional lift of the projection from the vertex representable to its mesh simple.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.incomingMapFinite {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : Q) : T.incomingCoefficientFiniteModule hP z ⟶ T.contravariantRepresentableFiniteModule hP z

Finite-dimensional lift of the incoming-arrow map.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.translationMapFinite {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : { z : Q // z ∉ T.projective }) : T.contravariantRepresentableFiniteModule hP (T.tau z) ⟶ T.incomingCoefficientFiniteModule hP ↑z

Finite-dimensional lift of the paired translation map.

instance MagnitudeConjecture.MeshCategory.RightMeshData.simpleProjectionFinite_epi {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : Q) : CategoryTheory.Epi (T.simpleProjectionFinite hP z)

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.simpleStandardAugmentation {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : Q) : CoveringHom.finiteDimensionalLinearCoyoneda (Opposite.op z) ⋯ ⟶ T.simpleFiniteModule z

The standard opposite-category projective representable maps onto the mesh simple through its identification with the literal mesh representable.

instance MagnitudeConjecture.MeshCategory.RightMeshData.simpleStandardAugmentation_epi {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : Q) : CategoryTheory.Epi (T.simpleStandardAugmentation hP z)

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.simpleFiniteRepresentablePresentation {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : Q) : CoveringHom.FiniteRepresentablePresentation hP (T.simpleFiniteModule z)

The canonical one-generator finite representable presentation of a mesh simple.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.simplePositiveShortComplex {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (z : Q) : CategoryTheory.ShortComplex (CategoryTheory.Functor T.VertexCategoryᵒᵖ (ModuleCat k))

The positive-tail mesh presentation in the ambient functor category.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.simpleTranslationShortComplex {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (z : { z : Q // z ∉ T.projective }) : CategoryTheory.ShortComplex (CategoryTheory.Functor T.VertexCategoryᵒᵖ (ModuleCat k))

The paired-translation part of a nonprojective mesh-simple presentation in the ambient functor category.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.simplePositiveShortComplex_exact {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (z : Q) : (T.simplePositiveShortComplex z).Exact

The positive-tail mesh presentation is categorically exact.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.simpleTranslationShortComplex_exact {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (z : { z : Q // z ∉ T.projective }) : (T.simpleTranslationShortComplex z).Exact

The paired-translation mesh presentation is categorically exact at its middle term.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.simplePositiveFiniteShortComplex {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : Q) : CategoryTheory.ShortComplex (CoveringHom.FiniteDimensionalModuleCategory k)

The positive-tail mesh presentation inside the finite-dimensional linear-module category.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.simpleTranslationFiniteShortComplex {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : { z : Q // z ∉ T.projective }) : CategoryTheory.ShortComplex (CoveringHom.FiniteDimensionalModuleCategory k)

The paired-translation part of the mesh-simple presentation inside the finite-dimensional linear-module category.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.simplePositiveFiniteShortComplex_exact {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : Q) : (T.simplePositiveFiniteShortComplex hP z).Exact

The finite-dimensional positive-tail mesh presentation is exact.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.simpleTranslationFiniteShortComplex_exact {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : { z : Q // z ∉ T.projective }) : (T.simpleTranslationFiniteShortComplex hP z).Exact

The finite-dimensional paired-translation mesh presentation is exact at its middle term.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.simpleStandardPositiveShortComplex {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : Q) : CategoryTheory.ShortComplex (CoveringHom.FiniteDimensionalModuleCategory k)

The positive-tail presentation with its projective middle term written in the package's standard opposite-category representable convention.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.simplePositiveFiniteStandardIso {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : Q) : T.simplePositiveFiniteShortComplex hP z ≅ T.simpleStandardPositiveShortComplex hP z

Replacing the literal mesh representable by the standard opposite-category representable gives an isomorphic short complex.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.simpleStandardPositiveShortComplex_exact {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : Q) : (T.simpleStandardPositiveShortComplex hP z).Exact

The standard-representable positive-tail presentation is exact.