Irreducible representatives of standard-form arrows

The standard-form AR quiver indexes parallel arrows by the numerical arrow-multiplicity entry. Here that finite index is identified with the literal occurrences of the required label in the chosen right almost-split middle term. The corresponding middle-term components give concrete irreducible module morphisms. Pulling this assignment to the based universal cover supplies the initial arrow representatives for the two-sided Bongartz--Gabriel normalization.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormOccurrence {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

Occurrences of y in the chosen right almost-split middle term ending at x.

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

The number of literal occurrences with endpoints (y,x) is the official standard-form arrow multiplicity.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormArrowOccurrenceEquiv {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.StandardFormArrow x y ≃ S.StandardFormOccurrence x y

Abstract standard-form arrows are canonically chosen representatives of the corresponding literal middle-term occurrences.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormOccurrenceMiddleIndexEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : (y : Fin S.n) × S.StandardFormOccurrence x y ≃ Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData x)

Forgetting the retained label identifies the disjoint union of all occurrence fibres with the full finite middle-index type.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMiddleIndexEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData x) ≃ (y : Fin S.n) × S.StandardFormArrow x y

The displayed middle indices at x are exactly the standard-form arrows leaving x, with the target label retained in the dependent sum.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMiddleIndexEquiv_fst {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData x)) : ((S.standardFormMiddleIndexEquiv x) i).fst = FiniteTauMatrix.rightMiddleLabel S.finiteTauCategoryData.toFiniteRightTauCategoryData x i

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormArrowOccurrenceEquiv_middleIndex {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData x)) : (S.standardFormArrowOccurrenceEquiv x ((S.standardFormMiddleIndexEquiv x) i).fst) ((S.standardFormMiddleIndexEquiv x) i).snd = ⟨i, ⋯⟩

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormArrowMap {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} (a : S.StandardFormArrow x y) : S.fgObj y ⟶ S.fgObj x

The irreducible module morphism represented by one reversed standard-form arrow.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormArrowMap_middleIndex {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData x)) : S.standardFormArrowMap ((S.standardFormMiddleIndexEquiv x) i).snd = FiniteTauMatrix.rightMiddleComponent S.finiteTauCategoryData x i

