Magnitude conjecture

MagnitudeConjecture.Combinatorics.EulerSurplus

Auslander--Reiten Euler counts and surplus #

This file formalizes the first numerical reduction in the frozen manuscript. For a finite Auslander--Reiten vertex type, the almost-split meshes are indexed by the nonprojective vertices. Hence

mesh count = vertex count - projective count.

If the projective count is the number of simple modules and magnitude is given by the Auslander--Reiten Euler characteristic vertices - arrows + meshes, its surplus over the number of simples is 2 * meshes - arrows.

source
def MagnitudeConjecture.ARCount.vertexCount {ι : Type u} [Fintype ι] :
ℤ

Number of vertices, regarded as an integer for Euler calculations.

Instances For
    source
    def MagnitudeConjecture.ARCount.arrowCount {ι : Type u} [Fintype ι] (arrowMultiplicity : ι → ι → ℕ) :
    ℤ

    Total arrow multiplicity of a finite directed multigraph.

    Instances For
      source
      def MagnitudeConjecture.ARCount.indegree {ι : Type u} [Fintype ι] (arrowMultiplicity : ι → ι → ℕ) (target : ι) :
      ℤ

      Total incoming arrow multiplicity at one vertex.

      Instances For
        source
        def MagnitudeConjecture.ARCount.projectiveCount {ι : Type u} [Fintype ι] (IsProjective : ι → Prop) [DecidablePred IsProjective] :
        ℤ

        Number of projective vertices. In the module-category specialization this is the number of simple modules.

        Instances For
          source
          def MagnitudeConjecture.ARCount.meshCount {ι : Type u} [Fintype ι] (IsProjective : ι → Prop) [DecidablePred IsProjective] :
          ℤ

          Number of almost-split meshes, indexed by nonprojective vertices.

          Instances For
            source
            def MagnitudeConjecture.ARCount.eulerMagnitude {ι : Type u} [Fintype ι] (arrowMultiplicity : ι → ι → ℕ) (IsProjective : ι → Prop) [DecidablePred IsProjective] :
            ℤ

            The Auslander--Reiten Euler expression for magnitude.

            Instances For
              source
              def MagnitudeConjecture.ARCount.surplus {ι : Type u} [Fintype ι] (arrowMultiplicity : ι → ι → ℕ) (IsProjective : ι → Prop) [DecidablePred IsProjective] :
              ℤ

              Magnitude minus the number of simple modules, represented here by the number of projective vertices.

              Instances For
                source
                def MagnitudeConjecture.ARCount.localDensity {ι : Type u} [Fintype ι] (arrowMultiplicity : ι → ι → ℕ) (IsProjective : ι → Prop) [DecidablePred IsProjective] (X : ι) :
                ℤ

                Local density used in the finite-control covering argument: twice the nonprojective indicator minus total incoming arrow multiplicity.

                Instances For
                  source
                  theorem MagnitudeConjecture.ARCount.sum_indegree_eq_arrowCount {ι : Type u} [Fintype ι] (arrowMultiplicity : ι → ι → ℕ) :
                  ∑ X : ι, indegree arrowMultiplicity X = arrowCount arrowMultiplicity

                  Incoming multiplicities sum to the total arrow multiplicity.

                  source
                  theorem MagnitudeConjecture.ARCount.sum_nonprojectiveIndicator_eq_meshCount {ι : Type u} [Fintype ι] (IsProjective : ι → Prop) [DecidablePred IsProjective] :
                  (∑ X : ι, if IsProjective X then 0 else 1) = meshCount IsProjective

                  The sum of nonprojective indicators is the number of meshes.

                  source
                  theorem MagnitudeConjecture.ARCount.sum_projectiveIndicator_eq_projectiveCount {ι : Type u} [Fintype ι] (IsProjective : ι → Prop) [DecidablePred IsProjective] :
                  (∑ X : ι, if IsProjective X then 1 else 0) = projectiveCount IsProjective

                  The sum of projective indicators is the number of projective vertices.

                  source
                  theorem MagnitudeConjecture.ARCount.vertexCount_eq_projectiveCount_add_meshCount {ι : Type u} [Fintype ι] (IsProjective : ι → Prop) [DecidablePred IsProjective] :
                  vertexCount = projectiveCount IsProjective + meshCount IsProjective

                  Projective and nonprojective vertices partition the finite AR vertex set.

                  source
                  theorem MagnitudeConjecture.ARCount.surplus_eq_two_mul_meshCount_sub_arrowCount {ι : Type u} [Fintype ι] (arrowMultiplicity : ι → ι → ℕ) (IsProjective : ι → Prop) [DecidablePred IsProjective] :
                  surplus arrowMultiplicity IsProjective = 2 * meshCount IsProjective - arrowCount arrowMultiplicity

                  Frozen manuscript, equations (2.1)--(2.2): the magnitude surplus is twice the number of meshes minus the total arrow multiplicity.

                  source
                  theorem MagnitudeConjecture.ARCount.sum_localDensity_eq_surplus {ι : Type u} [Fintype ι] (arrowMultiplicity : ι → ι → ℕ) (IsProjective : ι → Prop) [DecidablePred IsProjective] :
                  ∑ X : ι, localDensity arrowMultiplicity IsProjective X = surplus arrowMultiplicity IsProjective

                  Frozen manuscript, local-density formula: summing the vertexwise density recovers the Auslander--Reiten surplus.