Commutative squares for the direct height #
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directHeight_square_tauPlus
{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 V W Y : S.SurvivingLabel K}
(hVW : V ≠ W)
(hV : B.directFactorHeight V = B.directFactorHeight X + 1)
(hW : B.directFactorHeight W = B.directFactorHeight X + 1)
(hY : B.directFactorHeight Y = B.directFactorHeight V + 1)
(a : S.factorObject K X ⟶ S.factorObject K V)
(b : S.factorObject K V ⟶ S.factorObject K Y)
(c : S.factorObject K X ⟶ S.factorObject K W)
(d : S.factorObject K W ⟶ S.factorObject K Y)
(ha : a ≠ 0)
(hb : b ≠ 0)
(hd : d ≠ 0)
(hsquare : CategoryTheory.CategoryStruct.comp a b = CategoryTheory.CategoryStruct.comp c d)
:
∃ (hn : ¬(S.factorFiniteTauCategoryData K).IsProjective Y), (S.factorFiniteTauCategoryData K).tauPlus ⟨Y, hn⟩ = X
A square of nonzero adjacent-height maps with distinct middle labels identifies the source with the target's AR translate.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directHeight_square_target_unique
{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 Z : S.SurvivingLabel K}
(hY : ∃ (hn : ¬(S.factorFiniteTauCategoryData K).IsProjective Y), (S.factorFiniteTauCategoryData K).tauPlus ⟨Y, hn⟩ = X)
(hZ : ∃ (hn : ¬(S.factorFiniteTauCategoryData K).IsProjective Z), (S.factorFiniteTauCategoryData K).tauPlus ⟨Z, hn⟩ = X)
:
Y = Z
Translation injectivity makes a square's target unique once its source has been identified as the translate.