chainBotCoeff_add_chainTopCoeff_le_three

English

There is a correspondence between RootPairing P and its flip, a RootPairing on the swapped modules M and N, preserving the pairing structure.

Русский

Существует соответствие между RootPairing P и его переворотом flip, который располагается на swapped модулях M и N, сохраняющее структуру пары.

LaTeX

$$$$ P.flip : RootPairing \; ι \; R \; N \; M $$$$

Lean4

theorem chainBotCoeff_add_chainTopCoeff_le_three [P.IsReduced] : P.chainBotCoeff i j + P.chainTopCoeff i j ≤ 3 :=
  by
  by_cases h : LinearIndependent R ![P.root i, P.root j]
  swap; · simp [chainTopCoeff_of_not_linearIndependent, chainBotCoeff_of_not_linearIndependent, h]
  rw [← Int.ofNat_le, Nat.cast_add, Nat.cast_ofNat, chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx h]
  have := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed i (P.chainTopIdx i j)
  aesop

Похожие утверждения