Riedtmann covering theorem for the normalized universal realization

This file implements the radical-layer argument of Riedtmann, Proposition 2.3, for the normalized standard-form universal mesh functor. The right almost-split half first approximates every fixed-target morphism by lifted mesh paths modulo successive powers of the categorical radical.

@[instance_reducible]

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

@[instance_reducible]

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalCoveringArrowFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : Fin S.n) : Fintype (x ⟶ y)

@[instance_reducible]

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalCoveringStarFintype {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) : Fintype (Quiver.Star W)

@[instance_reducible]

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalCoveringCostarFintype {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) : Fintype (Quiver.Costar W)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormResidueRemainder_not_isSplitEpi {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) (f : S.fgObj x ⟶ S.fgObj x) : have r := (FiniteTauMatrix.algebraicallyClosedResidueMap S.finiteTauCategoryData.toFiniteRightTauCategoryData x) f; ¬CategoryTheory.IsSplitEpi (f - r • CategoryTheory.CategoryStruct.id (S.fgObj x))

The scalar residue remainder of an endomorphism of a chosen indecomposable is radical, hence is not split epic.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormResidueRemainder_not_isSplitMono {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) (f : S.fgObj x ⟶ S.fgObj x) : have r := (FiniteTauMatrix.algebraicallyClosedResidueMap S.finiteTauCategoryData.toFiniteRightTauCategoryData x) f; ¬CategoryTheory.IsSplitMono (f - r • CategoryTheory.CategoryStruct.id (S.fgObj x))

The scalar residue remainder of an indecomposable endomorphism is also not split monic.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.not_isSplitEpi_fgObj_of_ne {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} (hxy : x ≠ y) (f : S.fgObj x ⟶ S.fgObj y) : ¬CategoryTheory.IsSplitEpi f

A morphism between two differently labelled chosen indecomposables is not split epic.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.not_isSplitMono_fgObj_of_ne {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} (hxy : x ≠ y) (f : S.fgObj x ⟶ S.fgObj y) : ¬CategoryTheory.IsSplitMono f

A morphism between two differently labelled chosen indecomposables is not split monic.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMeshObj {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) : MeshCategory.RawCategory (MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀)

A universal-cover vertex as an object of its raw mesh category.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalIndecMeshFunctor_obj_meshObj {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) : (S.standardFormUniversalIndecMeshFunctor x₀).obj (S.standardFormUniversalMeshObj x₀ W) = W.fst

The skeletal realization sends the mesh object represented by W to its base label.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalTargetFiberDiagonal {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (X : S.FGIndecCategory) (r : k) : DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => S.standardFormUniversalMeshObj x₀ W ⟶ ↑Z

The possible degree-zero contribution in a fixed-source target fibre. It is supported at the source vertex itself when its base label is the fixed downstairs target, and is zero otherwise.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalTargetFiberDiagonal_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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (X : S.FGIndecCategory) : S.standardFormUniversalTargetFiberDiagonal x₀ W X 0 = 0

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalTargetFiberDiagonal_add {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (X : S.FGIndecCategory) (r s : k) : S.standardFormUniversalTargetFiberDiagonal x₀ W X (r + s) = S.standardFormUniversalTargetFiberDiagonal x₀ W X r + S.standardFormUniversalTargetFiberDiagonal x₀ W X s

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_targetFiberHomMap_diagonal_self {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (r : k) : (LinearCovering.targetFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) (S.standardFormUniversalMeshObj x₀ W) W.fst) (S.standardFormUniversalTargetFiberDiagonal x₀ W W.fst r) = r • CategoryTheory.CategoryStruct.id ((S.standardFormUniversalIndecMeshFunctor x₀).obj (S.standardFormUniversalMeshObj x₀ W))

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalSourceFiberDiagonal {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) (X : S.FGIndecCategory) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (r : k) : DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => ↑Z ⟶ S.standardFormUniversalMeshObj x₀ W

The possible degree-zero contribution in a fixed-target source fibre. It is supported at the target vertex itself when its base label is the fixed downstairs source, and is zero otherwise.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalSourceFiberDiagonal_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) (X : S.FGIndecCategory) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) : S.standardFormUniversalSourceFiberDiagonal x₀ X W 0 = 0

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalSourceFiberDiagonal_add {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) (X : S.FGIndecCategory) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (r s : k) : S.standardFormUniversalSourceFiberDiagonal x₀ X W (r + s) = S.standardFormUniversalSourceFiberDiagonal x₀ X W r + S.standardFormUniversalSourceFiberDiagonal x₀ X W s

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_sourceFiberHomMap_diagonal_self {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (r : k) : (LinearCovering.sourceFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) W.fst (S.standardFormUniversalMeshObj x₀ W)) (S.standardFormUniversalSourceFiberDiagonal x₀ W.fst W r) = r • CategoryTheory.CategoryStruct.id ((S.standardFormUniversalIndecMeshFunctor x₀).obj (S.standardFormUniversalMeshObj x₀ W))

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMiddleHom {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) : S.standardFormUniversalMeshObj x₀ (S.standardFormUniversalMiddleVertex x₀ W i) ⟶ S.standardFormUniversalMeshObj x₀ W

The raw mesh-category morphism represented by one displayed arrow into the lifted sink at W.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalIndecMeshFunctor_map_middleHom {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) : ((S.standardFormUniversalIndecMeshFunctor x₀).map (S.standardFormUniversalMiddleHom x₀ W i)).hom = S.standardFormUniversalNormalizedArrowMap x₀ (S.standardFormUniversalMiddleArrow x₀ W i)

The skeletal realization of the displayed raw mesh arrow is its chosen normalized irreducible module map.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMappedMiddleHom {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) : S.fgObj (FiniteTauMatrix.rightMiddleLabel S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst i) ⟶ S.fgObj W.fst

