Recursive construction of the standard mesh realization

The vertices are processed in an increasing enumeration of the chosen directed order. At one target, the incoming occurrence representatives are replaced by the components of a right almost-split sink. The nonprojective sink is first normalized so that its paired source composite vanishes; the projective sink is the transported radical inclusion.

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instQuiverFinN_2 {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.instFintypeHomFinN_2 {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i j : Fin S.n) : Fintype (i ⟶ j)

@[instance_reducible]

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshArrowFintype' {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i j : Fin S.n) : Fintype (S.MeshArrow i j)

structure MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.DirectedVertex {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) : Type

A wrapper carrying the selected directed order without replacing the ordinary numerical order on Fin S.n.

• val : Fin S.n

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.directedVertexUnderlyingEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) : S.DirectedVertex H ≃ Fin S.n

Forget the directed-order wrapper.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.directedVertexFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) : Fintype (S.DirectedVertex H)

@[instance_reducible]

noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.directedVertexLinearOrder {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) : LinearOrder (S.DirectedVertex H)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.directedVertexOrderIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) : Fin S.n ≃o S.DirectedVertex H

The order isomorphism enumerating the wrapped directed vertices.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.directedVertexEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) : Fin S.n ≃ Fin S.n

An increasing enumeration of the selected directed linear order, kept as an equivalence so its type does not export a competing order instance.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.directedVertexIndex {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) (z : Fin S.n) : Fin S.n

The position of a vertex in the selected directed enumeration.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.directedVertexIndex_equiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) (p : Fin S.n) : S.directedVertexIndex H ((S.directedVertexEquiv H) p) = p

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.directedVertexEquiv_index {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) (z : Fin S.n) : (S.directedVertexEquiv H) (S.directedVertexIndex H z) = z

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.directedVertexEquiv_lt_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) (p q : Fin S.n) : (S.directedVertexEquiv H) p < (S.directedVertexEquiv H) q ↔ p < q

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.directedVertexIndex_lt_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) (y z : Fin S.n) : S.directedVertexIndex H y < S.directedVertexIndex H z ↔ y < z

@[reducible, inline]

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

