English
If a Finset t has cardinality at least finrank+1, there exists a nontrivial relation with coefficients summing to zero.
Русский
Если множество t имеет размер не менее finrank+1, тождество: существует ненулевая линейная связь, сумма коэффициентов равна нулю.
LaTeX
$$$t \;\text{finset},\; \operatorname{finrank} R M + 1 < |t| \Rightarrow \exists f:\ M \to R,\; \sum_{e \in t} f(e) e = 0 \\ \land \ \sum_{e \in t} f(e) = 0 \land \exists x \in t, f(x) \neq 0$$$
Lean4
/-- If a finset has cardinality larger than `finrank + 1`,
then there is a nontrivial linear relation amongst its elements,
such that the coefficients of the relation sum to zero. -/
theorem exists_nontrivial_relation_sum_zero_of_finrank_succ_lt_card {t : Finset M} (h : finrank R M + 1 < t.card) :
∃ f : M → R, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0 := by
-- Pick an element x₀ ∈ t,
obtain ⟨x₀, x₀_mem⟩ :=
card_pos.1
((Nat.succ_pos _).trans h)
-- and apply the previous lemma to the {xᵢ - x₀}
let shift : M ↪ M := ⟨(· - x₀), sub_left_injective⟩
classical
let t' := (t.erase x₀).map shift
have h' : finrank R M < t'.card := by
rw [card_map, card_erase_of_mem x₀_mem]
exact Nat.lt_pred_iff.mpr h
obtain ⟨g, gsum, x₁, x₁_mem, nz⟩ := exists_nontrivial_relation_of_finrank_lt_card h'
let f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
refine
⟨f, ?_, ?_, ?_⟩
-- After this, it's a matter of verifying the properties,
-- based on the corresponding properties for `g`.
· rw [sum_map, Embedding.coeFn_mk] at gsum
simp_rw [f, ← t.sum_erase_add _ x₀_mem, if_pos, neg_smul, sum_smul, ← sub_eq_add_neg, ← sum_sub_distrib, ← gsum,
smul_sub]
refine sum_congr rfl fun x x_mem ↦ ?_
rw [if_neg (mem_erase.mp x_mem).1]
· simp_rw [f, ← t.sum_erase_add _ x₀_mem, if_pos, add_neg_eq_zero]
exact sum_congr rfl fun x x_mem ↦ if_neg (mem_erase.mp x_mem).1
· obtain ⟨x₁, x₁_mem', rfl⟩ := Finset.mem_map.mp x₁_mem
have := mem_erase.mp x₁_mem'
exact ⟨x₁, by simpa only [f, Embedding.coeFn_mk, sub_add_cancel, this.2, true_and, if_neg this.1]⟩
