Iyama's zero-middle boundary for a primitive factor #
The two Hom-unit equations identify the distinguished source and sink as the
only projective and injective boundary labels whose corresponding mesh has
zero middle term. This is the literal l⁺/l⁻ boundary condition used in
Iyama's projective-socle realization theorem.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.multiplicity_rightMeshDefect
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
(D : S.PrimitiveMultiplicityInput K)
(x : S.SurvivingLabel K)
:
FiniteTauMatrix.rightMeshLabelWeightDefect (S.factorFiniteTauCategoryData K)
(fun (y : S.SurvivingLabel K) => ↑(D.multiplicity ↑y)) x = if x = D.source then 1 else 0
The primitive multiplicity has categorical right-mesh defect one at the distinguished source and zero at every other label.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.multiplicity_leftMeshDefect
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
(D : S.PrimitiveMultiplicityInput K)
(x : S.SurvivingLabel K)
:
FiniteTauMatrix.leftMeshLabelWeightDefect (S.factorFiniteTauCategoryData K)
(fun (y : S.SurvivingLabel K) => ↑(D.multiplicity ↑y)) x = if x = D.sink then 1 else 0
The primitive multiplicity has categorical left-mesh defect one at the distinguished sink and zero at every other label.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.rightMiddle_isZero_iff_eq_source
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
(B : S.PrimitiveDirectedBoundaryData D)
(p : S.FactorProjectiveLabel K)
:
CategoryTheory.Limits.IsZero ((S.factorFiniteTauCategoryData K).thetaPlus ↑p) ↔ ↑p = D.source
Among the tau-projective boundary labels, the distinguished source is exactly the one with zero right-mesh middle term.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.leftMiddle_isZero_iff_eq_sink
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
(B : S.PrimitiveDirectedBoundaryData D)
(i : S.FactorInjectiveLabel K)
:
CategoryTheory.Limits.IsZero ((S.factorFiniteTauCategoryData K).thetaMinus ↑i) ↔ ↑i = D.sink
Among the tau-injective boundary labels, the distinguished sink is exactly the one with zero left-mesh middle term.