Magnitude conjecture

MagnitudeConjecture.LinearAlgebra.UpperTriangularWeakPositivity

Weak positivity makes an upper-triangular Cartan matrix thin #

For a nonnegative upper-unitriangular integral Cartan matrix, weak positivity of the inverse-Cartan quadratic form forces every matrix entry to be at most one. The proof truncates a projective column at a chosen row and subtracts the corresponding unit vector.

source
def MagnitudeConjecture.CartanCoordinate.WeaklyPositiveCartanData.columnTail {ι : Type u} [LinearOrder ι] (C : Matrix ι ι ℤ) (i j : ι) :
ι → ℤ

The tail of a Cartan column beginning at a chosen index.

Instances For
    source
    theorem MagnitudeConjecture.CartanCoordinate.WeaklyPositiveCartanData.inverse_blockTriangular {ι : Type u} [Fintype ι] [DecidableEq ι] [LinearOrder ι] (D : WeaklyPositiveCartanData) (hC : D.C.BlockTriangular id) :
    D.Cinv.BlockTriangular id
    source
    theorem MagnitudeConjecture.CartanCoordinate.WeaklyPositiveCartanData.inverse_diagonal_eq_one {ι : Type u} [Fintype ι] [DecidableEq ι] [LinearOrder ι] (D : WeaklyPositiveCartanData) (hC : D.C.BlockTriangular id) (i : ι) :
    D.Cinv i i = 1
    source
    theorem MagnitudeConjecture.CartanCoordinate.WeaklyPositiveCartanData.inverse_mulVec_columnTail {ι : Type u} [Fintype ι] [DecidableEq ι] [LinearOrder ι] (D : WeaklyPositiveCartanData) (hC : D.C.BlockTriangular id) {i j t : ι} (hit : i ≤ t) :
    D.Cinv.mulVec (columnTail D.C i j) t = Pi.single j 1 t
    source
    theorem MagnitudeConjecture.CartanCoordinate.WeaklyPositiveCartanData.quadraticForm_columnTail {ι : Type u} [Fintype ι] [DecidableEq ι] [LinearOrder ι] (D : WeaklyPositiveCartanData) (hC : D.C.BlockTriangular id) {i j : ι} (hij : i ≤ j) :
    quadraticForm D.Cinv (columnTail D.C i j) = 1
    source
    theorem MagnitudeConjecture.CartanCoordinate.WeaklyPositiveCartanData.columnTail_dot_inverse_unit {ι : Type u} [Fintype ι] [DecidableEq ι] [LinearOrder ι] (D : WeaklyPositiveCartanData) (hC : D.C.BlockTriangular id) (i j : ι) :
    columnTail D.C i j ⬝ᵥ D.Cinv.mulVec (Pi.single i 1) = D.C i j
    source
    theorem MagnitudeConjecture.CartanCoordinate.WeaklyPositiveCartanData.entry_le_one_of_blockTriangular {ι : Type u} [Fintype ι] [DecidableEq ι] [LinearOrder ι] (D : WeaklyPositiveCartanData) (hC : D.C.BlockTriangular id) (i j : ι) :
    D.C i j ≤ 1

    Every entry of a nonnegative upper-unitriangular weakly positive Cartan matrix is zero or one.