Dual normalization on the standard-form universal cover

The positive-height construction normalizes realized sinks. This file implements the dual induction on arrows whose module-theoretic source has nonpositive Bongartz--Gabriel height. It normalizes realized sources while retaining their minimal left almost-split invariant.

@[instance_reducible]

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

@[reducible, inline]

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

A lifted standard-form vertex whose represented module is noninjective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRightMeshData_arrowEquiv_cast {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {z z' : { z : Fin S.n // z ∉ S.standardFormRightMeshData.projective }} (h : z = z') (y : Fin S.n) (b : S.StandardFormArrow (↑z) y) : Quiver.Hom.cast ⋯ ⋯ ((S.standardFormRightMeshData.arrowEquiv z y) b) = (S.standardFormRightMeshData.arrowEquiv z' y) (Quiver.Hom.cast ⋯ ⋯ b)

Polarization commutes with transport of its nonprojective mesh endpoint.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRightMeshData_arrowEquiv_symm_cast {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {z z' : { z : Fin S.n // z ∉ S.standardFormRightMeshData.projective }} (h : z = z') (y : Fin S.n) (a : S.StandardFormArrow y (S.standardFormRightMeshData.tau z)) : Quiver.Hom.cast ⋯ ⋯ ((S.standardFormRightMeshData.arrowEquiv z y).symm a) = (S.standardFormRightMeshData.arrowEquiv z' y).symm (Quiver.Hom.cast ⋯ ⋯ a)

The inverse polarization also commutes with transport of its nonprojective mesh endpoint.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSourceArrowMap {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.standardFormRightMeshData.projective }) (g : S.finiteTauCategoryData.obj (S.standardFormRightMeshData.tau z) ⟶ (S.finiteTauCategoryData.rightMesh (S.finiteTauCategoryData.obj ↑z)).X₂) {y : Fin S.n} (a : S.StandardFormArrow y (S.standardFormRightMeshData.tau z)) : S.finiteTauCategoryData.obj (S.standardFormRightMeshData.tau z) ⟶ S.finiteTauCategoryData.obj y

Extract a component from a replacement source at one downstairs noninjective standard-form vertex.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSourceArrowMap_paired {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.standardFormRightMeshData.projective }) (g : S.finiteTauCategoryData.obj (S.standardFormRightMeshData.tau z) ⟶ (S.finiteTauCategoryData.rightMesh (S.finiteTauCategoryData.obj ↑z)).X₂) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData ↑z)) : S.standardFormSourceArrowMap z g ((S.standardFormRightMeshData.arrowEquiv z ((S.standardFormMiddleIndexEquiv ↑z) i).fst) ((S.standardFormMiddleIndexEquiv ↑z) i).snd) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (FiniteTauMatrix.rightMiddleProjection S.finiteTauCategoryData (↑z) i) (CategoryTheory.eqToHom ⋯))

On a polarized displayed occurrence, downstairs source-component extraction is literal postcomposition with the middle projection.

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

Extract from a replacement mesh source the component represented by one arrow ending at the translated vertex.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalSourceArrowMap_pairedMiddleArrow {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) (g : S.fgObj (S.standardFormTau (MeshCategory.RightMeshData.UniversalCover.baseNonprojective S.standardFormRightMeshData x₀ W)) ⟶ (S.finiteTauCategoryData.rightMesh (S.fgObj (↑W).fst)).X₂) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData (↑W).fst)) : S.standardFormUniversalSourceArrowMap x₀ W g (S.standardFormUniversalPairedMiddleArrow x₀ W i) = CategoryTheory.CategoryStruct.comp g (FiniteTauMatrix.rightMiddleProjection S.finiteTauCategoryData (↑(MeshCategory.RightMeshData.UniversalCover.baseNonprojective S.standardFormRightMeshData x₀ W)) i)

