Local normalization on the standard-form universal cover #
Square-freeness makes the indecomposable labels in a displayed mesh middle term pairwise distinct. If every realized sink is minimal right almost split, then every assigned arrow is irreducible. The paired arrows in one lifted mesh therefore assemble into a minimal left almost-split map: after factoring its components through the chosen left almost-split source, the comparison endomorphism has invertible diagonal entries and hence is an automorphism by the finite Krull--Schmidt matrix theorem.
Twisting the chosen right sink by the inverse comparison makes the lifted mesh relation hold literally while preserving minimal right almost-splitness.
theorem
MagnitudeConjecture.RightModule.rightMinimal_precomp_iso
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{E' E Z : C}
{f : E ⟶ Z}
(hf : QuotientSubmoduleEquidistribution.IsRightMinimal f)
(e : E' ≅ E)
:
QuotientSubmoduleEquidistribution.IsRightMinimal (CategoryTheory.CategoryStruct.comp e.hom f)
Precomposition by an isomorphism preserves right minimality.
@[instance_reducible]
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNormalizationQuiverInstance
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
:
Quiver (Fin S.n)
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRightMiddleLabel_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)
:
Function.Injective (FiniteTauMatrix.rightMiddleLabel S.finiteTauCategoryData.toFiniteRightTauCategoryData x)
The official middle labels of a standard-form right mesh are pairwise distinct.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.isIrreducible_comp_of_rightAlmostSplit_rightMinimal
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
{x y : Fin S.n}
{E : FinitelyGeneratedCategory A}
(inc : S.fgObj x ⟶ E)
(proj : E ⟶ S.fgObj x)
(hinc : CategoryTheory.CategoryStruct.comp inc proj = CategoryTheory.CategoryStruct.id (S.fgObj x))
(g : E ⟶ S.fgObj y)
(hg : QuotientSubmoduleEquidistribution.IsRightAlmostSplit g)
(hgmin : QuotientSubmoduleEquidistribution.IsRightMinimal g)
:
QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (CategoryTheory.CategoryStruct.comp inc g)
A component cut out by a split inclusion from a minimal right almost-split morphism between selected indecomposables is irreducible.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSinkCondition.arrow_isIrreducible
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
{D : S.StandardFormUniversalArrowAssignment x₀}
(hD :
S.StandardFormUniversalSinkCondition x₀
fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D)
{W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀}
(a : W ⟶ Z)
:
Under the global sink invariant, every universal-cover arrow representative is irreducible.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSinkCondition.exists_realizedSource_iso
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
{D : S.StandardFormUniversalArrowAssignment x₀}
(hD :
S.StandardFormUniversalSinkCondition x₀
fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D)
(W :
{ W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ })
:
∃ (e :
(S.finiteTauCategoryData.rightMesh (S.fgObj (↑W).fst)).X₂ ≅ (S.finiteTauCategoryData.rightMesh (S.fgObj (↑W).fst)).X₂),
CategoryTheory.CategoryStruct.comp
(S.standardFormRightSource
(MeshCategory.RightMeshData.UniversalCover.baseNonprojective S.standardFormRightMeshData x₀ W))
e.hom = S.standardFormUniversalRealizedSource x₀
(fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W
The representatives on the polarized partner arrows assemble into a minimal left almost-split map. More precisely, they differ from the chosen right-mesh source by an automorphism of the displayed middle term.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSinkCondition.realizedSourceIso
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
{D : S.StandardFormUniversalArrowAssignment x₀}
(hD :
S.StandardFormUniversalSinkCondition x₀
fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D)
(W :
{ W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ })
:
(S.finiteTauCategoryData.rightMesh (S.fgObj (↑W).fst)).X₂ ≅ (S.finiteTauCategoryData.rightMesh (S.fgObj (↑W).fst)).X₂
The canonical comparison automorphism between the chosen mesh source and the source assembled from a sink-compatible universal assignment.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSinkCondition.rightSource_comp_realizedSourceIso
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
{D : S.StandardFormUniversalArrowAssignment x₀}
(hD :
S.StandardFormUniversalSinkCondition x₀
fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D)
(W :
{ W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ })
:
CategoryTheory.CategoryStruct.comp
(S.standardFormRightSource
(MeshCategory.RightMeshData.UniversalCover.baseNonprojective S.standardFormRightMeshData x₀ W))
(realizedSourceIso S x₀ hD W).hom = S.standardFormUniversalRealizedSource x₀
(fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W
The comparison automorphism realizes the assembled source exactly.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSinkCondition.realizedSource_isLeftAlmostSplit
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
{D : S.StandardFormUniversalArrowAssignment x₀}
(hD :
S.StandardFormUniversalSinkCondition x₀
fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D)
(W :
{ W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ })
:
The source assembled from a sink-compatible universal assignment is left almost split.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSinkCondition.realizedSource_isLeftMinimal
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
{D : S.StandardFormUniversalArrowAssignment x₀}
(hD :
S.StandardFormUniversalSinkCondition x₀
fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D)
(W :
{ W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ })
:
The source assembled from a sink-compatible universal assignment is left minimal.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSinkCondition.normalizedSink
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
{D : S.StandardFormUniversalArrowAssignment x₀}
(hD :
S.StandardFormUniversalSinkCondition x₀
fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D)
(W :
{ W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ })
:
(S.finiteTauCategoryData.rightMesh (S.fgObj (↑W).fst)).X₂ ⟶ S.fgObj (↑W).fst
Twist the chosen downstairs right sink so that its source is the source assembled from the current universal arrow assignment.
Instances For
@[simp]
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSinkCondition.realizedSource_comp_normalizedSink
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
{D : S.StandardFormUniversalArrowAssignment x₀}
(hD :
S.StandardFormUniversalSinkCondition x₀
fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D)
(W :
{ W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ })
:
CategoryTheory.CategoryStruct.comp
(S.standardFormUniversalRealizedSource x₀
(fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W)
(normalizedSink S x₀ hD W) = 0
The locally normalized source and sink have zero composite.
@[simp]
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSinkCondition.realizedSource_comp_normalizedSink_assoc
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
{D : S.StandardFormUniversalArrowAssignment x₀}
(hD :
S.StandardFormUniversalSinkCondition x₀
fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D)
(W :
{ W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ })
{Z : FinitelyGeneratedCategory A}
(h : S.fgObj (↑W).fst ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(S.standardFormUniversalRealizedSource x₀
(fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W)
(CategoryTheory.CategoryStruct.comp (normalizedSink S x₀ hD W) h) = CategoryTheory.CategoryStruct.comp 0 h
The locally normalized source and sink have zero composite.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSinkCondition.normalizedSink_isRightAlmostSplit
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
{D : S.StandardFormUniversalArrowAssignment x₀}
(hD :
S.StandardFormUniversalSinkCondition x₀
fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D)
(W :
{ W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ })
:
The locally normalized sink remains right almost split.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSinkCondition.normalizedSink_isRightMinimal
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
{D : S.StandardFormUniversalArrowAssignment x₀}
(hD :
S.StandardFormUniversalSinkCondition x₀
fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D)
(W :
{ W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ })
:
The locally normalized sink remains right minimal.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSinkCondition.heightSink
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
{D : S.StandardFormUniversalArrowAssignment x₀}
(hD :
S.StandardFormUniversalSinkCondition x₀
fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D)
(m : ℤ)
(W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀)
(_hW : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ W = m)
:
(S.finiteTauCategoryData.rightMesh (S.fgObj W.fst)).X₂ ⟶ S.fgObj W.fst
At one height, use the normalized sink at nonprojective vertices and leave the current realized sink unchanged at projective vertices.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSinkCondition.heightSink_eq_of_projective
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
{D : S.StandardFormUniversalArrowAssignment x₀}
(hD :
S.StandardFormUniversalSinkCondition x₀
fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D)
(m : ℤ)
(W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀)
(hW : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ W = m)
(hP : W ∈ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀)
:
heightSink S x₀ hD m W hW = S.standardFormUniversalRealizedSink x₀
(fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSinkCondition.heightSink_eq_of_nonprojective
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
{D : S.StandardFormUniversalArrowAssignment x₀}
(hD :
S.StandardFormUniversalSinkCondition x₀
fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D)
(m : ℤ)
(W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀)
(hW : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ W = m)
(hP : W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀)
:
heightSink S x₀ hD m W hW = normalizedSink S x₀ hD ⟨W, hP⟩
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSinkCondition.normalizeAtHeight
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
{D : S.StandardFormUniversalArrowAssignment x₀}
(hD :
S.StandardFormUniversalSinkCondition x₀
fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D)
(m : ℤ)
:
Simultaneously normalize every nonprojective lifted mesh at one height, while retaining projective sinks.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSinkCondition.normalizeAtHeight_sinkCondition
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
{D : S.StandardFormUniversalArrowAssignment x₀}
(hD :
S.StandardFormUniversalSinkCondition x₀
fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D)
(m : ℤ)
:
S.StandardFormUniversalSinkCondition x₀
fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} =>
normalizeAtHeight S x₀ hD m
Height normalization preserves the global minimal right almost-split sink invariant.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSinkCondition.realizedSource_normalizeAtHeight_eq
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
{D : S.StandardFormUniversalArrowAssignment x₀}
(hD :
S.StandardFormUniversalSinkCondition x₀
fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D)
(m : ℤ)
(W :
{ W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ })
(hW : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ ↑W = m)
:
S.standardFormUniversalRealizedSource x₀
(fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} =>
normalizeAtHeight S x₀ hD m)
W = S.standardFormUniversalRealizedSource x₀
(fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D) W
Replacing sinks at height m does not change the source of a mesh whose
endpoint has height m: every paired arrow used by that source starts one
height lower.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSinkCondition.normalizeAtHeight_mesh_zero
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
{D : S.StandardFormUniversalArrowAssignment x₀}
(hD :
S.StandardFormUniversalSinkCondition x₀
fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => D)
(m : ℤ)
(W :
{ W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ })
(hW : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ ↑W = m)
:
CategoryTheory.CategoryStruct.comp
(S.standardFormUniversalRealizedSource x₀
(fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} =>
normalizeAtHeight S x₀ hD m)
W)
(S.standardFormUniversalRealizedSink x₀
(fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} =>
normalizeAtHeight S x₀ hD m)
↑W) = 0
Every nonprojective mesh at the selected height satisfies its literal zero relation after simultaneous normalization.
structure
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSinkAssignment
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
:
Type u
An arrow assignment together with the global minimal right almost-split sink invariant needed by the positive-height induction.
- arrowMap : S.StandardFormUniversalArrowAssignment x₀
- sinkCondition : S.StandardFormUniversalSinkCondition x₀ fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => self.arrowMap
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalInitialSinkAssignment
{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)
:
The occurrence-component assignment is the initial state of the positive-height induction.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormUniversalSinkAssignment.normalizeAtHeight
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
(E : S.StandardFormUniversalSinkAssignment x₀)
(m : ℤ)
:
Normalize all sinks at one height while retaining the global sink invariant.
Instances For
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalPositiveStage
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
:
ℕ → S.StandardFormUniversalSinkAssignment x₀
Stage n of the positive induction has normalized precisely the positive
heights 1, ..., n.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalPositiveArrowMap
{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)
:
The positive limiting assignment. An arrow whose source has positive
height n takes its representative from stage n; arrows of nonpositive
source height retain their initial representatives.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalPositiveArrowMap_eq_stage_of_height_eq_nat
{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 Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀}
(hW : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ W = ↑n)
(a : W ⟶ Z)
:
S.standardFormUniversalPositiveArrowMap x₀ a = (S.standardFormUniversalPositiveStage x₀ n).arrowMap a
At a source of natural-number height n, the positive limiting
assignment agrees with stage n.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalPositiveStage_succ_arrow_eq_of_height_ne
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
(n : ℕ)
{W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀}
(hW : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ W ≠ ↑(n + 1))
(a : W ⟶ Z)
:
(S.standardFormUniversalPositiveStage x₀ (n + 1)).arrowMap a = (S.standardFormUniversalPositiveStage x₀ n).arrowMap a
The successor positive stage changes only arrows whose source has the newly processed height.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalPositiveRealizedSink_eq_stage
{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₀)
(hW : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ W = ↑n)
:
S.standardFormUniversalRealizedSink x₀
(fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} =>
S.standardFormUniversalPositiveArrowMap x₀)
W = S.standardFormUniversalRealizedSink x₀
(fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} =>
(S.standardFormUniversalPositiveStage x₀ n).arrowMap)
W
At a vertex of natural-number height n, the limiting realized sink is
already the sink of stage n.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalPositiveRealizedSource_eq_stage_succ
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
(n : ℕ)
(W :
{ W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ })
(hW : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ ↑W = ↑(n + 1))
:
S.standardFormUniversalRealizedSource x₀
(fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} =>
S.standardFormUniversalPositiveArrowMap x₀)
W = S.standardFormUniversalRealizedSource x₀
(fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} =>
(S.standardFormUniversalPositiveStage x₀ (n + 1)).arrowMap)
W
For a mesh ending at height n + 1, its source in the limiting
assignment is already its source at stage n + 1. Its paired arrows start
at height n, so the successor stage leaves them unchanged.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalPositive_mesh_zero_of_height_eq_succ
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
(n : ℕ)
(W :
{ W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ })
(hW : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ ↑W = ↑(n + 1))
:
CategoryTheory.CategoryStruct.comp
(S.standardFormUniversalRealizedSource x₀
(fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} =>
S.standardFormUniversalPositiveArrowMap x₀)
W)
(S.standardFormUniversalRealizedSink x₀
(fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} =>
S.standardFormUniversalPositiveArrowMap x₀)
↑W) = 0
Every mesh whose endpoint has positive natural-number height satisfies its literal zero relation in the positive limiting assignment.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalPositiveRealizedSink_eq_initial_of_nonpos
{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 : MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ W ≤ 0)
:
S.standardFormUniversalRealizedSink x₀
(fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} =>
S.standardFormUniversalPositiveArrowMap x₀)
W = S.standardFormUniversalRealizedSink x₀
(fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} =>
S.standardFormUniversalArrowMap x₀)
W
At a nonpositive source height, the positive induction leaves the realized sink equal to its initial value.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalPositiveArrowMap_sinkCondition
{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)
:
Passing to the pointwise positive limit preserves the global minimal right almost-split sink invariant.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalPositive_mesh_zero
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x₀ : Fin S.n)
(W :
{ W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ })
(hW : 0 < MeshCategory.RightMeshData.UniversalCover.vertexHeight S.standardFormRightMeshData x₀ ↑W)
:
CategoryTheory.CategoryStruct.comp
(S.standardFormUniversalRealizedSource x₀
(fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} =>
S.standardFormUniversalPositiveArrowMap x₀)
W)
(S.standardFormUniversalRealizedSink x₀
(fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} =>
S.standardFormUniversalPositiveArrowMap x₀)
↑W) = 0
Every nonprojective mesh at positive height satisfies its literal zero relation in the positive limiting assignment.