The displayed middle arrow with its literal underlying module-Hom type. This wrapper keeps object-definition transports out of additive formulas.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMappedMiddleHom_eq_normalized {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) : S.standardFormUniversalMappedMiddleHom x₀ W i = S.standardFormUniversalNormalizedArrowMap x₀ (S.standardFormUniversalMiddleArrow x₀ W i)

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalIndecMeshFunctor_map_incomingArrowHom {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (d : Quiver.Star W) : ((S.standardFormUniversalIndecMeshFunctor x₀).map ((MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀).incomingArrowHom d)).hom = S.standardFormUniversalNormalizedArrowMap x₀ d.snd

The image of an arbitrary incoming arrow is its normalized irreducible representative. This star-indexed form avoids transports through the chosen finite enumeration of the middle term.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMappedIncomingHom {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (d : Quiver.Star W) : S.fgObj d.fst.fst ⟶ S.fgObj W.fst

An arbitrary incoming arrow after realization, with its literal underlying module-Hom type.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMappedIncomingHom_eq_normalized {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (d : Quiver.Star W) : S.standardFormUniversalMappedIncomingHom x₀ W d = S.standardFormUniversalNormalizedArrowMap x₀ d.snd

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalIndecMeshFunctor_map_outgoingArrowHom {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (d : Quiver.Costar W) : ((S.standardFormUniversalIndecMeshFunctor x₀).map ((MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀).outgoingArrowHom d)).hom = S.standardFormUniversalNormalizedArrowMap x₀ d.snd

The image of an arbitrary categorical outgoing arrow is its normalized irreducible representative.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMappedOutgoingHom {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (d : Quiver.Costar W) : S.fgObj W.fst ⟶ S.fgObj d.fst.fst

An arbitrary outgoing categorical arrow after realization, with its literal underlying module-Hom type.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMappedOutgoingHom_eq_normalized {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (d : Quiver.Costar W) : S.standardFormUniversalMappedOutgoingHom x₀ W d = S.standardFormUniversalNormalizedArrowMap x₀ d.snd

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalArrowAssignment_cast_target {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₀) {Y W W' : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (h : W = W') (a : Y ⟶ W) : D (Quiver.Hom.cast ⋯ h a) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (D a)

A dependent arrow assignment applied after transporting the target of a reversed quiver arrow is transported by the corresponding object equality.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalCostarCast {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₀} (h : W = W') : Quiver.Costar W ≃ Quiver.Costar W'

Transport the distinguished source vertex of an outgoing costar.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalCostarCast_apply {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₀} (h : W = W') (d : Quiver.Costar W) : (S.standardFormUniversalCostarCast x₀ h) d = ⟨d.fst, Quiver.Hom.cast ⋯ h d.snd⟩

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMappedOutgoingHom_costarCast {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₀} (h : W = W') (d : Quiver.Costar W) : S.standardFormUniversalMappedOutgoingHom x₀ W' ((S.standardFormUniversalCostarCast x₀ h) d) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (S.standardFormUniversalMappedOutgoingHom x₀ W d)

Realization of an outgoing arrow commutes with transport of its source vertex.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.natCard_meshArrow_eq_arrowMultiplicity {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (target source : Fin S.n) : Nat.card (S.MeshArrow target source) = FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData source target

Literal right-mesh occurrences have the official finite-tau arrow multiplicity, including at the projective boundary.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.natCard_minimalLeftOccurrence_eq_standardFormArrow {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (source target : Fin S.n) : Nat.card (S.almostSplitSkeleton.LeftAROccurrence (S.minimalLeftAlmostSplitAt source) target) = Nat.card (S.StandardFormArrow target source)

The occurrences of one target in the chosen minimal left-almost-split middle term are equinumerous with the reversed standard-form arrows that represent maps from the fixed source to that target.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.minimalLeftOccurrenceEquivStandardFormArrow {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (source target : Fin S.n) : S.almostSplitSkeleton.LeftAROccurrence (S.minimalLeftAlmostSplitAt source) target ≃ S.StandardFormArrow target source

Match the chosen left-almost-split summand occurrences at source with the outgoing reversed standard-form arrows, target by target.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.minimalLeftAlmostSplitAt_label_injective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (source : Fin S.n) : Function.Injective (S.minimalLeftAlmostSplitAt source).label

Square-freeness of the standard-form quiver forces the chosen minimal left-almost-split middle decomposition to contain no repeated label.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.minimalLeftMiddleIndexEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (source : Fin S.n) : (S.minimalLeftAlmostSplitAt source).index.obj ≃ (target : Fin S.n) × S.almostSplitSkeleton.LeftAROccurrence (S.minimalLeftAlmostSplitAt source) target

Regroup the indices of the chosen minimal left-almost-split middle term by their target labels.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.minimalLeftMiddleCostarEquiv {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (source : Fin S.n) : (S.minimalLeftAlmostSplitAt source).index.obj ≃ Quiver.Costar source

The chosen left-almost-split middle indices are the categorical outgoing costar of the corresponding base standard-form vertex.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.minimalLeftMiddleCostarEquiv_fst {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (source : Fin S.n) (t : (S.minimalLeftAlmostSplitAt source).index.obj) : ((S.minimalLeftMiddleCostarEquiv source) t).fst = (S.minimalLeftAlmostSplitAt source).label t

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalLeftMiddleCostarEquiv {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) : (S.minimalLeftAlmostSplitAt W.fst).index.obj ≃ Quiver.Costar W

Lift the left-almost-split middle indices uniquely to the outgoing costar of a selected universal-cover vertex.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalLeftMiddleCostarEquiv_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) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (t : (S.minimalLeftAlmostSplitAt W.fst).index.obj) : (MeshCategory.RightMeshData.UniversalCover.projection S.standardFormRightMeshData x₀).costar W ((S.standardFormUniversalLeftMiddleCostarEquiv x₀ W) t) = (S.minimalLeftMiddleCostarEquiv W.fst) t

Projecting the lifted outgoing arrow attached to a left-middle index recovers its base costar arrow.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalLeftMiddleCostarEquiv_target_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) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (t : (S.minimalLeftAlmostSplitAt W.fst).index.obj) : ((S.standardFormUniversalLeftMiddleCostarEquiv x₀ W) t).fst.fst = (S.minimalLeftAlmostSplitAt W.fst).label t

The base label of the lifted outgoing target is the label of its chosen left-almost-split summand.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizedOutgoingSource {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) : S.fgObj W.fst ⟶ (S.minimalLeftAlmostSplitAt W.fst).middle

Reassemble all realized outgoing arrows at W into the chosen minimal left-almost-split middle term at its base label.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizedOutgoingSource_decomposition_π {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (t : (S.minimalLeftAlmostSplitAt W.fst).index.obj) : CategoryTheory.CategoryStruct.comp (S.standardFormUniversalRealizedOutgoingSource x₀ W) (CategoryTheory.CategoryStruct.comp (S.minimalLeftAlmostSplitAt W.fst).decomposition.hom (CategoryTheory.Limits.biproduct.π (fun (j : (S.minimalLeftAlmostSplitAt W.fst).index.obj) => S.fgObj ((S.minimalLeftAlmostSplitAt W.fst).label j)) t)) = CategoryTheory.CategoryStruct.comp (S.standardFormUniversalMappedOutgoingHom x₀ W ((S.standardFormUniversalLeftMiddleCostarEquiv x₀ W) t)) (CategoryTheory.eqToHom ⋯)

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizedOutgoingSource_decomposition_π_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) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (t : (S.minimalLeftAlmostSplitAt W.fst).index.obj) {Z : FinitelyGeneratedCategory A} (h : S.fgObj ((S.minimalLeftAlmostSplitAt W.fst).label t) ⟶ Z) : CategoryTheory.CategoryStruct.comp (S.standardFormUniversalRealizedOutgoingSource x₀ W) (CategoryTheory.CategoryStruct.comp (S.minimalLeftAlmostSplitAt W.fst).decomposition.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun (j : (S.minimalLeftAlmostSplitAt W.fst).index.obj) => S.fgObj ((S.minimalLeftAlmostSplitAt W.fst).label j)) t) h)) = CategoryTheory.CategoryStruct.comp (S.standardFormUniversalMappedOutgoingHom x₀ W ((S.standardFormUniversalLeftMiddleCostarEquiv x₀ W) t)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizedOutgoingSource_component_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) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (t : (S.minimalLeftAlmostSplitAt W.fst).index.obj) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (CategoryTheory.CategoryStruct.comp (S.standardFormUniversalRealizedOutgoingSource x₀ W) (CategoryTheory.CategoryStruct.comp (S.minimalLeftAlmostSplitAt W.fst).decomposition.hom (CategoryTheory.Limits.biproduct.π (fun (j : (S.minimalLeftAlmostSplitAt W.fst).index.obj) => S.fgObj ((S.minimalLeftAlmostSplitAt W.fst).label j)) t)))

Every chosen-summand component of the reassembled outgoing source is irreducible.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_minimalLeftAlmostSplitAt_iso_realizedOutgoingSource {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) : ∃ (e : (S.minimalLeftAlmostSplitAt W.fst).middle ≅ (S.minimalLeftAlmostSplitAt W.fst).middle), CategoryTheory.CategoryStruct.comp (S.minimalLeftAlmostSplitAt W.fst).map e.hom = S.standardFormUniversalRealizedOutgoingSource x₀ W

The source assembled from every outgoing universal-cover arrow differs from the chosen minimal left-almost-split map by an automorphism of its middle term. This includes injective source vertices.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizedOutgoingSourceIso {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) : (S.minimalLeftAlmostSplitAt W.fst).middle ≅ (S.minimalLeftAlmostSplitAt W.fst).middle

The comparison automorphism between the chosen left-almost-split source and the outgoing source assembled from the normalized realization.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.minimalLeftAlmostSplitAt_comp_realizedOutgoingSourceIso {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) : CategoryTheory.CategoryStruct.comp (S.minimalLeftAlmostSplitAt W.fst).map (S.standardFormUniversalRealizedOutgoingSourceIso x₀ W).hom = S.standardFormUniversalRealizedOutgoingSource x₀ W

The chosen left-almost-split map followed by the comparison automorphism is the reassembled outgoing source.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizedOutgoingSource_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) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit (S.standardFormUniversalRealizedOutgoingSource x₀ W)

The outgoing source assembled from the normalized universal realization is left almost split at every vertex, including injective vertices.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizedOutgoingSource_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) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) : QuotientSubmoduleEquidistribution.IsLeftMinimal (S.standardFormUniversalRealizedOutgoingSource x₀ W)

The outgoing source assembled from the normalized universal realization is left minimal at every vertex.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizedOutgoingSource_mono_of_not_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) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (hW : ¬CategoryTheory.Injective (S.fgObj W.fst)) : CategoryTheory.Mono (S.standardFormUniversalRealizedOutgoingSource x₀ W)

At a noninjective lifted vertex, the source assembled from all outgoing normalized arrows is monic. Under the comparison automorphism it is the chosen left almost-split monomorphism at the underlying indecomposable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.eq_zero_of_comp_standardFormUniversalMappedOutgoingHom_of_not_injective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ X : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (hW : ¬CategoryTheory.Injective (S.fgObj W.fst)) (q : S.fgObj X ⟶ S.fgObj W.fst) (hq : ∀ (d : Quiver.Costar W), CategoryTheory.CategoryStruct.comp q (S.standardFormUniversalMappedOutgoingHom x₀ W d) = 0) : q = 0

At a noninjective lifted vertex, the normalized outgoing arrows jointly detect morphisms into that vertex.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_factor_realizedOutgoingSource_eq_sum {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (X : Fin S.n) (h : (S.minimalLeftAlmostSplitAt W.fst).middle ⟶ S.fgObj X) : CategoryTheory.CategoryStruct.comp (S.standardFormUniversalRealizedOutgoingSource x₀ W) h = ∑ t : (S.minimalLeftAlmostSplitAt W.fst).index.obj, CategoryTheory.CategoryStruct.comp (S.standardFormUniversalMappedOutgoingHom x₀ W ((S.standardFormUniversalLeftMiddleCostarEquiv x₀ W) t)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (j : (S.minimalLeftAlmostSplitAt W.fst).index.obj) => S.fgObj ((S.minimalLeftAlmostSplitAt W.fst).label j)) t) (CategoryTheory.CategoryStruct.comp (S.minimalLeftAlmostSplitAt W.fst).decomposition.inv h)))

Expanding the chosen left-middle biproduct writes a factor through the reassembled outgoing source as the sum of its lifted-arrow components.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_endomorphism_eq_scalar_add_outgoing_sum {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (f : S.fgObj W.fst ⟶ S.fgObj W.fst) : ∃ (r : k) (g : (t : (S.minimalLeftAlmostSplitAt W.fst).index.obj) → S.fgObj ((S.standardFormUniversalLeftMiddleCostarEquiv x₀ W) t).fst.fst ⟶ S.fgObj W.fst), f = r • CategoryTheory.CategoryStruct.id (S.fgObj W.fst) + ∑ t : (S.minimalLeftAlmostSplitAt W.fst).index.obj, CategoryTheory.CategoryStruct.comp (S.standardFormUniversalMappedOutgoingHom x₀ W ((S.standardFormUniversalLeftMiddleCostarEquiv x₀ W) t)) (g t)

Remove the scalar residue of an endomorphism and factor the radical remainder through all normalized outgoing arrows.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_morphism_eq_outgoing_sum_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) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) {X : Fin S.n} (hWX : W.fst ≠ X) (f : S.fgObj W.fst ⟶ S.fgObj X) : ∃ (g : (t : (S.minimalLeftAlmostSplitAt W.fst).index.obj) → S.fgObj ((S.standardFormUniversalLeftMiddleCostarEquiv x₀ W) t).fst.fst ⟶ S.fgObj X), f = ∑ t : (S.minimalLeftAlmostSplitAt W.fst).index.obj, CategoryTheory.CategoryStruct.comp (S.standardFormUniversalMappedOutgoingHom x₀ W ((S.standardFormUniversalLeftMiddleCostarEquiv x₀ W) t)) (g t)

A morphism to a differently labelled indecomposable factors through all normalized outgoing arrows at its source.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_oneStep_targetFiber {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (X : S.FGIndecCategory) (f : S.fgObj W.fst ⟶ S.fgObj X) : ∃ (a : DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => S.standardFormUniversalMeshObj x₀ W ⟶ ↑Z) (g : (t : (S.minimalLeftAlmostSplitAt W.fst).index.obj) → S.fgObj ((S.standardFormUniversalLeftMiddleCostarEquiv x₀ W) t).fst.fst ⟶ S.fgObj X), CategoryTheory.InducedCategory.homMk f = (LinearCovering.targetFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) (S.standardFormUniversalMeshObj x₀ W) X) a + CategoryTheory.InducedCategory.homMk (∑ t : (S.minimalLeftAlmostSplitAt W.fst).index.obj, CategoryTheory.CategoryStruct.comp (S.standardFormUniversalMappedOutgoingHom x₀ W ((S.standardFormUniversalLeftMiddleCostarEquiv x₀ W) t)) (g t))

The fixed-source Riedtmann one-step decomposition, with the scalar identity term already bundled as a target-fibre contribution.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNormalizedOutgoingArrow_mem_radical {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (d : Quiver.Costar W) : S.standardFormUniversalMappedOutgoingHom x₀ W d ∈ S.fgNilpotentRadicalData.ideal.hom (S.fgObj W.fst) (S.fgObj d.fst.fst)

Every outgoing arrow of the normalized universal realization belongs to the categorical radical ideal.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_exists_targetFiber_mod_radicalPower {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) (X : S.FGIndecCategory) (n : ℕ) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (f : S.fgObj W.fst ⟶ S.fgObj X) : ∃ (a : DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => S.standardFormUniversalMeshObj x₀ W ⟶ ↑Z), (CategoryTheory.InducedCategory.homMk f - (LinearCovering.targetFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) (S.standardFormUniversalMeshObj x₀ W) X) a).hom ∈ (S.fgNilpotentRadicalData.ideal.pow n).hom (S.fgObj W.fst) (S.fgObj X)

Riedtmann's fixed-source approximation: modulo the n-th radical power, every module morphism is the image of a finite target-fibre sum of raw mesh morphisms.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_targetFiberHomMap_surjective_meshObj {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (X : S.FGIndecCategory) : Function.Surjective ⇑(LinearCovering.targetFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) (S.standardFormUniversalMeshObj x₀ W) X)

Nilpotence terminates the fixed-source radical approximation, giving exact surjectivity of the target-fibre map at every represented source.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_exists_targetFiber_eq_diagonal_add_outgoing {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (X : S.FGIndecCategory) (a : DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => S.standardFormUniversalMeshObj x₀ W ⟶ ↑Z) : ∃ (r : k) (b : (d : Quiver.Costar W) → DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => S.standardFormUniversalMeshObj x₀ d.fst ⟶ ↑Z), a = S.standardFormUniversalTargetFiberDiagonal x₀ W X r + ∑ d : Quiver.Costar W, (LinearCovering.targetFiberPrecomp (S.standardFormUniversalIndecMeshFunctor x₀) X ((MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀).outgoingArrowHom d)) (b d)

Every fixed-source target-fibre family is a possible scalar at the source vertex plus families precomposed with the arrows leaving that vertex. This is the direct-sum form of decomposition by the first arrow.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNoninjectiveMeshBase {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (hW : ¬CategoryTheory.Injective (S.fgObj W.fst)) : { z : Fin S.n // z ∉ S.standardFormRightMeshData.projective }

The downstairs nonprojective endpoint whose translate is a selected noninjective standard-form label.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNoninjectiveMeshBase_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) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (hW : ¬CategoryTheory.Injective (S.fgObj W.fst)) : S.standardFormRightMeshData.tau (S.standardFormUniversalNoninjectiveMeshBase x₀ W hW) = W.fst

The recovered downstairs mesh endpoint translates to the base label of the selected noninjective lifted vertex.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNoninjectiveMeshEndpoint {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (hW : ¬CategoryTheory.Injective (S.fgObj W.fst)) : { Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // Z ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }

Reverse the formal mesh edge at a noninjective lifted vertex. The result is the unique lifted nonprojective mesh endpoint whose translate is the original vertex.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNoninjectiveMeshEndpoint_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) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (hW : ¬CategoryTheory.Injective (S.fgObj W.fst)) : MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ (S.standardFormUniversalNoninjectiveMeshEndpoint x₀ W hW) = W

Translating the endpoint obtained by reversing the formal mesh edge recovers the original noninjective lifted vertex.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalPairedIncomingHom {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₀ }) (d : Quiver.Star ↑W) : S.standardFormUniversalMeshObj x₀ (MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ W) ⟶ S.standardFormUniversalMeshObj x₀ d.fst

The raw mesh morphism represented by the polarized partner of an arbitrary incoming arrow at a nonprojective lifted vertex.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMappedPairedIncomingHom {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₀ }) (d : Quiver.Star ↑W) : S.fgObj (S.standardFormTau (MeshCategory.RightMeshData.UniversalCover.baseNonprojective S.standardFormRightMeshData x₀ W)) ⟶ S.fgObj d.fst.fst

A polarized partner of an arbitrary incoming arrow after realization, with its literal underlying module-Hom type.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMappedPairedIncomingHom_eq_normalized {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₀ }) (d : Quiver.Star ↑W) : S.standardFormUniversalMappedPairedIncomingHom x₀ W d = S.standardFormUniversalNormalizedArrowMap x₀ (((MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀).arrowEquiv W d.fst) d.snd)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_paired_sourceFiber_sum_eq_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) (X : S.FGIndecCategory) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) (q : DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => ↑Z ⟶ S.standardFormUniversalMeshObj x₀ (MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ W)) : ∑ d : Quiver.Star ↑W, (LinearCovering.sourceFiberPostcomp (S.standardFormUniversalIndecMeshFunctor x₀) X ((MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀).incomingArrowHom d)) ((LinearCovering.sourceFiberPostcomp (S.standardFormUniversalIndecMeshFunctor x₀) X (S.standardFormUniversalPairedIncomingHom x₀ W d)) q) = 0

