English
The bracket of h_j with f_i equals minus CartanMatrix_{ij} times f_i.
Русский
Скобка [h_j, f_i] равна минус CartanMatrix_{ij} умноженное на f_i.
LaTeX
$$$\\,[h_j, f_i\\] = -\\mathrm{cartanMatrix}_{ij}\\, f_i$$$
Lean4
theorem isNotG2 : P.IsNotG2 :=
by
have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
have : NoZeroSMulDivisors ℤ M := .int_of_charZero R M
rw [← P.not_isG2_iff_isNotG2]
intro contra
obtain ⟨n, h₃⟩ := h₃
obtain ⟨x, y, h₀⟩ : ∃ x y : ℤ, x • P.root i + y • P.root j = P.root k :=
by
rw [← Submodule.mem_span_pair, IsG2.span_eq_rootSpan_int hi hj hij]
exact Submodule.subset_span (mem_range_self k)
let s : Set ℤ := {-3, -1, 0, 1, 3}
let A : ℤ := P.pairingIn ℤ j i
have hki : P.root k ≠ P.root i := fun contra ↦
by
replace h₁ : 2 • P.root i = P.root l := by rwa [contra, ← two_nsmul] at h₁
exact P.nsmul_notMem_range_root ⟨_, h₁.symm⟩
have hki' : P.root k ≠ -P.root i := fun contra ↦
by
replace h₁ : P.root l = 0 := by rwa [contra, neg_add_cancel, eq_comm] at h₁
exact P.ne_zero _ h₁
have hli : P.root l ≠ P.root i := fun contra ↦
by
replace h₁ : P.root k = 0 := by rwa [contra, add_eq_right] at h₁
exact P.ne_zero _ h₁
have hli' : P.root l ≠ -P.root i := fun contra ↦
by
replace h₁ : P.root k = 2 • P.root l := by
rwa [← neg_eq_iff_eq_neg.mpr contra, ← sub_eq_add_neg, sub_eq_iff_eq_add, ← two_nsmul] at h₁
exact P.nsmul_notMem_range_root ⟨_, h₁⟩
have hmi : P.root m ≠ P.root i := fun contra ↦
by
replace h₂ : P.root k = P.root i + P.root j := by rwa [contra, sub_eq_iff_eq_add] at h₂
replace h₃ : P.root n = 2 • P.root i := by rw [h₃, h₂]; abel
exact P.nsmul_notMem_range_root ⟨_, h₃⟩
have hmi' : P.root m ≠ -P.root i := fun contra ↦
by
replace h₂ : P.root k = -P.root i + P.root j := by rwa [contra, sub_eq_iff_eq_add] at h₂
replace h₃ : P.root n = 0 := by rw [h₃, h₂]; abel
exact P.ne_zero _ h₃
have hni : P.root n ≠ P.root i := fun contra ↦
by
replace h₃ : P.root k = P.root j := by rwa [contra, add_comm, add_sub_assoc, left_eq_add, sub_eq_zero] at h₃
replace h₂ : P.root m = 0 := by rw [← h₂, h₃, sub_self]
exact P.ne_zero _ h₂
have hni' : P.root n ≠ -P.root i := fun contra ↦
by
replace h₃ : 2 • P.root n = P.root m := by
rwa [← neg_eq_iff_eq_neg.mpr contra, add_comm, add_sub_assoc, eq_neg_add_iff_add_eq, ← two_nsmul, h₂] at h₃
exact P.nsmul_notMem_range_root ⟨_, h₃.symm⟩
replace h₁ : 2 * (x + 1) + A * y ∈ s :=
by
convert IsG2.pairingIn_mem_zero_one_three P l i hli hli'
replace h₁ : P.root l = (x + 1) • P.root i + y • P.root j := by rw [← h₁, ← h₀]; module
rw [pairingIn_eq_add_of_root_eq_smul_add_smul (S := ℤ) (j := i) h₁, pairingIn_same, Int.zsmul_eq_mul,
Int.zsmul_eq_mul]
ring
replace h₂ : 2 * x + A * (y - 1) ∈ s :=
by
convert IsG2.pairingIn_mem_zero_one_three P m i hmi hmi'
replace h₂ : P.root m = x • P.root i + (y - 1) • P.root j := by rw [← h₂, ← h₀]; module
rw [pairingIn_eq_add_of_root_eq_smul_add_smul (S := ℤ) (j := i) h₂, pairingIn_same, Int.zsmul_eq_mul,
Int.zsmul_eq_mul]
ring
replace h₃ : 2 * (x + 1) + A * (y - 1) ∈ s :=
by
convert IsG2.pairingIn_mem_zero_one_three P n i hni hni'
replace h₃ : P.root n = (x + 1) • P.root i + (y - 1) • P.root j := by rw [h₃, ← h₀]; module
rw [pairingIn_eq_add_of_root_eq_smul_add_smul (S := ℤ) (j := i) h₃, pairingIn_same, Int.zsmul_eq_mul,
Int.zsmul_eq_mul]
ring
replace h₀ : 2 * x + A * y ∈ s :=
by
convert IsG2.pairingIn_mem_zero_one_three P k i hki hki'
rw [pairingIn_eq_add_of_root_eq_smul_add_smul (j := i) h₀.symm, pairingIn_same, Int.zsmul_eq_mul, Int.zsmul_eq_mul]
ring
have hA : A ∈ s :=
IsG2.pairingIn_mem_zero_one_three P j i (P.root.injective.ne_iff.mpr hij.symm) (b.root_ne_neg_of_ne hj hi hij.symm)
subst s
simp only [mem_insert_iff, mem_singleton_iff] at h₀ h₁ h₂ h₃ hA
rcases hA with hA | hA | hA | hA | hA <;> rw [hA] at h₀ h₁ h₂ h₃ <;>
omega
/- An auxiliary result en route to `RootPairing.chainBotCoeff_mul_chainTopCoeff`. -/
