The standard mesh grading after deleting indecomposables #
This file isolates the homogeneous-ideal step in Proposition 3.7 of the frozen manuscript. A standard mesh presentation grades the ambient skeleton by path length. The ideal of maps factoring through the deleted additive subcategory is then proved homogeneous, so the literal factor category inherits that grading.
The proof expands a factorization through a finite biproduct of deleted indecomposables and then expands both coordinate maps into their homogeneous parts. No alternative or legacy grading interface is retained.
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.factorIdealSubmodule
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(K : Set (Fin S.n))
(x y : Fin S.n)
:
Submodule k (S.ambientAddPoint x ⟶ S.ambientAddPoint y)
The factor ideal in one ambient skeleton Hom space, regarded as a linear submodule.
Instances For
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.FactorIdealIsHomogeneous
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[quiver : Quiver (Fin S.n)]
[arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)]
{T : MeshCategory.RightMeshData (Fin S.n)}
(H : S.StandardMeshPresentation T)
(K : Set (Fin S.n))
:
The manuscript's homogeneous-deleted-ideal assertion, stated directly for the ambient path grading supplied by standardness.
Instances For
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.homogeneousMorphismSet
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[quiver : Quiver (Fin S.n)]
[arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)]
{T : MeshCategory.RightMeshData (Fin S.n)}
(H : S.StandardMeshPresentation T)
(x y : Fin S.n)
:
Set (S.ambientAddPoint x ⟶ S.ambientAddPoint y)
The set of homogeneous morphisms in one ambient skeleton Hom space.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.span_homogeneousMorphismSet_eq_top
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[quiver : Quiver (Fin S.n)]
[arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)]
{T : MeshCategory.RightMeshData (Fin S.n)}
(H : S.StandardMeshPresentation T)
(x y : Fin S.n)
:
Submodule.span k (H.homogeneousMorphismSet x y) = ⊤
The homogeneous morphisms span the whole ambient skeleton Hom space.
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.homogeneousFactorGeneratorSet
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[quiver : Quiver (Fin S.n)]
[arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)]
{T : MeshCategory.RightMeshData (Fin S.n)}
(H : S.StandardMeshPresentation T)
(K : Set (Fin S.n))
(x y : Fin S.n)
:
Set (S.ambientAddPoint x ⟶ S.ambientAddPoint y)
Homogeneous composites through one deleted indecomposable.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.composite_mem_span_homogeneousFactorGeneratorSet
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[quiver : Quiver (Fin S.n)]
[arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)]
{T : MeshCategory.RightMeshData (Fin S.n)}
(H : S.StandardMeshPresentation T)
(K : Set (Fin S.n))
{x y z : Fin S.n}
(hz : z ∈ K)
(left : S.ambientAddPoint x ⟶ S.ambientAddPoint z)
(right : S.ambientAddPoint z ⟶ S.ambientAddPoint y)
:
CategoryTheory.CategoryStruct.comp left right ∈ Submodule.span k (H.homogeneousFactorGeneratorSet K x y)
An arbitrary composite through one deleted indecomposable lies in the span of homogeneous such composites.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.factorIdealSubmodule_eq_span_homogeneousFactorGeneratorSet
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[quiver : Quiver (Fin S.n)]
[arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)]
{T : MeshCategory.RightMeshData (Fin S.n)}
(H : S.StandardMeshPresentation T)
(K : Set (Fin S.n))
(x y : Fin S.n)
:
factorIdealSubmodule K x y = Submodule.span k (H.homogeneousFactorGeneratorSet K x y)
Maps factoring through the deleted additive subcategory are exactly the span of homogeneous composites through individual deleted indecomposables.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.homogeneousFactorGeneratorSet_isHomogeneous
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[quiver : Quiver (Fin S.n)]
[arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)]
{T : MeshCategory.RightMeshData (Fin S.n)}
(H : S.StandardMeshPresentation T)
(K : Set (Fin S.n))
{x y : Fin S.n}
{f : S.ambientAddPoint x ⟶ S.ambientAddPoint y}
(hf : f ∈ H.homogeneousFactorGeneratorSet K x y)
:
∃ (d : ℕ), f ∈ H.component x y d
Every generator in the homogeneous presentation of the deleted-object ideal belongs to one ambient path-degree component.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.factorIdealIsHomogeneous
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[quiver : Quiver (Fin S.n)]
[arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)]
{T : MeshCategory.RightMeshData (Fin S.n)}
(H : S.StandardMeshPresentation T)
(K : Set (Fin S.n))
:
The ideal of maps factoring through any chosen additive closure of deleted indecomposables is homogeneous for the standard mesh grading.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.factorHomLinearMap
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(K : Set (Fin S.n))
(x y : Fin S.n)
:
(S.ambientAddPoint x ⟶ S.ambientAddPoint y) →ₗ[k] (S.factorFunctor K).obj (S.ambientAddPoint x) ⟶ (S.factorFunctor K).obj (S.ambientAddPoint y)
The quotient map on a Hom space between two selected indecomposables.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.ker_factorHomLinearMap
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(K : Set (Fin S.n))
(x y : Fin S.n)
:
(factorHomLinearMap K x y).ker = factorIdealSubmodule K x y
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.factorComponent
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[quiver : Quiver (Fin S.n)]
[arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)]
{T : MeshCategory.RightMeshData (Fin S.n)}
(H : S.StandardMeshPresentation T)
(K : Set (Fin S.n))
(x y : S.SurvivingLabel K)
(d : ℕ)
:
Submodule k (S.factorObject K x ⟶ S.factorObject K y)
The degree-d component in the literal factor Hom space.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.factorPathHom
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[quiver : Quiver (Fin S.n)]
[arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)]
{T : MeshCategory.RightMeshData (Fin S.n)}
(H : S.StandardMeshPresentation T)
(K : Set (Fin S.n))
{x y : Fin S.n}
(p : Quiver.Path y x)
:
(S.factorFunctor K).obj (S.ambientAddPoint x) ⟶ (S.factorFunctor K).obj (S.ambientAddPoint y)
The morphism represented in the literal factor by one quiver path. The
quiver orientation is opposite to categorical composition: a path y ⟶ x
represents a morphism from the object at x to the object at y.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.factorPathHom_mem_factorComponent
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[quiver : Quiver (Fin S.n)]
[arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)]
{T : MeshCategory.RightMeshData (Fin S.n)}
(H : S.StandardMeshPresentation T)
(K : Set (Fin S.n))
{x y : S.SurvivingLabel K}
(p : Quiver.Path ↑y ↑x)
{d : ℕ}
(hp : p.length = d)
:
H.factorPathHom K p ∈ H.factorComponent K x y d
A path of length d represents a degree-d morphism in the literal
factor.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.factorPathHom_comp
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[quiver : Quiver (Fin S.n)]
[arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)]
{T : MeshCategory.RightMeshData (Fin S.n)}
(H : S.StandardMeshPresentation T)
(K : Set (Fin S.n))
{x y z : Fin S.n}
(p : Quiver.Path y x)
(q : Quiver.Path z y)
:
H.factorPathHom K (q.comp p) = CategoryTheory.CategoryStruct.comp (H.factorPathHom K p) (H.factorPathHom K q)
Concatenation of paths becomes categorical composition in the literal factor.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.factorComponent_isInternal
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[quiver : Quiver (Fin S.n)]
[arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)]
{T : MeshCategory.RightMeshData (Fin S.n)}
(H : S.StandardMeshPresentation T)
(K : Set (Fin S.n))
(x y : S.SurvivingLabel K)
:
DirectSum.IsInternal (H.factorComponent K x y)
A homogeneous deleted-object ideal gives an internal grading on every factor Hom space between surviving skeleton objects.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.factor_comp_mem_component
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[quiver : Quiver (Fin S.n)]
[arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)]
{T : MeshCategory.RightMeshData (Fin S.n)}
(H : S.StandardMeshPresentation T)
(K : Set (Fin S.n))
{x y z : S.SurvivingLabel K}
{i j : ℕ}
{f : S.factorObject K x ⟶ S.factorObject K y}
{g : S.factorObject K y ⟶ S.factorObject K z}
(hf : f ∈ H.factorComponent K x y i)
(hg : g ∈ H.factorComponent K y z j)
:
CategoryTheory.CategoryStruct.comp f g ∈ H.factorComponent K x z (i + j)
Composition in the factor grading adds path degrees.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.factor_id_mem_component_zero
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[quiver : Quiver (Fin S.n)]
[arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)]
{T : MeshCategory.RightMeshData (Fin S.n)}
(H : S.StandardMeshPresentation T)
(K : Set (Fin S.n))
(x : S.SurvivingLabel K)
:
CategoryTheory.CategoryStruct.id (S.factorObject K x) ∈ H.factorComponent K x x 0
Identities of surviving factor objects have degree zero.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.factorComponent_mem_radical_of_pos
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[quiver : Quiver (Fin S.n)]
[arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)]
{T : MeshCategory.RightMeshData (Fin S.n)}
[IsAlgClosed k]
(H : S.StandardMeshPresentation T)
(Hdir : S.HasAcyclicNonzeroNonisomorphisms)
(K : Set (Fin S.n))
{x y : S.SurvivingLabel K}
{d : ℕ}
{f : S.factorObject K x ⟶ S.factorObject K y}
(hf : f ∈ H.factorComponent K x y d)
(hd : 0 < d)
:
f ∈ (S.factorFiniteTauCategoryData K).radical.ideal.hom (S.factorObject K x) (S.factorObject K y)
Every positive-degree homogeneous morphism between surviving factor indecomposables belongs to the categorical radical.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.factorPathHom_mem_radical_mul
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[quiver : Quiver (Fin S.n)]
[arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)]
{T : MeshCategory.RightMeshData (Fin S.n)}
[IsAlgClosed k]
(H : S.StandardMeshPresentation T)
(Hdir : S.HasAcyclicNonzeroNonisomorphisms)
(K : Set (Fin S.n))
{x y : S.SurvivingLabel K}
(p : Quiver.Path ↑y ↑x)
(hp : 2 ≤ p.length)
:
H.factorPathHom K p ∈ ((S.factorFiniteTauCategoryData K).radical.ideal ⋆ᵢ (S.factorFiniteTauCategoryData K).radical.ideal).hom
(S.factorObject K x) (S.factorObject K y)
Every represented path of length at least two belongs to the square of the categorical radical in the literal factor. If the first intermediate vertex was deleted, the path factors through a zero object; otherwise its two positive-length pieces are radical.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.factorComponent_mem_radical_mul
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[quiver : Quiver (Fin S.n)]
[arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)]
{T : MeshCategory.RightMeshData (Fin S.n)}
[IsAlgClosed k]
(H : S.StandardMeshPresentation T)
(Hdir : S.HasAcyclicNonzeroNonisomorphisms)
(K : Set (Fin S.n))
{x y : S.SurvivingLabel K}
{d : ℕ}
{f : S.factorObject K x ⟶ S.factorObject K y}
(hf : f ∈ H.factorComponent K x y d)
(hd : 2 ≤ d)
:
f ∈ ((S.factorFiniteTauCategoryData K).radical.ideal ⋆ᵢ (S.factorFiniteTauCategoryData K).radical.ideal).hom
(S.factorObject K x) (S.factorObject K y)
Every morphism in a factor-category homogeneous component of degree at least two lies in the square of the categorical radical.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.factor_component_zero_eq_bot_of_ne
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[quiver : Quiver (Fin S.n)]
[arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)]
{T : MeshCategory.RightMeshData (Fin S.n)}
(H : S.StandardMeshPresentation T)
(K : Set (Fin S.n))
{x y : S.SurvivingLabel K}
(hxy : x ≠ y)
:
H.factorComponent K x y 0 = ⊥
Degree zero still vanishes between distinct surviving labels.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.factorSkeletonHomGrading
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[quiver : Quiver (Fin S.n)]
[arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)]
{T : MeshCategory.RightMeshData (Fin S.n)}
(H : S.StandardMeshPresentation T)
(K : Set (Fin S.n))
:
The path grading supplied by a standard mesh presentation descends to the exact skeleton-grading interface consumed by the poset-space argument.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.irreducible_mem_factorComponent_one
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[quiver : Quiver (Fin S.n)]
[arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)]
{T : MeshCategory.RightMeshData (Fin S.n)}
[IsAlgClosed k]
(H : S.StandardMeshPresentation T)
(Hdir : S.HasAcyclicNonzeroNonisomorphisms)
(K : Set (Fin S.n))
{D : S.PrimitiveMultiplicityInput K}
{P : Type u}
[Fintype P]
[PartialOrder P]
(R : S.PrimitiveProjectivePosetData D P)
(hsink : D.multiplicity ↑D.sink = 1)
{x y : S.SurvivingLabel K}
{f : S.factorObject K x ⟶ S.factorObject K y}
(hfirr : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f)
:
f ∈ H.factorComponent K x y 1
In the primitive-factor setting of the manuscript, every irreducible morphism between surviving indecomposables has path degree one.