Equal-height commutative squares identify the AR translate #
theorem
MagnitudeConjecture.FiniteTauMatrix.exists_nonzero_rightMesh_map_of_square
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{Ind : Type w}
[Fintype Ind]
(T : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C Ind)
{X V W Y : Ind}
(a : T.obj X ⟶ T.obj V)
(b : T.obj V ⟶ T.obj Y)
(c : T.obj X ⟶ T.obj W)
(d : T.obj W ⟶ T.obj Y)
(ha : a ≠ 0)
(hb : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism b)
(hd : ¬CategoryTheory.IsSplitEpi d)
(hWV : ∀ (f : T.obj W ⟶ T.obj V), f = 0)
(hsquare : CategoryTheory.CategoryStruct.comp a b = CategoryTheory.CategoryStruct.comp c d)
:
A square with orthogonal middle objects has a nonzero map from its source to the first term of the chosen right mesh.
theorem
MagnitudeConjecture.FiniteTauMatrix.tauPlus_eq_source_of_height_square
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{Ind : Type w}
[Fintype Ind]
(T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind)
(height : Ind → ℕ)
(hh : ∀ {x y : Ind} (f : T.obj x ⟶ T.obj y), f ≠ 0 → ¬CategoryTheory.IsIso f → height x < height y)
(htau : ∀ (z : T.Nonprojective), height ↑z = height (T.tauPlus z) + 2)
{X V W Y : Ind}
(hVW : V ≠ W)
(heq : height V = height W)
(hXY : height Y = height X + 2)
(a : T.obj X ⟶ T.obj V)
(b : T.obj V ⟶ T.obj Y)
(c : T.obj X ⟶ T.obj W)
(d : T.obj W ⟶ T.obj Y)
(ha : a ≠ 0)
(hb : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism b)
(hd : ¬CategoryTheory.IsSplitEpi d)
(hsquare : CategoryTheory.CategoryStruct.comp a b = CategoryTheory.CategoryStruct.comp c d)
:
∃ (hn : ¬T.IsProjective Y), T.tauPlus ⟨Y, hn⟩ = X
The source of a square is the translate of its target when its middle objects are distinct of equal height and translation lowers height by two.