Magnitude conjecture

MagnitudeConjecture.CategoryTheory.FiniteSkeletonShiftAction

source
noncomputable def MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.shiftLabel {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [CategoryTheory.HasShift (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) a).Additive] (S : FiniteDimensionalModuleIndecomposableSkeleton) (g : G) (i : Fin S.n) :
Fin S.n

The skeleton label representing the inverse shift of a chosen indecomposable. The inverse makes this a left group action on labels.

Instances For
    source
    noncomputable def MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.shiftLabelIso {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [CategoryTheory.HasShift (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) a).Additive] (S : FiniteDimensionalModuleIndecomposableSkeleton) (g : G) (i : Fin S.n) :
    (CategoryTheory.shiftFunctor (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) (Additive.ofMul g⁻¹)).obj (S.obj i) ≅ S.obj (S.shiftLabel g i)

    Chosen identification of a shifted indecomposable with its strict skeleton representative.

    Instances For
      source
      @[simp]
      theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.shiftLabel_one {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [CategoryTheory.HasShift (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) a).Additive] (S : FiniteDimensionalModuleIndecomposableSkeleton) (i : Fin S.n) :
      S.shiftLabel 1 i = i
      source
      theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.shiftLabel_mul {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [CategoryTheory.HasShift (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) a).Additive] (S : FiniteDimensionalModuleIndecomposableSkeleton) (g h : G) (i : Fin S.n) :
      S.shiftLabel (g * h) i = S.shiftLabel g (S.shiftLabel h i)
      source
      @[implicit_reducible]
      noncomputable def MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.labelMulAction {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [CategoryTheory.HasShift (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) a).Additive] (S : FiniteDimensionalModuleIndecomposableSkeleton) :
      MulAction G (Fin S.n)

      A coherent shift becomes a strict action on the labels of a duplicate-free indecomposable skeleton.

      Instances For
        source
        @[implicit_reducible]
        noncomputable def MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.labelOrbitFintype {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [CategoryTheory.HasShift (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) a).Additive] (S : FiniteDimensionalModuleIndecomposableSkeleton) :
        Fintype (MulAction.orbitRel.Quotient G (Fin S.n))

        The finite orbit quotient of the strict skeleton-label action.

        Instances For
          source
          def MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.IsShiftFreeOnLabels {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [CategoryTheory.HasShift (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) (Additive G)] (S : FiniteDimensionalModuleIndecomposableSkeleton) :
          Prop

          Freeness of the coherent shift on the represented isomorphism classes.

          Instances For
            source
            theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.indecomposable_trivialStabilizer_of_isShiftFreeOnLabels {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [CategoryTheory.HasShift (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) (Additive G)] (S : FiniteDimensionalModuleIndecomposableSkeleton) (hfree : S.IsShiftFreeOnLabels) (X : MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) (hX : CategoryTheory.Indecomposable X) (a : Additive G) :
            Nonempty (X ≅ (CategoryTheory.shiftFunctor (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) a).obj X) → a = 0

            Freeness on the labels of a complete skeleton gives a trivial shift stabilizer for every indecomposable object in the ambient module category.

            source
            theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.labelMulAction_isCancelSMul {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [CategoryTheory.HasShift (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) a).Additive] (S : FiniteDimensionalModuleIndecomposableSkeleton) (hfree : S.IsShiftFreeOnLabels) :
            IsCancelSMul G (Fin S.n)

            A shift free on represented isomorphism classes induces a free strict action on skeleton labels.

            source
            noncomputable def MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.rightTauLocalDensity {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteDimensionalModuleIndecomposableSkeleton) [CategoryTheory.EnoughProjectives (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k)] (i : Fin S.n) :
            ℤ

            Local density of a strict indecomposable skeleton label.

            Instances For
              source
              theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.sum_rightTauLocalDensity_eq_surplus {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteDimensionalModuleIndecomposableSkeleton) [CategoryTheory.EnoughProjectives (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k)] :
              ∑ i : Fin S.n, S.rightTauLocalDensity i = ARCount.surplus (FiniteTauMatrix.arrowMultiplicity (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.rightTauData✝ S)) (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.rightTauData✝ S).IsProjective

              The total right-tau local density of a finite indecomposable skeleton is its Auslander--Reiten surplus.

              source
              theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.rightMiddleArity_shiftLabel {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [CategoryTheory.HasShift (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) a).Additive] (S : FiniteDimensionalModuleIndecomposableSkeleton) [CategoryTheory.EnoughProjectives (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k)] (g : G) (i : Fin S.n) :
              FiniteTauMatrix.rightMiddleArity (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.rightTauData✝ S) (S.shiftLabel g i) = FiniteTauMatrix.rightMiddleArity (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.rightTauData✝ S) i

              Incoming right-mesh arity is invariant under the strict skeleton-label action induced by shifts.

              source
              theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.isProjective_shiftLabel_iff {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [CategoryTheory.HasShift (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) a).Additive] (S : FiniteDimensionalModuleIndecomposableSkeleton) [CategoryTheory.EnoughProjectives (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k)] (g : G) (i : Fin S.n) :
              (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.rightTauData✝ S).IsProjective (S.shiftLabel g i) ↔ (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.rightTauData✝ S).IsProjective i

              The finite-right-tau projectivity predicate is invariant under the strict skeleton-label action induced by shifts.

              source
              theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.occurrenceLocalDensity_shiftLabel {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [CategoryTheory.HasShift (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) a).Additive] (S : FiniteDimensionalModuleIndecomposableSkeleton) [CategoryTheory.EnoughProjectives (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k)] (g : G) (i : Fin S.n) :
              CoveringAction.occurrenceLocalDensity (FiniteTauMatrix.rightArrowTarget (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.rightTauData✝ S)) (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.rightTauData✝ S).IsProjective (S.shiftLabel g i) = CoveringAction.occurrenceLocalDensity (FiniteTauMatrix.rightArrowTarget (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.rightTauData✝ S)) (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.rightTauData✝ S).IsProjective i

              The canonical finite-right-tau local density is invariant under the strict skeleton-label action induced by shifts.

              source
              theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.rightTauLocalDensity_shiftLabel {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [CategoryTheory.HasShift (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) a).Additive] (S : FiniteDimensionalModuleIndecomposableSkeleton) [CategoryTheory.EnoughProjectives (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k)] (g : G) (i : Fin S.n) :
              S.rightTauLocalDensity (S.shiftLabel g i) = S.rightTauLocalDensity i
              source
              theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.rightTauLocalDensity_smul {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [CategoryTheory.HasShift (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) a).Additive] (S : FiniteDimensionalModuleIndecomposableSkeleton) [CategoryTheory.EnoughProjectives (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k)] (g : G) (i : Fin S.n) :
              S.rightTauLocalDensity (g • i) = S.rightTauLocalDensity i

              Action-form version of local-density invariance.

              source
              theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.sum_occurrenceLocalDensity_eq_card_mul_orbitSum {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [CategoryTheory.HasShift (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k) a).Additive] (S : FiniteDimensionalModuleIndecomposableSkeleton) [CategoryTheory.EnoughProjectives (MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ModuleCategory✝ C k)] [Fintype G] (hfree : S.IsShiftFreeOnLabels) :
              ∑ i : Fin S.n, S.rightTauLocalDensity i = ↑(Fintype.card G) * ∑ q : MulAction.orbitRel.Quotient G (Fin S.n), CoveringAction.orbitInvariantDescend S.rightTauLocalDensity ⋯ q

              Total finite-right-tau local density scales over the free quotient of the strict skeleton-label action.