The ordinary mesh relation remains zero after applying it coefficientwise to an entire fixed-target source fibre.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_paired_targetFiber_sum_eq_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) (X : S.FGIndecCategory) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) (q : DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => S.standardFormUniversalMeshObj x₀ ↑W ⟶ ↑Z) : ∑ d : Quiver.Star ↑W, (LinearCovering.targetFiberPrecomp (S.standardFormUniversalIndecMeshFunctor x₀) X (S.standardFormUniversalPairedIncomingHom x₀ W d)) ((LinearCovering.targetFiberPrecomp (S.standardFormUniversalIndecMeshFunctor x₀) X ((MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀).incomingArrowHom d)) q) = 0

The ordinary mesh relation remains zero after applying it coefficientwise to an entire fixed-source target fibre.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNormalizedIncomingArrow_mem_radical {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (d : Quiver.Star W) : S.standardFormUniversalNormalizedArrowMap x₀ d.snd ∈ S.fgNilpotentRadicalData.ideal.hom (S.fgObj d.fst.fst) (S.fgObj W.fst)

Every incoming arrow of the universal mesh has radical image, without choosing a displayed middle-term index.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_exists_sourceFiber_eq_diagonal_add_incoming {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) (X : S.FGIndecCategory) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (a : DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => ↑Z ⟶ S.standardFormUniversalMeshObj x₀ W) : ∃ (r : k) (b : (d : Quiver.Star W) → DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => ↑Z ⟶ S.standardFormUniversalMeshObj x₀ d.fst), a = S.standardFormUniversalSourceFiberDiagonal x₀ X W r + ∑ d : Quiver.Star W, (LinearCovering.sourceFiberPostcomp (S.standardFormUniversalIndecMeshFunctor x₀) X ((MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀).incomingArrowHom d)) (b d)

Every fixed-target source-fibre family is a possible scalar at the target vertex plus families postcomposed with the arrows entering that vertex. This is the direct-sum form of decomposition by the final arrow.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNormalizedMiddleArrow_mem_radical {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) : S.standardFormUniversalNormalizedArrowMap x₀ (S.standardFormUniversalMiddleArrow x₀ W i) ∈ S.fgNilpotentRadicalData.ideal.hom (S.fgObj (FiniteTauMatrix.rightMiddleLabel S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst i)) (S.fgObj W.fst)

Every displayed normalized arrow lies in the categorical radical ideal of the representation-finite module category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNormalizedRealizedSource_factors_of_comp_sink_eq_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₀ }) {X : FGModuleCat Aᵐᵒᵖ} (q : X ⟶ (S.finiteTauCategoryData.rightMesh (S.fgObj (↑W).fst)).X₂) (hq : CategoryTheory.CategoryStruct.comp q (S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.standardFormUniversalNormalizedArrowMap x₀) ↑W) = 0) : ∃ (t : X ⟶ S.fgObj (S.standardFormTau (MeshCategory.RightMeshData.UniversalCover.baseNonprojective S.standardFormRightMeshData x₀ W))), CategoryTheory.CategoryStruct.comp t (S.standardFormUniversalRealizedSource x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.standardFormUniversalNormalizedArrowMap x₀) W) = q