The arrow attached to the i-th middle index is its actual chosen right-mesh component.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteTauCategoryData_obj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : S.finiteTauCategoryData.obj x = S.fgObj x

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRightSink {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : (S.finiteTauCategoryData.rightMesh (S.fgObj x)).X₂ ⟶ S.fgObj x

The terminal map of the chosen right mesh, after identifying its endpoint with the selected indecomposable representative.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRightSink_isRightAlmostSplit {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (S.standardFormRightSink x)

The chosen standard-form right sink is right almost split.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRightSink_isRightMinimal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : QuotientSubmoduleEquidistribution.IsRightMinimal (S.standardFormRightSink x)

The chosen standard-form right sink is right minimal.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSinkArrowMap {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} (g : (S.finiteTauCategoryData.rightMesh (S.fgObj x)).X₂ ⟶ S.fgObj x) (a : S.StandardFormArrow x y) : S.fgObj y ⟶ S.fgObj x

Take the occurrence component of an arbitrary replacement sink at one standard-form vertex.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSinkArrowMap_rightSink {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} (a : S.StandardFormArrow x y) : S.standardFormSinkArrowMap (S.standardFormRightSink x) a = S.standardFormArrowMap a

The initial arrow representative is the occurrence component of the chosen right almost-split sink.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormArrowMap_isIrreducible {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} (a : S.StandardFormArrow x y) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (S.standardFormArrowMap a)

Every chosen standard-form arrow representative is irreducible.

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

A nonprojective standard-form vertex as the corresponding nonzero right boundary of the finite tau-category.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormFiniteTauNonprojective_val {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // z ∉ S.standardFormProjectiveSet }) : ↑(S.standardFormFiniteTauNonprojective z) = ↑z

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteTauCategoryData_tauPlus_standardFormTau {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // z ∉ S.standardFormProjectiveSet }) : S.finiteTauCategoryData.tauPlus (S.standardFormFiniteTauNonprojective z) = S.standardFormTau z

The finite-tau positive translate and the standard-form translation have the same underlying label.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRightSource {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // z ∉ S.standardFormProjectiveSet }) : S.fgObj (S.standardFormTau z) ⟶ (S.finiteTauCategoryData.rightMesh (S.fgObj ↑z)).X₂

The first map of the chosen right mesh, with its source identified with the standard-form translate.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRightSource_mono {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // z ∉ S.standardFormProjectiveSet }) : CategoryTheory.Mono (S.standardFormRightSource z)

The first map of the chosen nonprojective standard-form right mesh is monic: it is the selected Auslander--Reiten kernel inclusion, up to the two displayed source identifications.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRightSource_isLeftAlmostSplit {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // z ∉ S.standardFormProjectiveSet }) : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit (S.standardFormRightSource z)

The identified first map of a chosen nonprojective right mesh is left almost split.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRightSource_isLeftMinimal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // z ∉ S.standardFormProjectiveSet }) : QuotientSubmoduleEquidistribution.IsLeftMinimal (S.standardFormRightSource z)

The identified first map of a chosen nonprojective right mesh is left minimal.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRightSource_comp_rightSink {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // z ∉ S.standardFormProjectiveSet }) : CategoryTheory.CategoryStruct.comp (S.standardFormRightSource z) (S.standardFormRightSink ↑z) = 0

The identified chosen right-mesh source and sink have zero composite.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRightSource_comp_rightSink_assoc {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // z ∉ S.standardFormProjectiveSet }) {Z : FinitelyGeneratedCategory A} (h : S.fgObj ↑z ⟶ Z) : CategoryTheory.CategoryStruct.comp (S.standardFormRightSource z) (CategoryTheory.CategoryStruct.comp (S.standardFormRightSink ↑z) h) = CategoryTheory.CategoryStruct.comp 0 h

The identified chosen right-mesh source and sink have zero composite.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRightSource_factors_of_comp_rightSink_eq_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // z ∉ S.standardFormProjectiveSet }) {X : FGModuleCat Aᵐᵒᵖ} (q : X ⟶ (S.finiteTauCategoryData.rightMesh (S.fgObj ↑z)).X₂) (hq : CategoryTheory.CategoryStruct.comp q (S.standardFormRightSink ↑z) = 0) : ∃ (t : X ⟶ S.fgObj (S.standardFormTau z)), CategoryTheory.CategoryStruct.comp t (S.standardFormRightSource z) = q

The identified first map of a chosen nonprojective right mesh is a weak kernel of its identified sink. Thus every morphism killed by the sink factors through the standard-form translate.

@[instance_reducible]

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

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMiddleBaseStar {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) : Quiver.Star W.fst

The finite middle index at a cover vertex, regarded as its corresponding outgoing arrow downstairs.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMiddleVertex {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀

The target cover vertex obtained by lifting one displayed middle occurrence from W.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMiddleArrow {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) : W ⟶ S.standardFormUniversalMiddleVertex x₀ W i

The unique lifted outgoing arrow represented by one displayed middle occurrence.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMiddleVertex_base {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) : (S.standardFormUniversalMiddleVertex x₀ W i).fst = FiniteTauMatrix.rightMiddleLabel S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst i

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMiddleArrow_val {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) : ↑(S.standardFormUniversalMiddleArrow x₀ W i) = ((S.standardFormMiddleIndexEquiv W.fst) i).snd

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMiddleStarEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst) ≃ Quiver.Star W

The displayed middle indices exhaust the outgoing star at every universal-cover vertex.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMiddleStarEquiv_apply {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) : (S.standardFormUniversalMiddleStarEquiv x₀ W) i = ⟨S.standardFormUniversalMiddleVertex x₀ W i, S.standardFormUniversalMiddleArrow x₀ W i⟩

The abstract star-equivalence lift is the explicit arrow obtained by extendOld.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) : FGModuleCat Aᵐᵒᵖ

The downstairs module object attached to a universal-cover vertex.

@[reducible, inline]

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

An arbitrary choice of module representative for every reversed arrow of the based universal cover.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalPairedMiddleArrow {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData (↑W).fst)) : S.standardFormUniversalMiddleVertex x₀ (↑W) i ⟶ MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ W

The polarized partner of the lifted arrow represented by one displayed middle occurrence at a nonprojective cover vertex.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalPairedMiddleArrow_val {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData (↑W).fst)) : ↑(S.standardFormUniversalPairedMiddleArrow x₀ W i) = (S.standardFormRightMeshData.arrowEquiv (MeshCategory.RightMeshData.UniversalCover.baseNonprojective S.standardFormRightMeshData x₀ W) (S.standardFormUniversalMiddleVertex x₀ (↑W) i).fst) ((S.standardFormMiddleIndexEquiv (↑W).fst) i).snd

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizedSource {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (D : S.StandardFormUniversalArrowAssignment x₀) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) : S.fgObj (S.standardFormTau (MeshCategory.RightMeshData.UniversalCover.baseNonprojective S.standardFormRightMeshData x₀ W)) ⟶ (S.finiteTauCategoryData.rightMesh (S.fgObj (↑W).fst)).X₂

Assemble the representatives on the polarized partner arrows into the source map of the lifted mesh at W.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizedSource_rightMiddleProjection {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (D : S.StandardFormUniversalArrowAssignment x₀) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData (↑W).fst)) : CategoryTheory.CategoryStruct.comp (S.standardFormUniversalRealizedSource x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W) (FiniteTauMatrix.rightMiddleProjection S.finiteTauCategoryData (↑W).fst i) = D (S.standardFormUniversalPairedMiddleArrow x₀ W i)

Projection to the i-th displayed summand recovers the representative on its polarized partner arrow.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizedSource_rightMiddleProjection_assoc {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (D : S.StandardFormUniversalArrowAssignment x₀) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData (↑W).fst)) {Z : FinitelyGeneratedCategory A} (h : S.finiteTauCategoryData.obj (FiniteTauMatrix.rightMiddleLabel S.finiteTauCategoryData.toFiniteRightTauCategoryData (↑W).fst i) ⟶ Z) : CategoryTheory.CategoryStruct.comp (S.standardFormUniversalRealizedSource x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W) (CategoryTheory.CategoryStruct.comp (FiniteTauMatrix.rightMiddleProjection S.finiteTauCategoryData (↑W).fst i) h) = CategoryTheory.CategoryStruct.comp (D (S.standardFormUniversalPairedMiddleArrow x₀ W i)) h

Projection to the i-th displayed summand recovers the representative on its polarized partner arrow.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizedSink {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (D : S.StandardFormUniversalArrowAssignment x₀) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) : (S.finiteTauCategoryData.rightMesh (S.fgObj W.fst)).X₂ ⟶ S.fgObj W.fst

Reassemble all arrow representatives leaving W into a single map from the chosen right-mesh middle term to its endpoint.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightMiddleInclusion_standardFormUniversalRealizedSink {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (D : S.StandardFormUniversalArrowAssignment x₀) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) : CategoryTheory.CategoryStruct.comp (FiniteTauMatrix.rightMiddleInclusion S.finiteTauCategoryData W.fst i) (S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W) = D (S.standardFormUniversalMiddleArrow x₀ W i)

The i-th component of the reassembled sink is the representative on the corresponding lifted arrow.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightMiddleInclusion_standardFormUniversalRealizedSink_assoc {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (D : S.StandardFormUniversalArrowAssignment x₀) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) {Z : FinitelyGeneratedCategory A} (h : S.fgObj W.fst ⟶ Z) : CategoryTheory.CategoryStruct.comp (FiniteTauMatrix.rightMiddleInclusion S.finiteTauCategoryData W.fst i) (CategoryTheory.CategoryStruct.comp (S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W) h) = CategoryTheory.CategoryStruct.comp (D (S.standardFormUniversalMiddleArrow x₀ W i)) h

The i-th component of the reassembled sink is the representative on the corresponding lifted arrow.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalArrowMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (a : W ⟶ Z) : S.standardFormUniversalObj x₀ Z ⟶ S.standardFormUniversalObj x₀ W

Initial irreducible arrow representatives on the universal cover, pulled back from the chosen standard-form occurrence representatives.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalArrowMap_isIrreducible {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (a : W ⟶ Z) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (S.standardFormUniversalArrowMap x₀ a)

Every initial universal-cover arrow representative is irreducible.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizedSink_arrowMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) : S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.standardFormUniversalArrowMap x₀) W = S.standardFormRightSink W.fst

Reassembling the initial lifted representatives recovers the chosen downstairs right almost-split sink exactly.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalSinkArrowMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (g : (S.finiteTauCategoryData.rightMesh (S.fgObj W.fst)).X₂ ⟶ S.fgObj W.fst) {Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (a : W ⟶ Z) : S.standardFormUniversalObj x₀ Z ⟶ S.standardFormUniversalObj x₀ W

Occurrence component of a replacement right sink at one universal-cover vertex.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalSinkArrowMap_middleArrow {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (g : (S.finiteTauCategoryData.rightMesh (S.fgObj W.fst)).X₂ ⟶ S.fgObj W.fst) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) : S.standardFormUniversalSinkArrowMap x₀ W g (S.standardFormUniversalMiddleArrow x₀ W i) = CategoryTheory.CategoryStruct.comp (FiniteTauMatrix.rightMiddleInclusion S.finiteTauCategoryData W.fst i) g

On an explicitly indexed lifted arrow, sink-component extraction is literally precomposition with the corresponding middle inclusion.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalSinkArrowMap_realizedSink_middleArrow {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (D : S.StandardFormUniversalArrowAssignment x₀) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) : S.standardFormUniversalSinkArrowMap x₀ W (S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W) (S.standardFormUniversalMiddleArrow x₀ W i) = D (S.standardFormUniversalMiddleArrow x₀ W i)

Extracting a displayed middle component from the sink reassembled from D returns that arrow representative.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalSinkArrowMap_realizedSink {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (D : S.StandardFormUniversalArrowAssignment x₀) {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (a : W ⟶ Z) : S.standardFormUniversalSinkArrowMap x₀ W (S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W) a = D a

Reassembly followed by component extraction is the identity for every universal-cover arrow, not only for the explicitly displayed lift.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalSinkArrowMap_rightSink {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) {Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (a : W ⟶ Z) : S.standardFormUniversalSinkArrowMap x₀ W (S.standardFormRightSink W.fst) a = S.standardFormUniversalArrowMap x₀ a

Initially, every lifted arrow is the occurrence component of the chosen downstairs right almost-split sink.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.replaceStandardFormUniversalArrowMapAt {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (D : S.StandardFormUniversalArrowAssignment x₀) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (g : (S.finiteTauCategoryData.rightMesh (S.fgObj W.fst)).X₂ ⟶ S.fgObj W.fst) : S.StandardFormUniversalArrowAssignment x₀

Replace all arrow representatives whose reversed-quiver source is one fixed universal-cover vertex.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.replaceStandardFormUniversalArrowMapAt_eq {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (D : S.StandardFormUniversalArrowAssignment x₀) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (g : (S.finiteTauCategoryData.rightMesh (S.fgObj W.fst)).X₂ ⟶ S.fgObj W.fst) {Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (a : W ⟶ Z) : S.replaceStandardFormUniversalArrowMapAt x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W g a = S.standardFormUniversalSinkArrowMap x₀ W g a

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.replaceStandardFormUniversalArrowMapAt_eq_of_ne {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (D : S.StandardFormUniversalArrowAssignment x₀) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (g : (S.finiteTauCategoryData.rightMesh (S.fgObj W.fst)).X₂ ⟶ S.fgObj W.fst) {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (hYW : Y ≠ W) (a : Y ⟶ Z) : S.replaceStandardFormUniversalArrowMapAt x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W g a = D a

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizedSink_replaceAt_eq {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (D : S.StandardFormUniversalArrowAssignment x₀) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (g : (S.finiteTauCategoryData.rightMesh (S.fgObj W.fst)).X₂ ⟶ S.fgObj W.fst) : S.standardFormUniversalRealizedSink x₀ (fun {W_1 Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.replaceStandardFormUniversalArrowMapAt x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W g) W = g

Reassembling at the replaced vertex recovers the replacement sink exactly.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizedSink_replaceAt_eq_of_ne {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (D : S.StandardFormUniversalArrowAssignment x₀) (W Y : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (g : (S.finiteTauCategoryData.rightMesh (S.fgObj W.fst)).X₂ ⟶ S.fgObj W.fst) (hYW : Y ≠ W) : S.standardFormUniversalRealizedSink x₀ (fun {W_1 Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.replaceStandardFormUniversalArrowMapAt x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W g) Y = S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) Y

A replacement at W leaves every realized sink at a different source vertex unchanged.

structure MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSinkCondition {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (D : S.StandardFormUniversalArrowAssignment x₀) : Prop

The inductive invariant: every realized sink is minimal right almost split.

• rightAlmostSplit (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W)
• rightMinimal (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) : QuotientSubmoduleEquidistribution.IsRightMinimal (S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalArrowMap_sinkCondition {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) : S.StandardFormUniversalSinkCondition x₀ fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.standardFormUniversalArrowMap x₀

The initial occurrence-component assignment satisfies the sink condition.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSinkCondition.replaceAt {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) {D : S.StandardFormUniversalArrowAssignment x₀} (hD : S.StandardFormUniversalSinkCondition x₀ fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (g : (S.finiteTauCategoryData.rightMesh (S.fgObj W.fst)).X₂ ⟶ S.fgObj W.fst) (hg : QuotientSubmoduleEquidistribution.IsRightAlmostSplit g) (hgmin : QuotientSubmoduleEquidistribution.IsRightMinimal g) : S.StandardFormUniversalSinkCondition x₀ fun {W_1 Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.replaceStandardFormUniversalArrowMapAt x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W g

Replacing one realized sink by another minimal right almost-split sink preserves the inductive invariant globally.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.replaceStandardFormUniversalArrowMapAtHeight {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (D : S.StandardFormUniversalArrowAssignment x₀) (m : ℤ) (g : (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) → MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ W = m → ((S.finiteTauCategoryData.rightMesh (S.fgObj W.fst)).X₂ ⟶ S.fgObj W.fst)) : S.StandardFormUniversalArrowAssignment x₀

Simultaneously replace the outgoing representatives at every cover vertex of one Bongartz--Gabriel height. No enumeration of the (potentially infinite) height fibre is required because each arrow has a unique source.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.replaceStandardFormUniversalArrowMapAtHeight_eq {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (D : S.StandardFormUniversalArrowAssignment x₀) (m : ℤ) (g : (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) → MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ W = m → ((S.finiteTauCategoryData.rightMesh (S.fgObj W.fst)).X₂ ⟶ S.fgObj W.fst)) {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (hW : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ W = m) (a : W ⟶ Z) : S.replaceStandardFormUniversalArrowMapAtHeight x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) m g a = S.standardFormUniversalSinkArrowMap x₀ W (g W hW) a

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.replaceStandardFormUniversalArrowMapAtHeight_eq_of_ne {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (D : S.StandardFormUniversalArrowAssignment x₀) (m : ℤ) (g : (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) → MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ W = m → ((S.finiteTauCategoryData.rightMesh (S.fgObj W.fst)).X₂ ⟶ S.fgObj W.fst)) {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (hW : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ W ≠ m) (a : W ⟶ Z) : S.replaceStandardFormUniversalArrowMapAtHeight x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) m g a = D a

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizedSink_replaceAtHeight_eq {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (D : S.StandardFormUniversalArrowAssignment x₀) (m : ℤ) (g : (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) → MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ W = m → ((S.finiteTauCategoryData.rightMesh (S.fgObj W.fst)).X₂ ⟶ S.fgObj W.fst)) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (hW : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ W = m) : S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.replaceStandardFormUniversalArrowMapAtHeight x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) m g) W = g W hW

At a selected height, reassembling the simultaneous replacement returns the supplied sink at that vertex.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizedSink_replaceAtHeight_eq_of_ne {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) (D : S.StandardFormUniversalArrowAssignment x₀) (m : ℤ) (g : (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) → MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ W = m → ((S.finiteTauCategoryData.rightMesh (S.fgObj W.fst)).X₂ ⟶ S.fgObj W.fst)) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (hW : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ W ≠ m) : S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.replaceStandardFormUniversalArrowMapAtHeight x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) m g) W = S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W

Outside the selected height, simultaneous replacement leaves the realized sink unchanged.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSinkCondition.replaceAtHeight {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x₀ : Fin S.n) {D : S.StandardFormUniversalArrowAssignment x₀} (hD : S.StandardFormUniversalSinkCondition x₀ fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) (m : ℤ) (g : (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) → MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ W = m → ((S.finiteTauCategoryData.rightMesh (S.fgObj W.fst)).X₂ ⟶ S.fgObj W.fst)) (hg : ∀ (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (hW : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ W = m), QuotientSubmoduleEquidistribution.IsRightAlmostSplit (g W hW)) (hgmin : ∀ (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (hW : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ W = m), QuotientSubmoduleEquidistribution.IsRightMinimal (g W hW)) : S.StandardFormUniversalSinkCondition x₀ fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.replaceStandardFormUniversalArrowMapAtHeight x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) m g

A simultaneous height replacement by minimal right almost-split sinks preserves the global sink condition.