English
Let P be an EmbeddedG2 root-pairing on a finite index set. For a fixed i, the integer-valued pairing with the composite root twoShortAddLong P decomposes as a linear combination of the pairings with short P and with long P: P.pairingIn Z i (twoShortAddLong P) = 2 · P.pairingIn Z i (short P) + 3 · P.pairingIn Z i (long P).
Русский
Пусть P задаёт вложенный корневой парыжинг для G2, индекс в конечном множестве. Для фиксированного i целостное число-скалярного скалярного сопряжения с корнем twoShortAddLong P является линейной комбинацией сопряжений с short P и long P: P.pairingIn ℤ i (twoShortAddLong P) = 2 · P.pairingIn ℤ i (short P) + 3 · P.pairingIn ℤ i (long P).
LaTeX
$$$P\,\mathrm{pairingIn}\,\mathbb{Z}\, i\, (\text{twoShortAddLong }P) = 2 \cdot P\,\mathrm{pairingIn}\,\mathbb{Z}\, i\, (\text{short }P) + 3 \cdot P\,\mathrm{pairingIn}\,\mathbb{Z}\, i\, (\text{long }P)$$$
Lean4
@[simp]
theorem pairingIn_twoShortAddLong_right :
P.pairingIn ℤ i (twoShortAddLong P) = 2 * P.pairingIn ℤ i (short P) + 3 * P.pairingIn ℤ i (long P) :=
by
suffices P.pairing i (twoShortAddLong P) = 2 * P.pairing i (short P) + 3 * P.pairing i (long P) from
algebraMap_injective ℤ R <| by simpa only [algebraMap_pairingIn, map_add, map_mul, map_ofNat]
have : Fintype ι := Fintype.ofFinite ι
have B := (P.posRootForm ℤ).toInvariantForm
apply mul_right_cancel₀ (B.ne_zero <| twoShortAddLong P)
calc
P.pairing i (twoShortAddLong P) * B.form (twoShortAddLongRoot P) (twoShortAddLongRoot P)
_ = 2 * B.form (P.root i) (twoShortAddLongRoot P) := ?_
_ = 2 * (2 * B.form (P.root i) (shortRoot P)) + 2 * B.form (P.root i) (longRoot P) := ?_
_ =
2 * P.pairing i (short P) * B.form (shortRoot P) (shortRoot P) +
P.pairing i (long P) * B.form (longRoot P) (longRoot P) :=
?_
_ =
(2 * P.pairing i (short P) + 3 * P.pairing i (long P)) *
B.form (twoShortAddLongRoot P) (twoShortAddLongRoot P) :=
?_
· rw [B.two_mul_apply_root_root]
· rw [twoShortAddLongRoot_eq, map_add, mul_add, map_smul, smul_eq_mul]
· rw [B.two_mul_apply_root_root, B.two_mul_apply_root_root, mul_assoc]
· rw [long_eq_three_mul_short, twoShortAddLongRoot_shortRoot]; ring