At a nonprojective lifted vertex, the normalized mesh source is a weak kernel of the normalized mesh sink. This is the local exactness statement used to peel a relation one mesh layer farther from its endpoint.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNormalizedRealizedSink_factors_of_source_comp_eq_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₀ }) {X : FGModuleCat Aᵐᵒᵖ} (q : (S.finiteTauCategoryData.rightMesh (S.fgObj (↑W).fst)).X₂ ⟶ X) (hq : CategoryTheory.CategoryStruct.comp (S.standardFormUniversalRealizedSource x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.standardFormUniversalNormalizedArrowMap x₀) W) q = 0) : ∃ (t : S.fgObj (↑W).fst ⟶ X), CategoryTheory.CategoryStruct.comp (S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.standardFormUniversalNormalizedArrowMap x₀) ↑W) t = q

At a nonprojective lifted vertex, the normalized mesh sink is a weak cokernel of the normalized mesh source. This is the target-side local exactness statement used to peel a relation one mesh layer farther from its source.

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

Expanding through the displayed middle biproduct writes a factor through the normalized realized sink as the finite sum of its arrow components.

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

Assemble the displayed incoming coefficients into the chosen middle term of the almost-split sink at W.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalIncomingMiddleLift_projection {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ X : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (c : (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) → S.fgObj X ⟶ S.fgObj (FiniteTauMatrix.rightMiddleLabel S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst i)) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) : CategoryTheory.CategoryStruct.comp (S.standardFormUniversalIncomingMiddleLift x₀ X W c) (FiniteTauMatrix.rightMiddleProjection S.finiteTauCategoryData W.fst i) = c i

A component of the assembled incoming middle map is its displayed coefficient.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalIncomingMiddleLift_projection_assoc {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ X : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (c : (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) → S.fgObj X ⟶ S.fgObj (FiniteTauMatrix.rightMiddleLabel S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst i)) (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.standardFormUniversalIncomingMiddleLift x₀ X W c) (CategoryTheory.CategoryStruct.comp (FiniteTauMatrix.rightMiddleProjection S.finiteTauCategoryData W.fst i) h) = CategoryTheory.CategoryStruct.comp (c i) h

A component of the assembled incoming middle map is its displayed coefficient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalIncomingMiddleLift_comp_sink {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ X : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (c : (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) → S.fgObj X ⟶ S.fgObj (FiniteTauMatrix.rightMiddleLabel S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst i)) : CategoryTheory.CategoryStruct.comp (S.standardFormUniversalIncomingMiddleLift x₀ X W c) (S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.standardFormUniversalNormalizedArrowMap x₀) W) = ∑ i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst), CategoryTheory.CategoryStruct.comp (c i) (S.standardFormUniversalNormalizedArrowMap x₀ (S.standardFormUniversalMiddleArrow x₀ W i))

