Magnitude conjecture

MagnitudeConjecture.Combinatorics.MeshMatrix

The Auslander--Reiten mesh matrix #

This file packages the signed incidence matrix used in the frozen manuscript. An arrow X ⟶ Y contributes its negative multiplicity in row X, column Y, while the mesh ending at a nonprojective vertex Y contributes 1 in row τ Y, column Y. The total sum of the entries is therefore the Auslander--Reiten Euler expression vertices - arrows + meshes.

The construction is deliberately combinatorial. A later categorical layer will identify this matrix with the inverse Hom matrix.

source
def MagnitudeConjecture.ARCount.matrixTotal {ι : Type u} [Fintype ι] {κ : Type v} [Fintype κ] (M : Matrix ι κ ℤ) :
ℤ

Sum of every entry of a finite integer matrix.

Instances For
    source
    def MagnitudeConjecture.ARCount.singletonMatrix {ι : Type u} [DecidableEq ι] (row column : ι) :
    Matrix ι ι ℤ

    A matrix with one unit entry in row row, column column.

    Instances For
      source
      def MagnitudeConjecture.ARCount.arrowMatrix {ι : Type u} (arrowMultiplicity : ι → ι → ℕ) :
      Matrix ι ι ℤ

      The signed arrow-incidence matrix. Its (X,Y) entry is the negative multiplicity of arrows X ⟶ Y.

      Instances For
        source
        def MagnitudeConjecture.ARCount.meshContribution {ι : Type u} [Fintype ι] [DecidableEq ι] (IsProjective : ι → Prop) [DecidablePred IsProjective] (tau : { Y : ι // ¬IsProjective Y } → ι) :
        Matrix ι ι ℤ

        Sum of the unit matrices contributed by the almost-split meshes.

        Instances For
          source
          def MagnitudeConjecture.ARCount.meshMatrix {ι : Type u} [Fintype ι] [DecidableEq ι] (arrowMultiplicity : ι → ι → ℕ) (IsProjective : ι → Prop) [DecidablePred IsProjective] (tau : { Y : ι // ¬IsProjective Y } → ι) :
          Matrix ι ι ℤ

          The paper-oriented Auslander--Reiten mesh matrix

          I - (arrow multiplicities) + (mesh contributions).

          Instances For
            source
            theorem MagnitudeConjecture.ARCount.matrixTotal_add {ι : Type u} [Fintype ι] {κ : Type v} [Fintype κ] (M N : Matrix ι κ ℤ) :
            matrixTotal (M + N) = matrixTotal M + matrixTotal N
            source
            theorem MagnitudeConjecture.ARCount.matrixTotal_sum {ι : Type u} [Fintype ι] {κ : Type v} [Fintype κ] {σ : Type w} [Fintype σ] (M : σ → Matrix ι κ ℤ) :
            matrixTotal (∑ k : σ, M k) = ∑ k : σ, matrixTotal (M k)
            source
            theorem MagnitudeConjecture.ARCount.matrixTotal_singletonMatrix {ι : Type u} [Fintype ι] [DecidableEq ι] (row column : ι) :
            matrixTotal (singletonMatrix row column) = 1
            source
            theorem MagnitudeConjecture.ARCount.matrixTotal_one {ι : Type u} [Fintype ι] [DecidableEq ι] :
            matrixTotal 1 = vertexCount
            source
            theorem MagnitudeConjecture.ARCount.matrixTotal_arrowMatrix {ι : Type u} [Fintype ι] (arrowMultiplicity : ι → ι → ℕ) :
            matrixTotal (arrowMatrix arrowMultiplicity) = -arrowCount arrowMultiplicity
            source
            theorem MagnitudeConjecture.ARCount.matrixTotal_meshContribution {ι : Type u} [Fintype ι] [DecidableEq ι] (IsProjective : ι → Prop) [DecidablePred IsProjective] (tau : { Y : ι // ¬IsProjective Y } → ι) :
            matrixTotal (meshContribution IsProjective tau) = meshCount IsProjective
            source
            theorem MagnitudeConjecture.ARCount.meshContribution_apply_of_projective {ι : Type u} [Fintype ι] [DecidableEq ι] (IsProjective : ι → Prop) [DecidablePred IsProjective] (tau : { Y : ι // ¬IsProjective Y } → ι) {source target : ι} (hTarget : IsProjective target) :
            meshContribution IsProjective tau source target = 0
            source
            theorem MagnitudeConjecture.ARCount.meshContribution_apply_of_nonprojective {ι : Type u} [Fintype ι] [DecidableEq ι] (IsProjective : ι → Prop) [DecidablePred IsProjective] (tau : { Y : ι // ¬IsProjective Y } → ι) {source target : ι} (hTarget : ¬IsProjective target) :
            meshContribution IsProjective tau source target = if source = tau ⟨target, hTarget⟩ then 1 else 0
            source
            theorem MagnitudeConjecture.ARCount.meshMatrix_apply_of_projective {ι : Type u} [Fintype ι] [DecidableEq ι] (arrowMultiplicity : ι → ι → ℕ) (IsProjective : ι → Prop) [DecidablePred IsProjective] (tau : { Y : ι // ¬IsProjective Y } → ι) {source target : ι} (hTarget : IsProjective target) :
            meshMatrix arrowMultiplicity IsProjective tau source target = (if source = target then 1 else 0) - ↑(arrowMultiplicity source target)
            source
            theorem MagnitudeConjecture.ARCount.meshMatrix_apply_of_nonprojective {ι : Type u} [Fintype ι] [DecidableEq ι] (arrowMultiplicity : ι → ι → ℕ) (IsProjective : ι → Prop) [DecidablePred IsProjective] (tau : { Y : ι // ¬IsProjective Y } → ι) {source target : ι} (hTarget : ¬IsProjective target) :
            meshMatrix arrowMultiplicity IsProjective tau source target = (if source = target then 1 else 0) - ↑(arrowMultiplicity source target) + if source = tau ⟨target, hTarget⟩ then 1 else 0
            source
            theorem MagnitudeConjecture.ARCount.matrixTotal_meshMatrix_eq_eulerMagnitude {ι : Type u} [Fintype ι] [DecidableEq ι] (arrowMultiplicity : ι → ι → ℕ) (IsProjective : ι → Prop) [DecidablePred IsProjective] (tau : { Y : ι // ¬IsProjective Y } → ι) :
            matrixTotal (meshMatrix arrowMultiplicity IsProjective tau) = eulerMagnitude arrowMultiplicity IsProjective

            Frozen manuscript, equation (2.1): the total entry sum of the mesh matrix is the Auslander--Reiten Euler expression.