Component extraction recovers the indicated component on each explicit polarized middle arrow.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalSourceArrowMap_transport {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (m : ℤ) (g : (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) → MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ (MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ W) = m → (S.fgObj (S.standardFormTau (MeshCategory.RightMeshData.UniversalCover.baseNonprojective S.standardFormRightMeshData x₀ W)) ⟶ (S.finiteTauCategoryData.rightMesh (S.fgObj (↑W).fst)).X₂)) {Y : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (W' W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) (h : W' = W) (b' : ↑W' ⟶ Y) (b : ↑W ⟶ Y) (hb : Quiver.Hom.cast ⋯ ⋯ b' = b) (hW' : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ (MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ W') = m) (hW : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ (MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ W) = m) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (S.standardFormUniversalSourceArrowMap x₀ W' (g W' hW') (MeshCategory.RightMeshData.UniversalCover.pairedArrow S.standardFormRightMeshData x₀ W' Y b')) = S.standardFormUniversalSourceArrowMap x₀ W (g W hW) (MeshCategory.RightMeshData.UniversalCover.pairedArrow S.standardFormRightMeshData x₀ W Y b)

Source-component extraction is invariant under simultaneous transport of the lifted mesh endpoint and its outgoing arrow.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalArrowSourceBase {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (_a : Y ⟶ Z) (hZ : ¬CategoryTheory.Injective (S.fgObj Z.fst)) : { z : Fin S.n // z ∉ S.standardFormRightMeshData.projective }

For an arrow whose represented module source is noninjective, recover the downstairs endpoint of the right mesh that produces it by polarization.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalArrowSourceBase_tau {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (a : Y ⟶ Z) (hZ : ¬CategoryTheory.Injective (S.fgObj Z.fst)) : S.standardFormRightMeshData.tau (S.standardFormUniversalArrowSourceBase x₀ a hZ) = Z.fst

The recovered downstairs mesh endpoint translates to the arrow target's base label.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalArrowSourceBasePartner {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (a : Y ⟶ Z) (hZ : ¬CategoryTheory.Injective (S.fgObj Z.fst)) : S.StandardFormArrow (↑(S.standardFormUniversalArrowSourceBase x₀ a hZ)) Y.fst

The downstairs polarized partner of an arrow ending at a noninjective lifted vertex.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalArrowSourceCostar {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (a : Y ⟶ Z) (hZ : ¬CategoryTheory.Injective (S.fgObj Z.fst)) : Quiver.Costar Y

Lift the recovered downstairs polarized partner into the costar of the arrow's source vertex. This determines the unique lifted mesh containing the arrow.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalArrowSourceCostar_projection {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (a : Y ⟶ Z) (hZ : ¬CategoryTheory.Injective (S.fgObj Z.fst)) : (MeshCategory.RightMeshData.UniversalCover.projection S.standardFormRightMeshData x₀).costar Y (S.standardFormUniversalArrowSourceCostar x₀ a hZ) = ⟨↑(S.standardFormUniversalArrowSourceBase x₀ a hZ), S.standardFormUniversalArrowSourceBasePartner x₀ a hZ⟩

Projecting the recovered costar lift returns its defining downstairs polarized partner.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalArrowSourceMesh {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (a : Y ⟶ Z) (hZ : ¬CategoryTheory.Injective (S.fgObj Z.fst)) : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }

The nonprojective lifted mesh endpoint recovered from an arrow ending at a noninjective vertex.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalArrowSourceMeshArrow {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (a : Y ⟶ Z) (hZ : ¬CategoryTheory.Injective (S.fgObj Z.fst)) : ↑(S.standardFormUniversalArrowSourceMesh x₀ a hZ) ⟶ Y

The lifted polarized partner from the recovered mesh endpoint to the original arrow's source vertex.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalArrowSourceMesh_costar {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (a : Y ⟶ Z) (hZ : ¬CategoryTheory.Injective (S.fgObj Z.fst)) : ⟨↑(S.standardFormUniversalArrowSourceMesh x₀ a hZ), S.standardFormUniversalArrowSourceMeshArrow x₀ a hZ⟩ = S.standardFormUniversalArrowSourceCostar x₀ a hZ

The recovered mesh endpoint and arrow are exactly the costar lift constructed above.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalArrowSourceMesh_base {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (a : Y ⟶ Z) (hZ : ¬CategoryTheory.Injective (S.fgObj Z.fst)) : (↑(S.standardFormUniversalArrowSourceMesh x₀ a hZ)).fst = ↑(S.standardFormUniversalArrowSourceBase x₀ a hZ)

The recovered lifted mesh endpoint lies over its recovered downstairs endpoint.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalArrowSourceMeshArrow_val {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (a : Y ⟶ Z) (hZ : ¬CategoryTheory.Injective (S.fgObj Z.fst)) : Quiver.Hom.cast ⋯ ⋯ ↑(S.standardFormUniversalArrowSourceMeshArrow x₀ a hZ) = S.standardFormUniversalArrowSourceBasePartner x₀ a hZ

After the base-label transport, the recovered lifted arrow projects to the recovered downstairs polarized partner.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalArrowSourceMesh_paired {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (a : Y ⟶ Z) (hZ : ¬CategoryTheory.Injective (S.fgObj Z.fst)) : ⟨MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ (S.standardFormUniversalArrowSourceMesh x₀ a hZ), MeshCategory.RightMeshData.UniversalCover.pairedArrow S.standardFormRightMeshData x₀ (S.standardFormUniversalArrowSourceMesh x₀ a hZ) Y (S.standardFormUniversalArrowSourceMeshArrow x₀ a hZ)⟩ = ⟨Z, a⟩

Pairing the recovered mesh arrow returns the original universal-cover arrow, including its target vertex.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_tau_noninjective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) : ¬CategoryTheory.Injective (S.fgObj (MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ W).fst)

The translated source vertex of every universal mesh represents a noninjective module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalArrowSourceCostar_pairedMiddleArrow {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (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.standardFormUniversalArrowSourceMesh x₀ (S.standardFormUniversalPairedMiddleArrow x₀ W i) ⋯), S.standardFormUniversalArrowSourceMeshArrow x₀ (S.standardFormUniversalPairedMiddleArrow x₀ W i) ⋯⟩ = ⟨↑W, S.standardFormUniversalMiddleArrow x₀ (↑W) i⟩

Applied to an explicit polarized mesh arrow, the recovered costar is the original lifted middle arrow.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalArrowSourceMesh_pairedMiddleArrow {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (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.standardFormUniversalArrowSourceMesh x₀ (S.standardFormUniversalPairedMiddleArrow x₀ W i) ⋯ = W

Applied to an explicit polarized mesh arrow, source-mesh recovery returns the original lifted mesh endpoint.

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

Simultaneously replace source components on all arrows whose represented module source has one fixed height. Injective sources are left unchanged; every other arrow canonically recovers its unique lifted mesh.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.replaceStandardFormUniversalArrowMapAtTargetHeight_pairedMiddleArrow {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (D : S.StandardFormUniversalArrowAssignment x₀) (m : ℤ) (g : (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) → MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ (MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ W) = m → (S.fgObj (S.standardFormTau (MeshCategory.RightMeshData.UniversalCover.baseNonprojective S.standardFormRightMeshData x₀ W)) ⟶ (S.finiteTauCategoryData.rightMesh (S.fgObj (↑W).fst)).X₂)) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) (hW : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ (MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ W) = m) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData (↑W).fst)) : S.replaceStandardFormUniversalArrowMapAtTargetHeight x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) m g (S.standardFormUniversalPairedMiddleArrow x₀ W i) = CategoryTheory.CategoryStruct.comp (g W hW) (FiniteTauMatrix.rightMiddleProjection S.finiteTauCategoryData (↑W).fst i)

At a selected mesh source height, simultaneous source replacement returns the supplied component on every displayed paired arrow.

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

Target-height replacement leaves an arrow unchanged away from the selected target height.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.replaceStandardFormUniversalArrowMapAtTargetHeight_eq_of_injective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (D : S.StandardFormUniversalArrowAssignment x₀) (m : ℤ) (g : (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) → MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ (MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ W) = m → (S.fgObj (S.standardFormTau (MeshCategory.RightMeshData.UniversalCover.baseNonprojective S.standardFormRightMeshData x₀ W)) ⟶ (S.finiteTauCategoryData.rightMesh (S.fgObj (↑W).fst)).X₂)) {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (hZ : CategoryTheory.Injective (S.fgObj Z.fst)) (a : Y ⟶ Z) : S.replaceStandardFormUniversalArrowMapAtTargetHeight x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) m g a = D a

Target-height replacement also leaves arrows ending at injective vertices unchanged.

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

At the selected translated-source height, the source assembled from all replaced components is exactly the supplied source.

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

Away from the selected translated-source height, target-height replacement leaves the realized mesh source unchanged.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.isIrreducible_comp_of_leftAlmostSplit_leftMinimal {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} {E : FinitelyGeneratedCategory A} (inc : S.fgObj y ⟶ E) (proj : E ⟶ S.fgObj y) (hinc : CategoryTheory.CategoryStruct.comp inc proj = CategoryTheory.CategoryStruct.id (S.fgObj y)) (g : S.fgObj x ⟶ E) (hg : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit g) (hgmin : QuotientSubmoduleEquidistribution.IsLeftMinimal g) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (CategoryTheory.CategoryStruct.comp g proj)

A component cut out by a split projection from a minimal left almost-split morphism between selected indecomposables is irreducible.

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

The global invariant used by the descending source normalization.

• arrow_isIrreducible {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (a : Y ⟶ Z) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (D a)
• leftAlmostSplit (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit (S.standardFormUniversalRealizedSource x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W)
• leftMinimal (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) : QuotientSubmoduleEquidistribution.IsLeftMinimal (S.standardFormUniversalRealizedSource x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W)

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

The positive limiting assignment supplies the initial invariant for the descending source normalization.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSourceCondition.exists_realizedSink_iso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {D : S.StandardFormUniversalArrowAssignment x₀} (hD : S.StandardFormUniversalSourceCondition x₀ fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) : ∃ (e : (S.finiteTauCategoryData.rightMesh (S.fgObj W.fst)).X₂ ≅ (S.finiteTauCategoryData.rightMesh (S.fgObj W.fst)).X₂), CategoryTheory.CategoryStruct.comp e.hom (S.standardFormRightSink W.fst) = S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W

Under the global source invariant, each realized sink differs from the chosen right almost-split sink by an automorphism of the displayed middle term.

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

The canonical comparison automorphism between the chosen mesh sink and the sink assembled from a source-compatible assignment.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSourceCondition.realizedSinkIso_comp_rightSink {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {D : S.StandardFormUniversalArrowAssignment x₀} (hD : S.StandardFormUniversalSourceCondition x₀ fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) : CategoryTheory.CategoryStruct.comp (realizedSinkIso S x₀ hD W).hom (S.standardFormRightSink W.fst) = S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W

The comparison automorphism realizes the assembled sink exactly.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSourceCondition.realizedSink_isRightAlmostSplit {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {D : S.StandardFormUniversalArrowAssignment x₀} (hD : S.StandardFormUniversalSourceCondition x₀ fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) (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)

Every sink assembled from a source-compatible assignment is right almost split, including the projective boundary vertices.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSourceCondition.normalizedSource {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {D : S.StandardFormUniversalArrowAssignment x₀} (hD : S.StandardFormUniversalSourceCondition x₀ fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) (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₂

Twist the chosen mesh source by the inverse sink comparison.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSourceCondition.normalizedSource_comp_realizedSink {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {D : S.StandardFormUniversalArrowAssignment x₀} (hD : S.StandardFormUniversalSourceCondition x₀ fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) : CategoryTheory.CategoryStruct.comp (normalizedSource S x₀ hD W) (S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) ↑W) = 0

The normalized source has zero composite with the currently realized sink.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSourceCondition.normalizedSource_comp_realizedSink_assoc {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {D : S.StandardFormUniversalArrowAssignment x₀} (hD : S.StandardFormUniversalSourceCondition x₀ fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) {Z : FinitelyGeneratedCategory A} (h : S.fgObj (↑W).fst ⟶ Z) : CategoryTheory.CategoryStruct.comp (normalizedSource S x₀ hD W) (CategoryTheory.CategoryStruct.comp (S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) ↑W) h) = CategoryTheory.CategoryStruct.comp 0 h

The normalized source has zero composite with the currently realized sink.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSourceCondition.normalizedSource_isLeftAlmostSplit {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {D : S.StandardFormUniversalArrowAssignment x₀} (hD : S.StandardFormUniversalSourceCondition x₀ fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit (normalizedSource S x₀ hD W)

The normalized source remains left almost split.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSourceCondition.normalizedSource_isLeftMinimal {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {D : S.StandardFormUniversalArrowAssignment x₀} (hD : S.StandardFormUniversalSourceCondition x₀ fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) : QuotientSubmoduleEquidistribution.IsLeftMinimal (normalizedSource S x₀ hD W)

The normalized source remains left minimal.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.isIrreducibleMorphism_eqToHom_comp {A : Type u} [Ring A] {X X' Y : FinitelyGeneratedCategory A} (h : X = X') (f : X' ⟶ Y) (hf : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) f)

Precomposition by equality transport preserves irreducibility.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.isIrreducibleMorphism_comp_eqToHom {A : Type u} [Ring A] {X Y Y' : FinitelyGeneratedCategory A} (h : Y = Y') (f : X ⟶ Y) (hf : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom h))

Postcomposition by equality transport preserves irreducibility.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSourceCondition.normalizedSourceArrowMap_isIrreducible {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {D : S.StandardFormUniversalArrowAssignment x₀} (hD : S.StandardFormUniversalSourceCondition x₀ fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) {Y : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (b : ↑W ⟶ Y) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (S.standardFormUniversalSourceArrowMap x₀ W (normalizedSource S x₀ hD W) (MeshCategory.RightMeshData.UniversalCover.pairedArrow S.standardFormRightMeshData x₀ W Y b))

Every component extracted from the normalized source is irreducible.

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

The replacement source used at one translated-source height.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSourceCondition.normalizeAtTargetHeight {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {D : S.StandardFormUniversalArrowAssignment x₀} (hD : S.StandardFormUniversalSourceCondition x₀ fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) (m : ℤ) : S.StandardFormUniversalArrowAssignment x₀

Simultaneously normalize all mesh sources whose translated vertex has one fixed height.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizedSink_replaceAtTargetHeight_eq {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (D : S.StandardFormUniversalArrowAssignment x₀) (m : ℤ) (g : (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) → MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ (MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ W) = m → (S.fgObj (S.standardFormTau (MeshCategory.RightMeshData.UniversalCover.baseNonprojective S.standardFormRightMeshData x₀ W)) ⟶ (S.finiteTauCategoryData.rightMesh (S.fgObj (↑W).fst)).X₂)) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) (hW : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ (MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ W) = m) : S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.replaceStandardFormUniversalArrowMapAtTargetHeight 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

Replacing sources at translated height m does not alter the realized sink in the same mesh: its outgoing arrows end at height m + 1.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSourceCondition.normalizeAtTargetHeight_sourceCondition {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {D : S.StandardFormUniversalArrowAssignment x₀} (hD : S.StandardFormUniversalSourceCondition x₀ fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) (m : ℤ) : S.StandardFormUniversalSourceCondition x₀ fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => normalizeAtTargetHeight S x₀ hD m

One target-height normalization preserves irreducibility and the global minimal left almost-split source invariant.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSourceCondition.normalizeAtTargetHeight_mesh_zero {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {D : S.StandardFormUniversalArrowAssignment x₀} (hD : S.StandardFormUniversalSourceCondition x₀ fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) (m : ℤ) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) (hW : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ (MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ W) = m) : CategoryTheory.CategoryStruct.comp (S.standardFormUniversalRealizedSource x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => normalizeAtTargetHeight S x₀ hD m) W) (S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => normalizeAtTargetHeight S x₀ hD m) ↑W) = 0

Every mesh at the selected translated-source height satisfies its literal zero relation after simultaneous source normalization.

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

An arrow assignment together with the global source invariant required by the descending induction.

• arrowMap : S.StandardFormUniversalArrowAssignment x₀
• sourceCondition : S.StandardFormUniversalSourceCondition x₀ fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => self.arrowMap

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

The positive limiting assignment is the initial state of the descending source induction.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSourceAssignment.normalizeAtTargetHeight {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (E : S.StandardFormUniversalSourceAssignment x₀) (m : ℤ) : S.StandardFormUniversalSourceAssignment x₀

Normalize all sources at one translated-source height while retaining the global source invariant.

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

Stage n + 1 of the descending induction normalizes translated-source height -n; stage zero is the positive limiting assignment.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNonpositiveStage_succ_arrow_eq_of_height_ne {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (n : ℕ) {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (hZ : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ Z ≠ -↑n) (a : Y ⟶ Z) : (S.standardFormUniversalNonpositiveStage x₀ (n + 1)).arrowMap a = (S.standardFormUniversalNonpositiveStage x₀ n).arrowMap a

A successor descending stage changes only arrows whose target has the newly processed height.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNonpositiveStage_arrow_eq_positive {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (r : ℕ) {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (hZ : 0 < MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ Z) (a : Y ⟶ Z) : (S.standardFormUniversalNonpositiveStage x₀ r).arrowMap a = S.standardFormUniversalPositiveArrowMap x₀ a

Positive-target arrows are never changed by the descending induction.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNonpositiveStage_arrow_stable {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (n r : ℕ) {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (hZ : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ Z = -↑n) (a : Y ⟶ Z) : (S.standardFormUniversalNonpositiveStage x₀ (n + 1 + r)).arrowMap a = (S.standardFormUniversalNonpositiveStage x₀ (n + 1)).arrowMap a

Once target height -n has been processed, all later descending stages agree on arrows with that target height.

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

The two-sided limiting assignment: nonpositive arrow targets use their stabilized descending stage; positive targets retain the positive limit.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNormalizedArrowMap_eq_stage_succ {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (n : ℕ) {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (hZ : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ Z = -↑n) (a : Y ⟶ Z) : S.standardFormUniversalNormalizedArrowMap x₀ a = (S.standardFormUniversalNonpositiveStage x₀ (n + 1)).arrowMap a

At target height -n, the two-sided limit agrees with descending stage n + 1.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNormalizedArrowMap_eq_positive {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (hZ : 0 < MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ Z) (a : Y ⟶ Z) : S.standardFormUniversalNormalizedArrowMap x₀ a = S.standardFormUniversalPositiveArrowMap x₀ a

At positive target height, the two-sided limit agrees with the positive limiting assignment.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNormalizedRealizedSource_eq_stage_succ {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (n : ℕ) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) (hW : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ (MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ W) = -↑n) : S.standardFormUniversalRealizedSource x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.standardFormUniversalNormalizedArrowMap x₀) W = S.standardFormUniversalRealizedSource x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => (S.standardFormUniversalNonpositiveStage x₀ (n + 1)).arrowMap) W

For a mesh whose translated source has height -n, its source in the two-sided limit is already its source at stage n + 1.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNormalizedRealizedSink_eq_stage_succ {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (n : ℕ) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) (hW : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ (MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ W) = -↑n) : S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.standardFormUniversalNormalizedArrowMap x₀) ↑W = S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => (S.standardFormUniversalNonpositiveStage x₀ (n + 1)).arrowMap) ↑W

For a mesh whose translated source has height -n, its sink in the two-sided limit is also already its sink at stage n + 1.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNormalized_mesh_zero_of_tau_height_eq_neg {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (n : ℕ) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) (hW : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ (MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ W) = -↑n) : CategoryTheory.CategoryStruct.comp (S.standardFormUniversalRealizedSource x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.standardFormUniversalNormalizedArrowMap x₀) W) (S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.standardFormUniversalNormalizedArrowMap x₀) ↑W) = 0

Every mesh whose translated source has height -n satisfies its literal zero relation in the two-sided limiting assignment.

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

Every representative in the two-sided limiting assignment remains irreducible.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNormalized_mesh_zero {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) : CategoryTheory.CategoryStruct.comp (S.standardFormUniversalRealizedSource x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.standardFormUniversalNormalizedArrowMap x₀) W) (S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.standardFormUniversalNormalizedArrowMap x₀) ↑W) = 0

Every lifted mesh satisfies its literal zero relation in the two-sided limiting assignment.