Composing the assembled middle map with the normalized sink is the sum of its displayed incoming-arrow composites.

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

Assemble maps out of the displayed middle summands into a map from the chosen right-mesh middle term.

@[simp]

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

Restricting the assembled outgoing middle map to a displayed summand recovers its coefficient.

@[simp]

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

Restricting the assembled outgoing middle map to a displayed summand recovers its coefficient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizedSource_comp_outgoingMiddleDesc {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ X : Fin S.n) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) (c : (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData (↑W).fst)) → S.fgObj (FiniteTauMatrix.rightMiddleLabel S.finiteTauCategoryData.toFiniteRightTauCategoryData (↑W).fst i) ⟶ S.fgObj X) : CategoryTheory.CategoryStruct.comp (S.standardFormUniversalRealizedSource x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.standardFormUniversalNormalizedArrowMap x₀) W) (S.standardFormUniversalOutgoingMiddleDesc x₀ X (↑W) c) = ∑ i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData (↑W).fst), CategoryTheory.CategoryStruct.comp (S.standardFormUniversalNormalizedArrowMap x₀ (S.standardFormUniversalPairedMiddleArrow x₀ W i)) (c i)

Composing the normalized mesh source with an assembled outgoing middle map is the sum of the polarized-arrow composites.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_nonprojective_outgoing_exact {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ X : Fin S.n) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) (c : (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData (↑W).fst)) → S.fgObj (FiniteTauMatrix.rightMiddleLabel S.finiteTauCategoryData.toFiniteRightTauCategoryData (↑W).fst i) ⟶ S.fgObj X) (hc : ∑ i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData (↑W).fst), CategoryTheory.CategoryStruct.comp (S.standardFormUniversalNormalizedArrowMap x₀ (S.standardFormUniversalPairedMiddleArrow x₀ W i)) (c i) = 0) : ∃ (t : S.fgObj (↑W).fst ⟶ S.fgObj X), ∀ (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData (↑W).fst)), c i = CategoryTheory.CategoryStruct.comp (S.standardFormUniversalNormalizedArrowMap x₀ (S.standardFormUniversalMiddleArrow x₀ (↑W) i)) t

At a nonprojective lifted endpoint, every relation among the normalized polarized arrows leaving its translate is generated by the arrows entering the endpoint.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_nonprojective_outgoingStar_exact {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ X : Fin S.n) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) (c : (d : Quiver.Star ↑W) → S.fgObj d.fst.fst ⟶ S.fgObj X) (hc : ∑ d : Quiver.Star ↑W, CategoryTheory.CategoryStruct.comp (S.standardFormUniversalMappedPairedIncomingHom x₀ W d) (c d) = 0) : ∃ (t : S.fgObj (↑W).fst ⟶ S.fgObj X), ∀ (d : Quiver.Star ↑W), c d = CategoryTheory.CategoryStruct.comp (S.standardFormUniversalMappedIncomingHom x₀ (↑W) d) t

Nonprojective outgoing exactness in the star coordinates at the mesh endpoint: a relation among polarized partners factors through the incoming arrows.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMeshStarCostarEquiv {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₀ }) : Quiver.Star ↑W ≃ Quiver.Costar (MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ W)

Polarization identifies the incoming star of a nonprojective mesh endpoint with the outgoing costar of its translated source.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMeshStarCostarEquiv_apply {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₀ }) (d : Quiver.Star ↑W) : (S.standardFormUniversalMeshStarCostarEquiv x₀ W) d = ⟨d.fst, ((MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀).arrowEquiv W d.fst) d.snd⟩

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMappedOutgoingHom_meshStarCostarEquiv {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₀ }) (d : Quiver.Star ↑W) : S.standardFormUniversalMappedOutgoingHom x₀ (MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ W) ((S.standardFormUniversalMeshStarCostarEquiv x₀ W) d) = S.standardFormUniversalMappedPairedIncomingHom x₀ W d

The costar arrow obtained by polarization realizes the same normalized map as the corresponding paired incoming arrow.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_nonprojective_translatedCostar_exact {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ X : Fin S.n) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) (c : (d : Quiver.Costar (MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ W)) → S.fgObj d.fst.fst ⟶ S.fgObj X) (hc : ∑ d : Quiver.Costar (MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ W), CategoryTheory.CategoryStruct.comp (S.standardFormUniversalMappedOutgoingHom x₀ (MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ W) d) (c d) = 0) : ∃ (t : S.fgObj (↑W).fst ⟶ S.fgObj X), ∀ (d : Quiver.Star ↑W), c ((S.standardFormUniversalMeshStarCostarEquiv x₀ W) d) = CategoryTheory.CategoryStruct.comp (S.standardFormUniversalMappedIncomingHom x₀ (↑W) d) t

