Upper-set squares in a zero-excess primitive factor #
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directLineLabel
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[IsAlgClosed k]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(U : Finset B.ProjectivePoset)
(hU : IsUpperSet ↑U)
:
S.SurvivingLabel (S.primitiveKilledLabels D)
Selected factor label of an upper-set line.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directLineLabel_ne
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[IsAlgClosed k]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
{U V : Finset B.ProjectivePoset}
(hU : IsUpperSet ↑U)
(hV : IsUpperSet ↑V)
(hne : U ≠ V)
:
B.directLineLabel U hU ≠ B.directLineLabel V hV
Distinct upper sets give distinct selected labels.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directUpperSet_square_tauPlus
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[IsAlgClosed k]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(hz :
DirectedDeletion.intrinsicEulerExcess
(FiniteTauMatrix.meshMatrix (S.factorFiniteTauCategoryData (S.primitiveKilledLabels D))) = 0)
(U V W Y : Finset B.ProjectivePoset)
(hU : IsUpperSet ↑U)
(hV : IsUpperSet ↑V)
(hW : IsUpperSet ↑W)
(hY : IsUpperSet ↑Y)
(hUV : U ⊆ V)
(hVY : V ⊆ Y)
(hUW : U ⊆ W)
(hWY : W ⊆ Y)
(hVW : V ≠ W)
(hcV : V.card = U.card + 1)
(hcW : W.card = U.card + 1)
(hcY : Y.card = V.card + 1)
:
∃ (hn : ¬(S.factorFiniteTauCategoryData (S.primitiveKilledLabels D)).IsProjective (B.directLineLabel Y hY)),
(S.factorFiniteTauCategoryData (S.primitiveKilledLabels D)).tauPlus ⟨B.directLineLabel Y hY, hn⟩ = B.directLineLabel U hU
A diamond of upper sets whose edges add one element determines an AR translate when the primitive factor has zero excess.