A choice of module morphism for every concrete reversed mesh arrow.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.FreePathFullAt {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (arrowMap : S.MeshArrowAssignment) (z : Fin S.n) : Prop

Free-path fullness at one target vertex.

structure MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.MeshStepData {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (arrowMap : S.MeshArrowAssignment) (z : Fin S.n) : Type u

All local data produced while processing one target.

• sink : (S.meshRightAlmostSplitAt z).middle ⟶ S.almostSplitSkeleton.obj z
• rightAlmostSplit : QuotientSubmoduleEquidistribution.IsRightAlmostSplit self.sink
• projective_kernel_zero : CategoryTheory.Projective (S.fgObj z) → ∀ {X : FGModuleCat Aᵐᵒᵖ} (q : X ⟶ (S.meshRightAlmostSplitAt z).middle), CategoryTheory.CategoryStruct.comp q self.sink = 0 → q = 0
• nonprojective_kernel_factor (hz : ¬CategoryTheory.Projective (S.fgObj z)) {X : FGModuleCat Aᵐᵒᵖ} (q : X ⟶ (S.meshRightAlmostSplitAt z).middle) : CategoryTheory.CategoryStruct.comp q self.sink = 0 → ∃ (t : X ⟶ S.fgObj (S.rightTranslationLabel ⟨z, hz⟩)), CategoryTheory.CategoryStruct.comp t (S.rightMeshSourceMap H (fun {i j : Fin S.n} => S.replaceArrowMapAt (fun {i j : Fin S.n} => arrowMap) z self.sink) ⟨z, hz⟩) = q
• meshRelation_zero (hz : ¬CategoryTheory.Projective (S.fgObj z)) : (LinearPathCategory.lift S.almostSplitSkeleton.obj fun {i j : Fin S.n} => S.replaceArrowMapAt (fun {i j : Fin S.n} => arrowMap) z self.sink).map ((S.rightMeshData H).meshRelation (S.rightMeshNonprojectiveVertex H ⟨z, hz⟩)) = 0

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_meshStepData {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (arrowMap : S.MeshArrowAssignment) (z : Fin S.n) (hfull : ∀ y < z, S.FreePathFullAt (fun {i j : Fin S.n} => arrowMap) y) : Nonempty (S.MeshStepData H (fun {i j : Fin S.n} => arrowMap) z)

The projective radical boundary or the normalized nonprojective AR sink supplies all data needed at one recursive step.

structure MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshStage {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (m : ℕ) : Type u

A global arrow assignment together with all properties established on the first m vertices of the directed enumeration.

• arrowMap : S.MeshArrowAssignment
• full (z : Fin S.n) : ↑(S.directedVertexIndex H z) < m → S.FreePathFullAt (fun {i j : Fin S.n} => self.arrowMap) z
• sink_rightAlmostSplit (z : Fin S.n) : ↑(S.directedVertexIndex H z) < m → QuotientSubmoduleEquidistribution.IsRightAlmostSplit (S.realizedRightMeshSink (fun {i j : Fin S.n} => self.arrowMap) z)
• projective_kernel_zero (z : Fin S.n) : CategoryTheory.Projective (S.fgObj z) → ↑(S.directedVertexIndex H z) < m → ∀ {X : FGModuleCat Aᵐᵒᵖ} (q : X ⟶ (S.meshRightAlmostSplitAt z).middle), CategoryTheory.CategoryStruct.comp q (S.realizedRightMeshSink (fun {i j : Fin S.n} => self.arrowMap) z) = 0 → q = 0
• nonprojective_kernel_factor (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : ↑(S.directedVertexIndex H ↑z) < m → ∀ {X : FGModuleCat Aᵐᵒᵖ} (q : X ⟶ (S.meshRightAlmostSplitAt ↑z).middle), CategoryTheory.CategoryStruct.comp q (S.realizedRightMeshSink (fun {i j : Fin S.n} => self.arrowMap) ↑z) = 0 → ∃ (t : X ⟶ S.fgObj (S.rightTranslationLabel z)), CategoryTheory.CategoryStruct.comp t (S.rightMeshSourceMap H (fun {i j : Fin S.n} => self.arrowMap) z) = q
• meshRelation_zero (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : ↑(S.directedVertexIndex H ↑z) < m → (LinearPathCategory.lift S.almostSplitSkeleton.obj fun {i j : Fin S.n} => self.arrowMap).map ((S.rightMeshData H).meshRelation (S.rightMeshNonprojectiveVertex H z)) = 0

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardMeshStageZero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) : S.StandardMeshStage H 0

Before the recursion starts, the properties on the empty prefix hold vacuously.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshStage.exists_succ {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) {m : ℕ} (D : S.StandardMeshStage H m) (hm : m < S.n) : Nonempty (S.StandardMeshStage H (m + 1))

Extend a completed prefix by one vertex. All earlier properties survive because only arrows ending at the new, strictly later target are changed.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_standardMeshStage {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (m : ℕ) (hm : m ≤ S.n) : Nonempty (S.StandardMeshStage H m)

The recursive construction reaches every prefix of the directed enumeration.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardMeshFinalStage {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) : S.StandardMeshStage H S.n

The completed recursive stage.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardMeshArrowMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) : S.MeshArrowAssignment

The globally normalized arrow assignment obtained after processing every vertex in the directed order.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardMeshFinalStage_index_lt {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (z : Fin S.n) : ↑(S.directedVertexIndex H z) < S.n

Every target has been processed in the final stage.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardMeshArrowMap_full {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (z : Fin S.n) : S.FreePathFullAt (fun {i j : Fin S.n} => S.standardMeshArrowMap H) z

The completed arrow assignment is full already on the free linear path category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardMeshArrowMap_sink_rightAlmostSplit {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (z : Fin S.n) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (S.realizedRightMeshSink (fun {i j : Fin S.n} => S.standardMeshArrowMap H) z)

The completed sinks are right almost split.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardMeshArrowMap_projective_kernel_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (z : Fin S.n) (hz : CategoryTheory.Projective (S.fgObj z)) {X : FGModuleCat Aᵐᵒᵖ} (q : X ⟶ (S.meshRightAlmostSplitAt z).middle) (hq : CategoryTheory.CategoryStruct.comp q (S.realizedRightMeshSink (fun {i j : Fin S.n} => S.standardMeshArrowMap H) z) = 0) : q = 0

At a projective target the completed incoming sink has zero kernel.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardMeshArrowMap_nonprojective_kernel_factor {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) {X : FGModuleCat Aᵐᵒᵖ} (q : X ⟶ (S.meshRightAlmostSplitAt ↑z).middle) (hq : CategoryTheory.CategoryStruct.comp q (S.realizedRightMeshSink (fun {i j : Fin S.n} => S.standardMeshArrowMap H) ↑z) = 0) : ∃ (t : X ⟶ S.fgObj (S.rightTranslationLabel z)), CategoryTheory.CategoryStruct.comp t (S.rightMeshSourceMap H (fun {i j : Fin S.n} => S.standardMeshArrowMap H) z) = q

At a nonprojective target the completed incoming sink has kernel generated by the paired source map from the translate.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshMiddleLift_decomposition_incoming {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X : FGModuleCat Aᵐᵒᵖ} (z : Fin S.n) (c : (a : (y : Fin S.n) × S.MeshArrow z y) → X ⟶ S.almostSplitSkeleton.obj a.fst) (a : (y : Fin S.n) × S.MeshArrow z y) : CategoryTheory.CategoryStruct.comp (S.meshMiddleLift z c) (CategoryTheory.CategoryStruct.comp (S.meshRightAlmostSplitAt z).decomposition.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun (j : (S.meshRightAlmostSplitAt z).index.obj) => S.almostSplitSkeleton.obj ((S.meshRightAlmostSplitAt z).label j)) ↑a.snd) (CategoryTheory.eqToHom ⋯))) = c a

The component formula for meshMiddleLift, stated at an arbitrary incoming arrow rather than at a displayed-middle index.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightMeshSourceMap_decomposition_incoming {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (arrowMap : S.MeshArrowAssignment) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (a : (y : Fin S.n) × S.MeshArrow (↑z) y) : CategoryTheory.CategoryStruct.comp (S.rightMeshSourceMap H (fun {i j : Fin S.n} => arrowMap) z) (CategoryTheory.CategoryStruct.comp (S.meshRightAlmostSplitAt ↑z).decomposition.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun (j : (S.meshRightAlmostSplitAt ↑z).index.obj) => S.almostSplitSkeleton.obj ((S.meshRightAlmostSplitAt ↑z).label j)) ↑a.snd) (CategoryTheory.eqToHom ⋯))) = arrowMap ((S.meshArrowEquiv H z a.fst) a.snd)

The component formula for the paired source map, again indexed by an arbitrary incoming arrow.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshMiddleLift_comp_realizedRightMeshSink {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (arrowMap : S.MeshArrowAssignment) {X : FGModuleCat Aᵐᵒᵖ} (z : Fin S.n) (c : (a : (y : Fin S.n) × S.MeshArrow z y) → X ⟶ S.almostSplitSkeleton.obj a.fst) : CategoryTheory.CategoryStruct.comp (S.meshMiddleLift z c) (S.realizedRightMeshSink (fun {i j : Fin S.n} => arrowMap) z) = ∑ a : (y : Fin S.n) × S.MeshArrow z y, CategoryTheory.CategoryStruct.comp (c a) (arrowMap a.snd)

Composing a map assembled from incoming-arrow coefficients with the assembled sink is the sum of the componentwise composites.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardMeshArrowMap_meshRelation_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : (LinearPathCategory.lift S.almostSplitSkeleton.obj fun {i j : Fin S.n} => S.standardMeshArrowMap H).map ((S.rightMeshData H).meshRelation (S.rightMeshNonprojectiveVertex H z)) = 0

The final assignment kills every ordinary mesh relation.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardMeshRealization {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) : MeshCategory.Realization (S.rightMeshData H) S.almostSplitSkeleton.obj

The recursively chosen arrows descend from the free path category to the ordinary mesh quotient.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardMeshRealization_freeFunctor_full {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) : (S.standardMeshRealization H).freeFunctor.Full

Fullness constructed target by target is exactly fullness of the free linear path realization.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardMeshDirectedExactData {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) : (S.standardMeshRealization H).DirectedExactData

The completed realization satisfies the local exactness hypotheses in Ringel's directed faithfulness argument.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientAddPointHomLinearEquiv {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) : (S.ambientAddPoint x ⟶ S.ambientAddPoint y) ≃ₗ[k] S.fgObj x ⟶ S.fgObj y

Morphisms between ambient selected points are literally morphisms between their underlying finitely generated modules.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardMeshPresentation {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) : S.StandardMeshPresentation (S.rightMeshData H)

Ringel standardness for the concrete right Auslander--Reiten mesh of a directed representation-finite algebra.