A vanishing family after all arrows leaving a translated mesh source is obtained by postcomposing the arrows entering the mesh endpoint.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNoninjectiveOutgoingCostarEquiv {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (hW : ¬CategoryTheory.Injective (S.fgObj W.fst)) : Quiver.Star ↑(S.standardFormUniversalNoninjectiveMeshEndpoint x₀ W hW) ≃ Quiver.Costar W

For a noninjective lifted source, its outgoing costar is parametrized by the incoming star of the canonical mesh endpoint whose translate is that source.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNoninjectiveOutgoingCostarEquiv_fst {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (hW : ¬CategoryTheory.Injective (S.fgObj W.fst)) (d : Quiver.Star ↑(S.standardFormUniversalNoninjectiveMeshEndpoint x₀ W hW)) : ((S.standardFormUniversalNoninjectiveOutgoingCostarEquiv x₀ W hW) d).fst = d.fst

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNoninjectiveIncomingCostarArrow {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (hW : ¬CategoryTheory.Injective (S.fgObj W.fst)) (d : Quiver.Costar W) : Quiver.Star ↑(S.standardFormUniversalNoninjectiveMeshEndpoint x₀ W hW)

The incoming star arrow associated with an outgoing costar at a noninjective source.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNoninjectiveIncomingCostarArrow_apply {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (hW : ¬CategoryTheory.Injective (S.fgObj W.fst)) (d : Quiver.Star ↑(S.standardFormUniversalNoninjectiveMeshEndpoint x₀ W hW)) : S.standardFormUniversalNoninjectiveIncomingCostarArrow x₀ W hW ((S.standardFormUniversalNoninjectiveOutgoingCostarEquiv x₀ W hW) d) = d

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNoninjectiveIncomingCostarHom {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (hW : ¬CategoryTheory.Injective (S.fgObj W.fst)) (d : Quiver.Costar W) : S.standardFormUniversalMeshObj x₀ d.fst ⟶ S.standardFormUniversalMeshObj x₀ ↑(S.standardFormUniversalNoninjectiveMeshEndpoint x₀ W hW)

The incoming arrow associated with an outgoing costar at a noninjective source, with its source definitionally equal to the costar endpoint.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNoninjectiveIncomingCostarHom_apply {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (hW : ¬CategoryTheory.Injective (S.fgObj W.fst)) (d : Quiver.Star ↑(S.standardFormUniversalNoninjectiveMeshEndpoint x₀ W hW)) : S.standardFormUniversalNoninjectiveIncomingCostarHom x₀ W hW ((S.standardFormUniversalNoninjectiveOutgoingCostarEquiv x₀ W hW) d) = (MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀).incomingArrowHom d

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_noninjective_outgoingCostar_exact {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ X : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (hW : ¬CategoryTheory.Injective (S.fgObj W.fst)) (c : (d : Quiver.Costar W) → S.fgObj d.fst.fst ⟶ S.fgObj X) (hc : ∑ d : Quiver.Costar W, CategoryTheory.CategoryStruct.comp (S.standardFormUniversalMappedOutgoingHom x₀ W d) (c d) = 0) : ∃ (t : S.fgObj (↑(S.standardFormUniversalNoninjectiveMeshEndpoint x₀ W hW)).fst ⟶ S.fgObj X), ∀ (d : Quiver.Star ↑(S.standardFormUniversalNoninjectiveMeshEndpoint x₀ W hW)), c ((S.standardFormUniversalNoninjectiveOutgoingCostarEquiv x₀ W hW) d) = CategoryTheory.CategoryStruct.comp (S.standardFormUniversalMappedIncomingHom x₀ (↑(S.standardFormUniversalNoninjectiveMeshEndpoint x₀ W hW)) d) t

At a noninjective lifted source, a vanishing outgoing costar family is obtained by postcomposing the incoming arrows at its canonical mesh endpoint.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_noninjective_paired_targetFiber_sum_eq_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) (X : S.FGIndecCategory) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (hW : ¬CategoryTheory.Injective (S.fgObj W.fst)) (q : DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => S.standardFormUniversalMeshObj x₀ ↑(S.standardFormUniversalNoninjectiveMeshEndpoint x₀ W hW) ⟶ ↑Z) : ∑ d : Quiver.Star ↑(S.standardFormUniversalNoninjectiveMeshEndpoint x₀ W hW), (LinearCovering.targetFiberPrecomp (S.standardFormUniversalIndecMeshFunctor x₀) X ((MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀).outgoingArrowHom ((S.standardFormUniversalNoninjectiveOutgoingCostarEquiv x₀ W hW) d))) ((LinearCovering.targetFiberPrecomp (S.standardFormUniversalIndecMeshFunctor x₀) X ((MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀).incomingArrowHom d)) q) = 0

The mesh relation at the canonical endpoint of a noninjective source, transported to that literal source vertex, vanishes coefficientwise in the target fibre.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalLeftOutgoingMiddleDesc {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ X : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (c : (t : (S.minimalLeftAlmostSplitAt W.fst).index.obj) → S.fgObj ((S.minimalLeftAlmostSplitAt W.fst).label t) ⟶ S.fgObj X) : (S.minimalLeftAlmostSplitAt W.fst).middle ⟶ S.fgObj X

Assemble maps from the chosen minimal left-almost-split summands into a map out of its middle term.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalLeftOutgoingMiddleDesc_component {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ X : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (c : (t : (S.minimalLeftAlmostSplitAt W.fst).index.obj) → S.fgObj ((S.minimalLeftAlmostSplitAt W.fst).label t) ⟶ S.fgObj X) (t : (S.minimalLeftAlmostSplitAt W.fst).index.obj) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (j : (S.minimalLeftAlmostSplitAt W.fst).index.obj) => S.fgObj ((S.minimalLeftAlmostSplitAt W.fst).label j)) t) (CategoryTheory.CategoryStruct.comp (S.minimalLeftAlmostSplitAt W.fst).decomposition.inv (S.standardFormUniversalLeftOutgoingMiddleDesc x₀ X W c)) = c t

A displayed summand of the assembled left-middle map is its prescribed coefficient.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalLeftOutgoingMiddleDesc_component_assoc {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ X : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (c : (t : (S.minimalLeftAlmostSplitAt W.fst).index.obj) → S.fgObj ((S.minimalLeftAlmostSplitAt W.fst).label t) ⟶ S.fgObj X) (t : (S.minimalLeftAlmostSplitAt W.fst).index.obj) {Z : FinitelyGeneratedCategory A} (h : S.fgObj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (j : (S.minimalLeftAlmostSplitAt W.fst).index.obj) => S.fgObj ((S.minimalLeftAlmostSplitAt W.fst).label j)) t) (CategoryTheory.CategoryStruct.comp (S.minimalLeftAlmostSplitAt W.fst).decomposition.inv (CategoryTheory.CategoryStruct.comp (S.standardFormUniversalLeftOutgoingMiddleDesc x₀ X W c) h)) = CategoryTheory.CategoryStruct.comp (c t) h

A displayed summand of the assembled left-middle map is its prescribed coefficient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizedOutgoingSource_comp_leftOutgoingMiddleDesc {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ X : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (c : (t : (S.minimalLeftAlmostSplitAt W.fst).index.obj) → S.fgObj ((S.minimalLeftAlmostSplitAt W.fst).label t) ⟶ S.fgObj X) : CategoryTheory.CategoryStruct.comp (S.standardFormUniversalRealizedOutgoingSource x₀ W) (S.standardFormUniversalLeftOutgoingMiddleDesc x₀ X W c) = ∑ t : (S.minimalLeftAlmostSplitAt W.fst).index.obj, CategoryTheory.CategoryStruct.comp (S.standardFormUniversalMappedOutgoingHom x₀ W ((S.standardFormUniversalLeftMiddleCostarEquiv x₀ W) t)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (c t))

Composing the realized outgoing source with an assembled left-middle map is the corresponding finite costar sum.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_injective_outgoing_exact {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ X : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (hW : CategoryTheory.Injective (S.fgObj W.fst)) (c : (t : (S.minimalLeftAlmostSplitAt W.fst).index.obj) → S.fgObj ((S.minimalLeftAlmostSplitAt W.fst).label t) ⟶ S.fgObj X) (hc : ∑ t : (S.minimalLeftAlmostSplitAt W.fst).index.obj, CategoryTheory.CategoryStruct.comp (S.standardFormUniversalMappedOutgoingHom x₀ W ((S.standardFormUniversalLeftMiddleCostarEquiv x₀ W) t)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (c t)) = 0) (t : (S.minimalLeftAlmostSplitAt W.fst).index.obj) : c t = 0

At an injective source, a relation among the chosen outgoing summands has every coefficient zero.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_injective_outgoingCostar_exact {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ X : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (hW : CategoryTheory.Injective (S.fgObj W.fst)) (c : (d : Quiver.Costar W) → S.fgObj d.fst.fst ⟶ S.fgObj X) (hc : ∑ d : Quiver.Costar W, CategoryTheory.CategoryStruct.comp (S.standardFormUniversalMappedOutgoingHom x₀ W d) (c d) = 0) (d : Quiver.Costar W) : c d = 0

At an injective lifted source, a vanishing outgoing costar sum has all coefficients zero.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_scalar_eq_zero_of_add_outgoingCostar_eq_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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (r : k) (c : (d : Quiver.Costar W) → S.fgObj d.fst.fst ⟶ S.fgObj W.fst) (hc : r • CategoryTheory.CategoryStruct.id (S.fgObj W.fst) + ∑ d : Quiver.Costar W, CategoryTheory.CategoryStruct.comp (S.standardFormUniversalMappedOutgoingHom x₀ W d) (c d) = 0) : r = 0

A scalar identity cannot cancel a sum through the normalized outgoing costar arrows.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_projective_incoming_exact {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ X : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (hW : W ∈ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀) (c : (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) → S.fgObj X ⟶ S.fgObj (FiniteTauMatrix.rightMiddleLabel S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst i)) (hc : ∑ i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst), CategoryTheory.CategoryStruct.comp (c i) (S.standardFormUniversalNormalizedArrowMap x₀ (S.standardFormUniversalMiddleArrow x₀ W i)) = 0) (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) : c i = 0

At a projective lifted endpoint, a vanishing incoming-arrow sum has all displayed coefficients zero.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_projective_incomingStar_exact {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ X : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (hW : W ∈ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀) (c : (d : Quiver.Star W) → S.fgObj X ⟶ S.fgObj d.fst.fst) (hc : ∑ d : Quiver.Star W, CategoryTheory.CategoryStruct.comp (c d) (S.standardFormUniversalMappedIncomingHom x₀ W d) = 0) (d : Quiver.Star W) : c d = 0

Projective incoming exactness in the star coordinates produced directly by raw final-arrow decomposition.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_nonprojective_incoming_exact {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ X : Fin S.n) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) (c : (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData (↑W).fst)) → S.fgObj X ⟶ S.fgObj (FiniteTauMatrix.rightMiddleLabel S.finiteTauCategoryData.toFiniteRightTauCategoryData (↑W).fst i)) (hc : ∑ i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData (↑W).fst), CategoryTheory.CategoryStruct.comp (c i) (S.standardFormUniversalNormalizedArrowMap x₀ (S.standardFormUniversalMiddleArrow x₀ (↑W) i)) = 0) : ∃ (t : S.fgObj X ⟶ S.fgObj (S.standardFormTau (MeshCategory.RightMeshData.UniversalCover.baseNonprojective S.standardFormRightMeshData x₀ W))), ∀ (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData (↑W).fst)), c i = CategoryTheory.CategoryStruct.comp t (S.standardFormUniversalNormalizedArrowMap x₀ (S.standardFormUniversalPairedMiddleArrow x₀ W i))

At a nonprojective lifted endpoint, a vanishing incoming-arrow sum is the image of the paired mesh-source family.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_nonprojective_incomingStar_exact {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ X : Fin S.n) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) (c : (d : Quiver.Star ↑W) → S.fgObj X ⟶ S.fgObj d.fst.fst) (hc : ∑ d : Quiver.Star ↑W, CategoryTheory.CategoryStruct.comp (c d) (S.standardFormUniversalMappedIncomingHom x₀ (↑W) d) = 0) : ∃ (t : S.fgObj X ⟶ S.fgObj (S.standardFormTau (MeshCategory.RightMeshData.UniversalCover.baseNonprojective S.standardFormRightMeshData x₀ W))), ∀ (d : Quiver.Star ↑W), c d = CategoryTheory.CategoryStruct.comp t (S.standardFormUniversalMappedPairedIncomingHom x₀ W d)

Nonprojective incoming exactness in the star coordinates produced directly by raw final-arrow decomposition.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_scalar_eq_zero_of_add_incoming_eq_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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (r : k) (c : (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) → S.fgObj W.fst ⟶ S.fgObj (FiniteTauMatrix.rightMiddleLabel S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst i)) (hc : r • CategoryTheory.CategoryStruct.id (S.fgObj W.fst) + ∑ i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst), CategoryTheory.CategoryStruct.comp (c i) (S.standardFormUniversalMappedMiddleHom x₀ W i) = 0) : r = 0

A scalar identity cannot cancel a sum through the normalized incoming irreducible arrows.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_scalar_eq_zero_of_add_incomingStar_eq_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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (r : k) (c : (d : Quiver.Star W) → S.fgObj W.fst ⟶ S.fgObj d.fst.fst) (hc : r • CategoryTheory.CategoryStruct.id (S.fgObj W.fst) + ∑ d : Quiver.Star W, CategoryTheory.CategoryStruct.comp (c d) (S.standardFormUniversalMappedIncomingHom x₀ W d) = 0) : r = 0

Star-indexed scalar separation, in the coordinates produced directly by the raw final-arrow decomposition.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_endomorphism_eq_scalar_add_arrow_sum {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (f : S.fgObj W.fst ⟶ S.fgObj W.fst) : ∃ (r : k) (g : (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) → S.fgObj W.fst ⟶ S.fgObj (FiniteTauMatrix.rightMiddleLabel S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst i)), f = r • CategoryTheory.CategoryStruct.id (S.fgObj W.fst) + ∑ i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst), CategoryTheory.CategoryStruct.comp (g i) (S.standardFormUniversalNormalizedArrowMap x₀ (S.standardFormUniversalMiddleArrow x₀ W i))

One radical-layer step for an endomorphism: remove its scalar residue, then factor the radical remainder through the lifted right almost-split sink.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_morphism_eq_arrow_sum_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) {X : Fin S.n} (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (hXW : X ≠ W.fst) (f : S.fgObj X ⟶ S.fgObj W.fst) : ∃ (g : (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) → S.fgObj X ⟶ S.fgObj (FiniteTauMatrix.rightMiddleLabel S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst i)), f = ∑ i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst), CategoryTheory.CategoryStruct.comp (g i) (S.standardFormUniversalNormalizedArrowMap x₀ (S.standardFormUniversalMiddleArrow x₀ W i))

One radical-layer step between differently labelled indecomposables: the morphism itself factors through the lifted right almost-split sink.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_oneStep_sourceFiber {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) (X : S.FGIndecCategory) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (f : S.fgObj X ⟶ S.fgObj W.fst) : ∃ (a : DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => ↑Z ⟶ S.standardFormUniversalMeshObj x₀ W) (g : (i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst)) → S.fgObj X ⟶ S.fgObj (FiniteTauMatrix.rightMiddleLabel S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst i)), CategoryTheory.InducedCategory.homMk f = (LinearCovering.sourceFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) X (S.standardFormUniversalMeshObj x₀ W)) a + CategoryTheory.InducedCategory.homMk (∑ i : Fin (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData W.fst), CategoryTheory.CategoryStruct.comp (g i) (S.standardFormUniversalNormalizedArrowMap x₀ (S.standardFormUniversalMiddleArrow x₀ W i)))

The Riedtmann one-step decomposition, already bundling the scalar identity term as a source-fibre contribution of the mesh functor.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_exists_sourceFiber_mod_radicalPower {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) (X : S.FGIndecCategory) (n : ℕ) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (f : S.fgObj X ⟶ S.fgObj W.fst) : ∃ (a : DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => ↑Z ⟶ S.standardFormUniversalMeshObj x₀ W), (CategoryTheory.InducedCategory.homMk f - (LinearCovering.sourceFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) X (S.standardFormUniversalMeshObj x₀ W)) a).hom ∈ (S.fgNilpotentRadicalData.ideal.pow n).hom (S.fgObj X) (S.fgObj W.fst)

