The Cartan quadratic-form coordinate estimate

This file formalizes the numerical heart of Appendix A in the frozen manuscript. For a nonnegative unimodular integral Cartan matrix with weakly positive quadratic form, a positive root and its positive Coxeter transform differ by at most one in every coordinate.

The module-theoretic application must still construct this data and identify dimension vectors along Auslander--Reiten translation. No such facts are assumed here under representation-theoretic names.

def MagnitudeConjecture.CartanCoordinate.quadraticForm {ι : Type u} [Fintype ι] (Cinv : Matrix ι ι ℤ) (x : ι → ℤ) : ℤ

The integral quadratic form represented by an inverse Cartan matrix.

def MagnitudeConjecture.CartanCoordinate.projectiveRoot {ι : Type u} (C : Matrix ι ι ℤ) (a : ι) : ι → ℤ

The projective root belonging to a Cartan index.

def MagnitudeConjecture.CartanCoordinate.coxeterMatrix {ι : Type u} [Fintype ι] (C Cinv : Matrix ι ι ℤ) : Matrix ι ι ℤ

The Coxeter matrix in the row-vector convention of the manuscript.

def MagnitudeConjecture.CartanCoordinate.inverseCoxeterMatrix {ι : Type u} [Fintype ι] (C Cinv : Matrix ι ι ℤ) : Matrix ι ι ℤ

The inverse Coxeter matrix.

def MagnitudeConjecture.CartanCoordinate.IsPositive {ι : Type u} (x : ι → ℤ) : Prop

A positive integral vector: coordinatewise nonnegative and nonzero.

structure MagnitudeConjecture.CartanCoordinate.WeaklyPositiveCartanData {ι : Type u} [Fintype ι] [DecidableEq ι] : Type u

Exact integral Cartan-form input used in the quadratic proof.

• C : Matrix ι ι ℤ
• Cinv : Matrix ι ι ℤ
• inverse_mul : self.Cinv * self.C = 1
• mul_inverse : self.C * self.Cinv = 1
• diagonal (i : ι) : self.C i i = 1
• nonnegative (i j : ι) : 0 ≤ self.C i j
• weaklyPositive (x : ι → ℤ) : IsPositive x → 1 ≤ quadraticForm self.Cinv x

def MagnitudeConjecture.CartanCoordinate.WeaklyPositiveCartanData.coxeter {ι : Type u} [Fintype ι] [DecidableEq ι] (D : WeaklyPositiveCartanData) : Matrix ι ι ℤ

The Coxeter transformation attached to the data.

def MagnitudeConjecture.CartanCoordinate.WeaklyPositiveCartanData.coxeterInv {ι : Type u} [Fintype ι] [DecidableEq ι] (D : WeaklyPositiveCartanData) : Matrix ι ι ℤ

The inverse Coxeter transformation attached to the data.

theorem MagnitudeConjecture.CartanCoordinate.WeaklyPositiveCartanData.quadraticForm_add {ι : Type u} [Fintype ι] (Cinv : Matrix ι ι ℤ) (x y : ι → ℤ) : quadraticForm Cinv (x + y) = quadraticForm Cinv x + quadraticForm Cinv y + x ⬝ᵥ Cinv.mulVec y + y ⬝ᵥ Cinv.mulVec x

Polarization of the integral quadratic form.

theorem MagnitudeConjecture.CartanCoordinate.WeaklyPositiveCartanData.crossTerm_projectiveRoot {ι : Type u} [Fintype ι] [DecidableEq ι] (C Cinv : Matrix ι ι ℤ) (hinv : Cinv * C = 1) (x : ι → ℤ) (a : ι) : x ⬝ᵥ Cinv.mulVec (projectiveRoot C a) + projectiveRoot C a ⬝ᵥ Cinv.mulVec x = x a - Matrix.vecMul x (coxeterMatrix C Cinv) a

The polarized pairing with a projective root is the coordinate change under the Coxeter transformation.

theorem MagnitudeConjecture.CartanCoordinate.WeaklyPositiveCartanData.projectiveRoot_positive {ι : Type u} [Fintype ι] [DecidableEq ι] (D : WeaklyPositiveCartanData) (a : ι) : IsPositive (projectiveRoot D.C a)

Every Cartan column is a positive integral vector.

theorem MagnitudeConjecture.CartanCoordinate.WeaklyPositiveCartanData.projectiveRoot_quadraticForm {ι : Type u} [Fintype ι] [DecidableEq ι] (D : WeaklyPositiveCartanData) (a : ι) : quadraticForm D.Cinv (projectiveRoot D.C a) = 1

Every Cartan column is a root of the quadratic form.

theorem MagnitudeConjecture.CartanCoordinate.WeaklyPositiveCartanData.coxeter_apply_le_add_one {ι : Type u} [Fintype ι] [DecidableEq ι] (D : WeaklyPositiveCartanData) (x : ι → ℤ) (hxpos : IsPositive x) (hxroot : quadraticForm D.Cinv x = 1) (a : ι) : Matrix.vecMul x D.coxeter a ≤ x a + 1

