Magnitude conjecture

MagnitudeConjecture.CategoryTheory.DeckOrbitTowerFiniteSkeleton

Finite indecomposable skeletons over orbit towers #

An additive equivalence of finite-dimensional module categories transports a duplicate-free complete indecomposable skeleton without changing its label type. The strict orbit-tower module equivalence therefore gives the two-stage quotient a skeleton with exactly the direct quotient's coordinates.

source
noncomputable def MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.mapEquivalence {k : Type v} [Field k] {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (S : FiniteDimensionalModuleIndecomposableSkeleton) (e : FiniteDimensionalModuleCategory k ≌ FiniteDimensionalModuleCategory k) [e.functor.Additive] :
FiniteDimensionalModuleIndecomposableSkeleton

Transport a finite complete indecomposable skeleton along an additive equivalence of finite-dimensional module categories.

Instances For
    source
    theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.rightMiddleArity_mapEquivalence {k : Type v} [Field k] {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (S : FiniteDimensionalModuleIndecomposableSkeleton) (e : FiniteDimensionalModuleCategory k ≌ FiniteDimensionalModuleCategory k) [e.functor.Additive] [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] (i : Fin S.n) :
    FiniteTauMatrix.rightMiddleArity (S.mapEquivalence e).toFiniteRightTauCategoryData i = FiniteTauMatrix.rightMiddleArity S.toFiniteRightTauCategoryData i

    Incoming right-mesh arity is preserved when a finite indecomposable skeleton is transported along an additive equivalence.

    source
    theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.isProjective_mapEquivalence_iff {k : Type v} [Field k] {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (S : FiniteDimensionalModuleIndecomposableSkeleton) (e : FiniteDimensionalModuleCategory k ≌ FiniteDimensionalModuleCategory k) [e.functor.Additive] [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] (i : Fin S.n) :
    (S.mapEquivalence e).toFiniteRightTauCategoryData.IsProjective i ↔ S.toFiniteRightTauCategoryData.IsProjective i

    The finite-right-tau projectivity predicate is preserved when a finite indecomposable skeleton is transported along an additive equivalence.

    source
    theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.rightTauLocalDensity_mapEquivalence {k : Type v} [Field k] {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (S : FiniteDimensionalModuleIndecomposableSkeleton) (e : FiniteDimensionalModuleCategory k ≌ FiniteDimensionalModuleCategory k) [e.functor.Additive] [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] (i : Fin S.n) :
    (S.mapEquivalence e).rightTauLocalDensity i = S.rightTauLocalDensity i

    Right-tau local density is preserved labelwise under transport of the finite indecomposable skeleton along an additive equivalence.

    source
    theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.surplus_mapEquivalence {k : Type v} [Field k] {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (S : FiniteDimensionalModuleIndecomposableSkeleton) (e : FiniteDimensionalModuleCategory k ≌ FiniteDimensionalModuleCategory k) [e.functor.Additive] [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] :
    ARCount.surplus (FiniteTauMatrix.arrowMultiplicity (S.mapEquivalence e).toFiniteRightTauCategoryData) (S.mapEquivalence e).toFiniteRightTauCategoryData.IsProjective = ARCount.surplus (FiniteTauMatrix.arrowMultiplicity S.toFiniteRightTauCategoryData) S.toFiniteRightTauCategoryData.IsProjective

    Transporting a complete finite indecomposable skeleton along an additive equivalence preserves its Auslander--Reiten surplus.

    source
    theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.surplus_eq_of_equivalence {k : Type v} [Field k] {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (S : FiniteDimensionalModuleIndecomposableSkeleton) (e : FiniteDimensionalModuleCategory k ≌ FiniteDimensionalModuleCategory k) [e.functor.Additive] [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] (T : FiniteDimensionalModuleIndecomposableSkeleton) :
    ARCount.surplus (FiniteTauMatrix.arrowMultiplicity T.toFiniteRightTauCategoryData) T.toFiniteRightTauCategoryData.IsProjective = ARCount.surplus (FiniteTauMatrix.arrowMultiplicity S.toFiniteRightTauCategoryData) S.toFiniteRightTauCategoryData.IsProjective

    Any two complete indecomposable skeletons related by an additive equivalence of finite-dimensional module categories have the same Auslander--Reiten surplus.

    source
    noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitTowerIndecomposableSkeleton {k : Type (max v w)} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {G : Type w} [Group G] [MulAction G C] [CategoryTheory.Linear k C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (N : Subgroup G) [N.Normal] :
    FiniteDimensionalModuleIndecomposableSkeleton → FiniteDimensionalModuleIndecomposableSkeleton

    Transport a direct strict-orbit indecomposable skeleton to the two-stage strict orbit tower, retaining the same finite label type.

    Instances For
      source
      theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitTowerIndecomposableSkeleton_rightTauLocalDensity {k : Type (max v w)} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {G : Type w} [Group G] [MulAction G C] [CategoryTheory.Linear k C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (N : Subgroup G) [N.Normal] [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] (S : FiniteDimensionalModuleIndecomposableSkeleton) (i : Fin S.n) :
      (D.deckOrbitTowerIndecomposableSkeleton N S).rightTauLocalDensity i = S.rightTauLocalDensity i

      Transport through the strict orbit-tower equivalence preserves the right-tau local density at every retained skeleton label.

      source
      theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.sum_rightTauLocalDensity_eq_deckOrbitTower {k : Type (max v w)} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {G : Type w} [Group G] [MulAction G C] [CategoryTheory.Linear k C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (N : Subgroup G) [N.Normal] [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] (S : FiniteDimensionalModuleIndecomposableSkeleton) (T : FiniteDimensionalModuleIndecomposableSkeleton) :
      ∑ j : Fin T.n, T.rightTauLocalDensity j = ∑ i : Fin S.n, S.rightTauLocalDensity i

      Every complete indecomposable skeleton on the two-stage strict orbit has the same total right-tau local density as every complete skeleton on the direct strict orbit.