Riedtmann's fixed-target approximation: modulo the n-th radical power, every module morphism is the image of a finite source-fibre sum of raw mesh morphisms.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_sourceFiberHomMap_surjective_meshObj {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) (X : S.FGIndecCategory) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) : Function.Surjective ⇑(LinearCovering.sourceFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) X (S.standardFormUniversalMeshObj x₀ W))

Nilpotence terminates the radical-layer approximation, giving exact surjectivity of the fixed-target source-fibre map at every represented universal-cover vertex.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_sourceFiber_kernel_peel {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) (X : S.FGIndecCategory) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (a : DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => ↑Z ⟶ S.standardFormUniversalMeshObj x₀ W) (ha : (LinearCovering.sourceFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) X (S.standardFormUniversalMeshObj x₀ W)) a = 0) : ∃ (b : (d : Quiver.Star W) → DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => ↑Z ⟶ S.standardFormUniversalMeshObj x₀ d.fst), (∀ (d : Quiver.Star W), (LinearCovering.sourceFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) X (S.standardFormUniversalMeshObj x₀ d.fst)) (b d) = 0) ∧ a = ∑ d : Quiver.Star W, (LinearCovering.sourceFiberPostcomp (S.standardFormUniversalIndecMeshFunctor x₀) X ((MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀).incomingArrowHom d)) (b d)

