Irreducibility across a single direct-height step #
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directHeight_radical_comp_eq_zero
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[IsAlgClosed k]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
(B : S.PrimitiveDirectedBoundaryData D)
{X Y : S.SurvivingLabel K}
(hgap : B.directFactorHeight Y ≤ B.directFactorHeight X + 1)
{M : S.FactorCategory K}
(g : S.factorObject K X ⟶ M)
(h : M ⟶ S.factorObject K Y)
(hg : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism g)
(hh : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism h)
:
CategoryTheory.CategoryStruct.comp g h = 0
The composite of two radical maps vanishes across at most one height step.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directHeight_radicalSquare_eq_zero
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[IsAlgClosed k]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
(B : S.PrimitiveDirectedBoundaryData D)
{X Y : S.SurvivingLabel K}
(hgap : B.directFactorHeight Y ≤ B.directFactorHeight X + 1)
(f : S.factorObject K X ⟶ S.factorObject K Y)
(hf :
f ∈ ((S.factorFiniteTauCategoryData K).radical.ideal ⋆ᵢ (S.factorFiniteTauCategoryData K).radical.ideal).hom
(S.factorObject K X) (S.factorObject K Y))
:
f = 0
In particular, the radical square vanishes across at most one height step.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directHeight_isIrreducible_of_eq_add_one
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[IsAlgClosed k]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
(B : S.PrimitiveDirectedBoundaryData D)
{X Y : S.SurvivingLabel K}
(hgap : B.directFactorHeight Y = B.directFactorHeight X + 1)
(f : S.factorObject K X ⟶ S.factorObject K Y)
(hf : f ≠ 0)
:
Nonzero maps across adjacent direct heights are irreducible.