Documentation

TauCeti.RepresentationTheory.ClassicalGroups.GelfandTsetlin.AddMonoid

The additive monoid of Gelfand-Tsetlin patterns #

The interlacing inequalities defining a Gelfand-Tsetlin pattern are homogeneous linear inequalities between entries, so patterns can be added entrywise: TauCeti.GTPattern n is an ordered cancellative commutative monoid for the pointwise addition and order of its entries. It is not a group, since negating a pattern reverses its inequalities. The polynomial patterns are the nonnegative ones for this order: those whose top weight is polynomial.

Main definitions #

Main results #

The entrywise additive monoid #

source
@[instance_reducible]
instance TauCeti.GTPattern.instZero {n : ℕ} :
Zero (GTPattern n)
source
@[instance_reducible]
instance TauCeti.GTPattern.instAdd {n : ℕ} :
Add (GTPattern n)
source
@[instance_reducible]
instance TauCeti.GTPattern.instSMulNat {n : ℕ} :
SMul ℕ (GTPattern n)
source
@[simp]
theorem TauCeti.GTPattern.coe_zero {n : ℕ} :
⇑0 = 0
source
@[simp]
theorem TauCeti.GTPattern.coe_add {n : ℕ} (P Q : GTPattern n) :
⇑(P + Q) = ⇑P + ⇑Q
source
@[simp]
theorem TauCeti.GTPattern.coe_nsmul {n : ℕ} (k : ℕ) (P : GTPattern n) :
⇑(k • P) = k • ⇑P
source
theorem TauCeti.GTPattern.zero_apply {n : ℕ} (i j : ℕ) :
0 i j = 0
source
theorem TauCeti.GTPattern.add_apply {n : ℕ} (P Q : GTPattern n) (i j : ℕ) :
(P + Q) i j = P i j + Q i j
source
theorem TauCeti.GTPattern.nsmul_apply {n : ℕ} (k : ℕ) (P : GTPattern n) (i j : ℕ) :
(k • P) i j = k • P i j
source
@[instance_reducible]
instance TauCeti.GTPattern.instAddCancelCommMonoid {n : ℕ} :
AddCancelCommMonoid (GTPattern n)

Gelfand-Tsetlin patterns form a cancellative commutative monoid under entrywise addition.

source
def TauCeti.GTPattern.coeFnAddMonoidHom {n : ℕ} :
GTPattern n →+ ℕ → ℕ → ℤ

The array of entries of a pattern, as an additive monoid homomorphism.

Instances For
    source
    @[simp]
    theorem TauCeti.GTPattern.coeFnAddMonoidHom_apply {n : ℕ} (P : GTPattern n) :
    coeFnAddMonoidHom P = ⇑P
    source
    @[simp]
    theorem TauCeti.GTPattern.coe_sum {n : ℕ} {ι : Type u_1} (s : Finset ι) (P : ι → GTPattern n) :
    ⇑(∑ i ∈ s, P i) = ∑ i ∈ s, ⇑(P i)
    source
    @[simp]
    theorem TauCeti.GTPattern.topRow_zero {n : ℕ} :
    topRow 0 = 0
    source
    @[simp]
    theorem TauCeti.GTPattern.topRow_add {n : ℕ} (P Q : GTPattern n) :
    (P + Q).topRow = P.topRow + Q.topRow
    source
    @[simp]
    theorem TauCeti.GTPattern.topRow_nsmul {n : ℕ} (k : ℕ) (P : GTPattern n) :
    (k • P).topRow = k • P.topRow

    Constant patterns #

    source
    def TauCeti.GTPattern.const (n : ℕ) (m : ℤ) :
    GTPattern n

    The constant pattern: every informative entry equals m. Adding it to a pattern is the determinant shift by m (TauCeti.GTPattern.shift_eq_add_const).

    Instances For
      source
      theorem TauCeti.GTPattern.const_apply {n : ℕ} (m : ℤ) (i j : ℕ) :
      (const n m) i j = if i < j ∧ j ≤ n then m else 0
      source
      @[simp]
      theorem TauCeti.GTPattern.const_apply_of_lt_of_le {n : ℕ} (m : ℤ) {i j : ℕ} (hij : i < j) (hj : j ≤ n) :
      (const n m) i j = m
      source
      @[simp]
      theorem TauCeti.GTPattern.topRow_const {n : ℕ} (m : ℤ) :
      (const n m).topRow = fun (x : Fin n) => m
      source
      @[simp]
      theorem TauCeti.GTPattern.const_zero {n : ℕ} :
      const n 0 = 0
      source
      theorem TauCeti.GTPattern.const_add {n : ℕ} (m m' : ℤ) :
      const n (m + m') = const n m + const n m'

      The entrywise order #

      source
      @[instance_reducible]
      instance TauCeti.GTPattern.instPartialOrder {n : ℕ} :
      PartialOrder (GTPattern n)

      Gelfand-Tsetlin patterns are ordered entrywise.

      source
      @[simp]
      theorem TauCeti.GTPattern.coe_le_coe {n : ℕ} {P Q : GTPattern n} :
      ⇑P ≤ ⇑Q ↔ P ≤ Q
      source
      theorem TauCeti.GTPattern.le_def {n : ℕ} {P Q : GTPattern n} :
      P ≤ Q ↔ ∀ (i j : ℕ), P i j ≤ Q i j
      source
      instance TauCeti.GTPattern.instIsOrderedCancelAddMonoid {n : ℕ} :
      IsOrderedCancelAddMonoid (GTPattern n)

      The entrywise order is compatible with entrywise addition.

      source
      theorem TauCeti.GTPattern.zero_le_iff {n : ℕ} {P : GTPattern n} :
      0 ≤ P ↔ ∀ (i j : ℕ), 0 ≤ P i j
      source
      theorem TauCeti.GTPattern.zero_le_iff_topRow {n : ℕ} {P : GTPattern n} :
      0 ≤ P ↔ ∀ (i : Fin n), 0 ≤ P.topRow i

      A pattern is nonnegative exactly when its top row is: every entry dominates an entry of the top row.

      source
      theorem TauCeti.GTPattern.zero_le_iff_isPolynomial {n : ℕ} {P : GTPattern n} :
      0 ≤ P ↔ P.topWeight.IsPolynomial

      The nonnegative patterns are those whose top weight is polynomial.