One exact Riedtmann peeling step in a fixed-target source fibre. A family in the kernel is a sum through the arrows entering the target, and the coefficient family can be chosen in the kernel at every preceding target. In the nonprojective case this is achieved by lifting the common mesh-source factor and subtracting the resulting mesh relation.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_targetFiber_kernel_peel {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (X : S.FGIndecCategory) (a : DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => S.standardFormUniversalMeshObj x₀ W ⟶ ↑Z) (ha : (LinearCovering.targetFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) (S.standardFormUniversalMeshObj x₀ W) X) a = 0) : ∃ (b : (d : Quiver.Costar W) → DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => S.standardFormUniversalMeshObj x₀ d.fst ⟶ ↑Z), (∀ (d : Quiver.Costar W), (LinearCovering.targetFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) (S.standardFormUniversalMeshObj x₀ d.fst) X) (b d) = 0) ∧ a = ∑ d : Quiver.Costar W, (LinearCovering.targetFiberPrecomp (S.standardFormUniversalIndecMeshFunctor x₀) X ((MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀).outgoingArrowHom d)) (b d)

One exact Riedtmann peeling step in a fixed-source target fibre. A kernel family is a sum through the arrows leaving its source, with every coefficient family again in the kernel.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalSourceFiberInLengthTail {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) (X : S.FGIndecCategory) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (n : ℕ) (a : DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => ↑Z ⟶ S.standardFormUniversalMeshObj x₀ W) : Prop

Componentwise path-length tail membership for a fixed-target source-fibre family.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_sourceFiberPostcomp_inLengthTail_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) (X : S.FGIndecCategory) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (d : Quiver.Star W) (n : ℕ) (a : DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => ↑Z ⟶ S.standardFormUniversalMeshObj x₀ d.fst) (ha : S.standardFormUniversalSourceFiberInLengthTail x₀ X d.fst n a) : S.standardFormUniversalSourceFiberInLengthTail x₀ X W (n + 1) ((LinearCovering.sourceFiberPostcomp (S.standardFormUniversalIndecMeshFunctor x₀) X ((MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀).incomingArrowHom d)) a)

Postcomposition by one displayed incoming arrow raises the componentwise path-length tail by one.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_sourceFiber_eq_zero_of_inLengthTail_all {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) (X : S.FGIndecCategory) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (a : DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => ↑Z ⟶ S.standardFormUniversalMeshObj x₀ W) (ha : ∀ (n : ℕ), S.standardFormUniversalSourceFiberInLengthTail x₀ X W n a) : a = 0

Componentwise path-length tails are separated on a fixed-target source fibre.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_sourceFiber_kernel_mem_lengthTail {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) (X : S.FGIndecCategory) (n : ℕ) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (a : DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => ↑Z ⟶ S.standardFormUniversalMeshObj x₀ W) (ha : (LinearCovering.sourceFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) X (S.standardFormUniversalMeshObj x₀ W)) a = 0) : S.standardFormUniversalSourceFiberInLengthTail x₀ X W n a

Iterated kernel peeling places a fixed-target kernel family in every prescribed path-length tail.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_sourceFiber_kernel_eq_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) (X : S.FGIndecCategory) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (a : DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => ↑Z ⟶ S.standardFormUniversalMeshObj x₀ W) (ha : (LinearCovering.sourceFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) X (S.standardFormUniversalMeshObj x₀ W)) a = 0) : a = 0

The fixed-target source-fibre map of the normalized universal realization has trivial kernel.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_sourceFiberHomMap_injective_meshObj {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) (X : S.FGIndecCategory) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) : Function.Injective ⇑(LinearCovering.sourceFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) X (S.standardFormUniversalMeshObj x₀ W))

Fixed-target source-fibre injectivity for a displayed universal-cover mesh object.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_sourceFiberHomMap_surjective {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) (X : S.FGIndecCategory) (Y : MeshCategory.RawCategory (MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀)) : Function.Surjective ⇑(LinearCovering.sourceFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) X Y)

Every raw mesh-category object is literally represented by its underlying universal-cover vertex, so the fixed-target surjectivity holds for an arbitrary target object.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_sourceFiberHomMap_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) (X : S.FGIndecCategory) (Y : MeshCategory.RawCategory (MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀)) : Function.Injective ⇑(LinearCovering.sourceFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) X Y)

The fixed-target source-fibre map is injective for an arbitrary raw mesh-category target.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_sourceFiberHomMap_bijective {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) (X : S.FGIndecCategory) (Y : MeshCategory.RawCategory (MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀)) : Function.Bijective ⇑(LinearCovering.sourceFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) X Y)

The normalized universal realization satisfies the fixed-target half of the linear covering condition.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_targetFiberHomMap_surjective {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 : MeshCategory.RawCategory (MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀)) (X : S.FGIndecCategory) : Function.Surjective ⇑(LinearCovering.targetFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) Y X)

Every raw mesh-category source is literally represented by its underlying universal-cover vertex, so fixed-source target-fibre surjectivity holds for an arbitrary source object.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalTargetFiberInLengthTail {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (X : S.FGIndecCategory) (n : ℕ) (a : DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => S.standardFormUniversalMeshObj x₀ W ⟶ ↑Z) : Prop

Componentwise path-length tail membership for a fixed-source target-fibre family.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_targetFiberPrecomp_inLengthTail_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) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (d : Quiver.Costar W) (X : S.FGIndecCategory) (n : ℕ) (a : DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => S.standardFormUniversalMeshObj x₀ d.fst ⟶ ↑Z) (ha : S.standardFormUniversalTargetFiberInLengthTail x₀ d.fst X n a) : S.standardFormUniversalTargetFiberInLengthTail x₀ W X (n + 1) ((LinearCovering.targetFiberPrecomp (S.standardFormUniversalIndecMeshFunctor x₀) X ((MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀).outgoingArrowHom d)) a)

Precomposition by one displayed outgoing arrow raises the componentwise path-length tail by one.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_targetFiber_eq_zero_of_inLengthTail_all {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (X : S.FGIndecCategory) (a : DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => S.standardFormUniversalMeshObj x₀ W ⟶ ↑Z) (ha : ∀ (n : ℕ), S.standardFormUniversalTargetFiberInLengthTail x₀ W X n a) : a = 0

Componentwise path-length tails are separated on a fixed-source target fibre.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_targetFiber_kernel_mem_lengthTail {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (X : S.FGIndecCategory) (a : DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => S.standardFormUniversalMeshObj x₀ W ⟶ ↑Z) (ha : (LinearCovering.targetFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) (S.standardFormUniversalMeshObj x₀ W) X) a = 0) : S.standardFormUniversalTargetFiberInLengthTail x₀ W X n a

Iterated kernel peeling places a fixed-source kernel family in every prescribed path-length tail.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_targetFiber_kernel_eq_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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (X : S.FGIndecCategory) (a : DirectSum (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) fun (Z : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor x₀) X) => S.standardFormUniversalMeshObj x₀ W ⟶ ↑Z) (ha : (LinearCovering.targetFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) (S.standardFormUniversalMeshObj x₀ W) X) a = 0) : a = 0

The fixed-source target-fibre map of the normalized universal realization has trivial kernel.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_targetFiberHomMap_injective_meshObj {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (X : S.FGIndecCategory) : Function.Injective ⇑(LinearCovering.targetFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) (S.standardFormUniversalMeshObj x₀ W) X)

Fixed-source target-fibre injectivity for a displayed universal-cover mesh object.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_targetFiberHomMap_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) (Y : MeshCategory.RawCategory (MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀)) (X : S.FGIndecCategory) : Function.Injective ⇑(LinearCovering.targetFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) Y X)

The fixed-source target-fibre map is injective for an arbitrary raw mesh-category source.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversal_targetFiberHomMap_bijective {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 : MeshCategory.RawCategory (MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀)) (X : S.FGIndecCategory) : Function.Bijective ⇑(LinearCovering.targetFiberHomMap (S.standardFormUniversalIndecMeshFunctor x₀) Y X)

The normalized universal realization satisfies the fixed-source half of the linear covering condition.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalIndecMeshFunctor_isCovering {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) : LinearCovering.IsCovering (S.standardFormUniversalIndecMeshFunctor x₀)

The normalized standard-form realization of the universal mesh category is a linear covering functor.