English
If i is positive, there exists j in the base support with nonzero pairingIn.
Русский
Если i положительно, существует j в опоре базы с ненулевым pairingIn.
LaTeX
$$b.IsPos i → ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0$$
Lean4
theorem exists_mem_support_pos_pairingIn [P.IsCrystallographic] {i : ι} (h₀ : b.IsPos i) :
∃ j ∈ b.support, 0 < P.pairingIn ℤ j i := by
by_contra! contra
suffices P.pairingIn ℤ i i ≤ 0 by simp_all
obtain ⟨f, hf₀, hf₁, hf₂⟩ := b.exists_root_eq_sum_int i
replace hf₁ : 0 < f := by
refine hf₁.resolve_right ?_
rw [isPos_iff, height_eq_sum hf₂] at h₀
contrapose! h₀
exact Finset.sum_nonpos fun i _ ↦ h₀.le i
have : P.pairingIn ℤ i i = ∑ j ∈ b.support, f j • P.pairingIn ℤ j i :=
algebraMap_injective ℤ R <| by
simp_rw [algebraMap_pairingIn, map_sum, ← root_coroot_eq_pairing, hf₂, map_sum, map_zsmul, LinearMap.coeFn_sum,
Finset.sum_apply, LinearMap.smul_apply, root_coroot_eq_pairing, zsmul_eq_mul, algebraMap_pairingIn]
rw [this]
refine Finset.sum_nonpos fun j _ ↦ ?_
by_cases hj : j ∈ Function.support f
· exact smul_nonpos_of_nonneg_of_nonpos (hf₁.le j) (contra j (hf₀ hj))
· simp_all
