The polarized AR mesh underlying the standard form

The standard form in the manuscript is the category algebra of the projective full subcategory of the mesh category of the Auslander--Reiten translation quiver. This file constructs that finite polarized translation quiver from an arbitrary finite indecomposable right-module skeleton. In particular, it does not assume that the module category is directed.

An arrow x ⟶ y in the quiver below is written in the path-category orientation and therefore represents one occurrence of an irreducible module map y ⟶ x. The polarization is the translation identity for official AR arrow multiplicities.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormArrow {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) : Type

Reversed AR-quiver arrows, indexed canonically by the official middle-term multiplicity.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.natCard_standardFormArrow {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) : Nat.card (S.StandardFormArrow x y) = FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData y x

@[reducible]

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

The reversed Auslander--Reiten quiver used to form the standard mesh category.

@[reducible]

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormArrowFintype {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)

Every standard-form arrow type is finite.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveSet {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : Set (Fin S.n)

The projective vertices in the standard-form translation quiver.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.mem_standardFormProjectiveSet_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : x ∈ S.standardFormProjectiveSet ↔ CategoryTheory.Projective (S.fgObj x)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormTau {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { x : Fin S.n // x ∉ S.standardFormProjectiveSet }) : Fin S.n

Auslander--Reiten translation on a nonprojective standard-form vertex.

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

Translation and the equality of the two arrow multiplicities across an AR mesh supply a polarization of the standard-form quiver.

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormAdditiveHullQuiver {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.standardFormAdditiveHullArrowFintype {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)

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormMeshAdditiveHull {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Type 1

The finite additive hull of the raw standard-form mesh category. This is the additive category in which the manuscript's mesh sequences become weak kernel diagrams.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormAdditiveRightMesh {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // z ∉ S.standardFormProjectiveSet }) : CategoryTheory.ShortComplex S.StandardFormMeshAdditiveHull

The additive-hull mesh ending at a nonprojective standard-form vertex.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormRiedtmannConditionB {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Prop

Riedtmann condition (b) for the standard-form mesh: every nonzero morphism out of a nonprojective vertex is detected by one arrow entering that vertex.

@[reducible, inline]

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

The perfect-composition-pairing witness in Riedtmann condition (c) at a standard-form projective vertex.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormRiedtmannConditionC {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Prop

Riedtmann condition (c) for the standard-form mesh.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRiedtmannConditionB_iff_incoming_epi {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.StandardFormRiedtmannConditionB ↔ ∀ (z : { z : Fin S.n // z ∉ S.standardFormProjectiveSet }), CategoryTheory.Epi (S.standardFormRightMeshData.additiveIncomingMap ↑z)

In the standard-form additive hull, Riedtmann condition (b) is exactly epimorphy of every nonprojective incoming-arrow matrix.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormAdditiveRightMesh_isWeakKernel {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // z ∉ S.standardFormProjectiveSet }) : QuotientSubmoduleEquidistribution.Iyama.ShortComplex.IsWeakKernel (S.standardFormAdditiveRightMesh z)

The nonprojective standard-form mesh is a weak-kernel diagram in the finite additive hull. This is the categorical right-exactness input in the Auslander-category recovery; it does not assert that the translation map is monic.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormAdditiveIncomingMap_mono_of_projective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) (hz : z ∈ S.standardFormProjectiveSet) : CategoryTheory.Mono (S.standardFormRightMeshData.additiveIncomingMap z)

At a projective standard-form vertex, the incoming-arrow matrix is monic. This is the projective boundary case of the mesh-presentation argument.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormProjectiveVertex {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : Type

Labels of projective vertices in the AR translation quiver.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormMeshCategory {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Type

The whole mesh category of the finite Auslander--Reiten translation quiver underlying the standard form.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormProjectiveMeshCategory {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Type

The full subcategory of the standard mesh category on the projective vertices. Its category algebra is the manuscript's standard form once the Bretscher--Gabriel finite-dimensionality and AR-identification layer is established.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveMeshCategoryFintype {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Fintype S.StandardFormProjectiveMeshCategory

The projective full subcategory has finitely many objects.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveMeshCategoryOppositeFintype {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Fintype S.StandardFormProjectiveMeshCategoryᵒᵖ

The opposite projective mesh category is finite as well.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveMeshInclusion {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor S.StandardFormProjectiveMeshCategory S.StandardFormMeshCategory

Inclusion of the projective vertices into the whole standard-form mesh category.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveMeshInclusion_additive {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormProjectiveMeshInclusion.Additive

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveMeshInclusion_linear {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor.Linear k S.standardFormProjectiveMeshInclusion

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormMeshHomFinite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Prop

The remaining finiteness assertion in the mesh-category construction of the standard form. It is separated from the already constructed finite polarized translation quiver because finite-dimensionality of all mesh Hom spaces is the local finite-dimensionality input in the Bongartz--Gabriel Auslander-category argument.

structure MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormRiedtmannConditions {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Prop

The three source-facing inputs in the Riedtmann mesh-Auslander criterion: local finite-dimensionality, incoming detection at every nonprojective vertex, and the perfect pairings based at projective vertices.

• homFinite : S.StandardFormMeshHomFinite
• conditionB : S.StandardFormRiedtmannConditionB
• conditionC : S.StandardFormRiedtmannConditionC

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

Finite-dimensional covariant representables on the projective full mesh subcategory, obtained from finite-dimensionality of its Hom spaces and its finite object set.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormFiniteDualCorepresentables {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hfinite : S.StandardFormMeshHomFinite) (X : S.StandardFormProjectiveMeshCategory) : CoveringHom.IsFiniteDimensionalModule k (CoveringHom.dualLinearYonedaLinearModule X)

Finite-dimensional coefficient-dual corepresentables on the projective full mesh subcategory.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRestrictedYonedaFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hfinite : S.StandardFormMeshHomFinite) : CategoryTheory.Functor S.StandardFormMeshCategory (CoveringHom.FiniteDimensionalModuleCategory k)

The manuscript's restricted Yoneda realization X ↦ Hom(-, X)|_P, from the whole mesh category to finite-dimensional contravariant modules on its projective full subcategory.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRestrictedYonedaFunctor_faithful_of_conditions {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (H : S.StandardFormRiedtmannConditions) : (S.standardFormRestrictedYonedaFunctor ⋯).Faithful

The projective vertices detect every morphism by Riedtmann condition (b), so the standard-form restricted Yoneda realization is faithful.

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

Covariant representables on the opposite projective mesh category are the contravariant projective modules used by mod P in the manuscript.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveMeshCategoryEndLocal {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hfinite : S.StandardFormMeshHomFinite) (X : S.StandardFormProjectiveMeshCategory) : IsLocalRing (CategoryTheory.End X)

Finite-dimensional mesh Hom spaces make every projective standard-form vertex have a local endomorphism ring. This is the local-boundedness part of the Bongartz--Gabriel mesh-Auslander layer.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveMeshCategorySkeletal {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Skeletal S.StandardFormProjectiveMeshCategory

The projective full mesh subcategory is skeletal: the path-length grading prevents distinct mesh vertices from becoming isomorphic.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveMeshCategoryOppositeSkeletal {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Skeletal S.StandardFormProjectiveMeshCategoryᵒᵖ

The opposite projective mesh category is skeletal as well.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveMeshCategoryIsLocallyBounded {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hfinite : S.StandardFormMeshHomFinite) : CoveringHom.IsLocallyBounded

Once its mesh Hom spaces are finite-dimensional, the projective full subcategory satisfies the complete locally bounded package used by the covering formalization.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormAlgebra {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hfinite : S.StandardFormMeshHomFinite) : Type u

The category algebra of the projective full subcategory of the AR mesh category. The opposite is deliberate: covariant modules on Pᵒᵖ are the contravariant modules mod P used by the manuscript, so the right-module category-algebra bridge is applied at Pᵒᵖ.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormAlgebra_finiteDimensional {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hfinite : S.StandardFormMeshHomFinite) : FiniteDimensional k (S.standardFormAlgebra hfinite)

The standard-form category algebra is finite-dimensional.