Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardIntervalIncomingDecomposition

Occurrence-preserving incoming decompositions in the control interval #

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intervalDecompQuiver {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
Quiver (Fin S.n)
Instances For
    source
    @[instance_reducible]
    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intervalDecompArrowFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : Fin S.n) :
    Fintype (x ⟶ y)
    Instances For
      source
      noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalIncomingSummand {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) (a : MeshCategory.RightMeshData.IncomingArrow z) :
      Graded.FiniteGradedModule.SupportedCategory (S.standardFormIntervalControlHeight + 2)

      Each occurrence is the shifted representative belonging to its incoming arrow.

      Instances For
        source
        noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalIncomingBicone {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) :
        CategoryTheory.Limits.Bicone (S.standardFormIntervalIncomingSummand z)

        The matrix coordinates restrict to the control interval without identifying repeated labels.

        Instances For
          source
          noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalIncomingBicone_isBilimit {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) :
          (S.standardFormIntervalIncomingBicone z).IsBilimit

          The literal incoming source is the direct sum indexed by incoming arrow occurrences.

          Instances For
            source
            noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalIncomingBiproductIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) :
            S.standardFormIntervalIncomingSource z 0 ⋯ ⋯ ≅ ⨁ S.standardFormIntervalIncomingSummand z

            The finite interval's actual incoming source decomposition retains all multiplicities.

            Instances For
              source
              theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalIncomingSummand_indecomposable {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) (a : MeshCategory.RightMeshData.IncomingArrow z) :
              CategoryTheory.Indecomposable (S.standardFormIntervalIncomingSummand z a)

              Every displayed occurrence is indecomposable in the interval.

              source
              theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalIncomingSummand_not_projective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) (a : MeshCategory.RightMeshData.IncomingArrow z) (ha : ¬CategoryTheory.Projective (S.fgObj a.fst)) :
              ¬CategoryTheory.Projective (S.standardFormIntervalIncomingSummand z a)

              Every originally nonprojective incoming occurrence stays nonprojective in the interval.