Forward half of the quadratic estimate: a positive root changes upward by at most one under the Coxeter transformation.

theorem MagnitudeConjecture.CartanCoordinate.WeaklyPositiveCartanData.coxeter_mul_coxeterInv {ι : Type u} [Fintype ι] [DecidableEq ι] (D : WeaklyPositiveCartanData) : D.coxeter * D.coxeterInv = 1

The displayed Coxeter inverse is a right inverse.

theorem MagnitudeConjecture.CartanCoordinate.WeaklyPositiveCartanData.coxeter_mul_Cinv_mul_transpose {ι : Type u} [Fintype ι] [DecidableEq ι] (D : WeaklyPositiveCartanData) : D.coxeter * D.Cinv * D.coxeter.transpose = D.Cinv

The Coxeter transformation preserves the inverse-Cartan bilinear matrix.

theorem MagnitudeConjecture.CartanCoordinate.WeaklyPositiveCartanData.quadraticForm_coxeter {ι : Type u} [Fintype ι] [DecidableEq ι] (D : WeaklyPositiveCartanData) (x : ι → ℤ) : quadraticForm D.Cinv (Matrix.vecMul x D.coxeter) = quadraticForm D.Cinv x

The inverse-Cartan quadratic form is invariant under the Coxeter transformation.

theorem MagnitudeConjecture.CartanCoordinate.WeaklyPositiveCartanData.vecMul_coxeter_coxeterInv {ι : Type u} [Fintype ι] [DecidableEq ι] (D : WeaklyPositiveCartanData) (x : ι → ℤ) : Matrix.vecMul (Matrix.vecMul x D.coxeter) D.coxeterInv = x

Applying the Coxeter transformation and then its displayed inverse returns the original row vector.

theorem MagnitudeConjecture.CartanCoordinate.WeaklyPositiveCartanData.quadraticForm_transpose {ι : Type u} [Fintype ι] (M : Matrix ι ι ℤ) (x : ι → ℤ) : quadraticForm M.transpose x = quadraticForm M x

Transposing the inverse matrix leaves its quadratic form unchanged.

def MagnitudeConjecture.CartanCoordinate.WeaklyPositiveCartanData.transpose {ι : Type u} [Fintype ι] [DecidableEq ι] (D : WeaklyPositiveCartanData) : WeaklyPositiveCartanData

The opposite Cartan matrix carries the transposed weakly positive Cartan data.

@[simp]

theorem MagnitudeConjecture.CartanCoordinate.WeaklyPositiveCartanData.transpose_coxeter {ι : Type u} [Fintype ι] [DecidableEq ι] (D : WeaklyPositiveCartanData) : D.transpose.coxeter = D.coxeterInv

theorem MagnitudeConjecture.CartanCoordinate.WeaklyPositiveCartanData.coxeter_coordinate_abs_sub_le_one {ι : Type u} [Fintype ι] [DecidableEq ι] (D : WeaklyPositiveCartanData) (x : ι → ℤ) (hxpos : IsPositive x) (hxroot : quadraticForm D.Cinv x = 1) (hypos : IsPositive (Matrix.vecMul x D.coxeter)) (hyroot : quadraticForm D.Cinv (Matrix.vecMul x D.coxeter) = 1) (a : ι) : |x a - Matrix.vecMul x D.coxeter a| ≤ 1

Quadratic-form form of the coordinate estimate. If both x and its Coxeter transform are positive roots, every coordinate changes by at most one.

structure MagnitudeConjecture.CartanCoordinate.LocalRootPairCoordinateData (a b : ℤ) : Type (u + 1)

Local numerical data for one coordinate of a positive-root pair related by a Coxeter transformation.

This wrapper is designed for the support-restriction argument in Appendix A of the frozen manuscript. The finite index type and Cartan form may depend on the Auslander--Reiten sequence: no ambient weak-positivity statement is built into the interface.

• index : Type u
• indexFintype : Fintype self.index
• indexDecidableEq : DecidableEq self.index
• cartan : WeaklyPositiveCartanData
• root : self.index → ℤ
• root_positive : IsPositive self.root
• root_quadraticForm : quadraticForm self.cartan.Cinv self.root = 1
• transform_positive : IsPositive (Matrix.vecMul self.root self.cartan.coxeter)
• transform_quadraticForm : quadraticForm self.cartan.Cinv (Matrix.vecMul self.root self.cartan.coxeter) = 1
• coordinate : self.index
• root_coordinate : self.root self.coordinate = a
• transform_coordinate : Matrix.vecMul self.root self.cartan.coxeter self.coordinate = b

theorem MagnitudeConjecture.CartanCoordinate.LocalRootPairCoordinateData.abs_sub_le_one {a b : ℤ} (D : LocalRootPairCoordinateData a b) : |a - b| ≤ 1

The local positive-root package implies the manuscript's bound for its identified coordinate.