Auslander--Reiten surplus under equivalence #
An additive equivalence between abelian categories preserves the total Auslander--Reiten surplus of two finite right-tau presentations when their indecomposable labels and represented objects are matched. This is the category-independent transport lemma needed to compare finite category modules with finitely generated modules over a category algebra.
theorem
MagnitudeConjecture.FiniteTauMatrix.rightMiddleArity_eq_of_equivalence
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Abelian D]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
(T : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I)
(U : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J)
(E : C ≌ D)
[E.functor.Additive]
(labelEquiv : I ≃ J)
(objIso : (i : I) → E.functor.obj (T.obj i) ≅ U.obj (labelEquiv i))
(i : I)
:
rightMiddleArity T i = rightMiddleArity U (labelEquiv i)
Incoming right-mesh arity is preserved by an additive equivalence after matching the indecomposable endpoint labels.
theorem
MagnitudeConjecture.FiniteTauMatrix.isProjective_equivalence_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Abelian D]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
(T : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I)
(U : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J)
(E : C ≌ D)
(labelEquiv : I ≃ J)
(objIso : (i : I) → E.functor.obj (T.obj i) ≅ U.obj (labelEquiv i))
[CategoryTheory.EnoughProjectives C]
[CategoryTheory.EnoughProjectives D]
(i : I)
:
T.IsProjective i ↔ U.IsProjective (labelEquiv i)
The finite-right-tau projectivity predicate is preserved at matched indecomposable labels.
theorem
MagnitudeConjecture.FiniteTauMatrix.betaAt_eq_of_equivalence
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Abelian D]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
(T : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I)
(U : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J)
(E : C ≌ D)
[E.functor.Additive]
(labelEquiv : I ≃ J)
(objIso : (i : I) → E.functor.obj (T.obj i) ≅ U.obj (labelEquiv i))
[CategoryTheory.EnoughProjectives C]
[CategoryTheory.EnoughProjectives D]
(i : I)
:
The number of nonprojective occurrences in a right almost-split middle term is preserved at matched labels.
theorem
MagnitudeConjecture.FiniteTauMatrix.beta_le_of_equivalence
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Abelian D]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
(T : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I)
(U : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J)
(E : C ≌ D)
[E.functor.Additive]
(labelEquiv : I ≃ J)
(objIso : (i : I) → E.functor.obj (T.obj i) ≅ U.obj (labelEquiv i))
[CategoryTheory.EnoughProjectives C]
[CategoryTheory.EnoughProjectives D]
{bound : ℕ}
(h : beta T ≤ bound)
:
beta U ≤ bound
A uniform bound on the nonprojective right-middle multiplicity is transported by an additive equivalence.
theorem
MagnitudeConjecture.FiniteTauMatrix.beta_le_iff_of_equivalence
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Abelian D]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
(T : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I)
(U : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J)
(E : C ≌ D)
[E.functor.Additive]
(labelEquiv : I ≃ J)
(objIso : (i : I) → E.functor.obj (T.obj i) ≅ U.obj (labelEquiv i))
[CategoryTheory.EnoughProjectives C]
[CategoryTheory.EnoughProjectives D]
{bound : ℕ}
:
A uniform beta bound is invariant under an additive equivalence with a
bijective matching of indecomposable labels.
theorem
MagnitudeConjecture.FiniteTauMatrix.localDensity_eq_of_equivalence
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Abelian D]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
(T : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I)
(U : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J)
(E : C ≌ D)
[E.functor.Additive]
(labelEquiv : I ≃ J)
(objIso : (i : I) → E.functor.obj (T.obj i) ≅ U.obj (labelEquiv i))
[CategoryTheory.EnoughProjectives C]
[CategoryTheory.EnoughProjectives D]
(i : I)
:
ARCount.localDensity (arrowMultiplicity T) T.IsProjective i = ARCount.localDensity (arrowMultiplicity U) U.IsProjective (labelEquiv i)
Matrix local density is preserved at every matched label.
theorem
MagnitudeConjecture.FiniteTauMatrix.surplus_eq_of_equivalence
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Abelian D]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.IsIdempotentComplete D]
{I : Type w₁}
[Fintype I]
{J : Type w₂}
[Fintype J]
(T : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C I)
(U : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D J)
(E : C ≌ D)
[E.functor.Additive]
(labelEquiv : I ≃ J)
(objIso : (i : I) → E.functor.obj (T.obj i) ≅ U.obj (labelEquiv i))
[CategoryTheory.EnoughProjectives C]
[CategoryTheory.EnoughProjectives D]
:
Matched finite right-tau presentations in equivalent abelian categories have the same Auslander--Reiten surplus.