Stiemke's lemma

Stiemke's lemma is the theorem of the alternative for a linear subspace and the nonnegative orthant: a subspace V of ι → ℝ meets the closed nonnegative orthant only in 0 exactly when some strictly positive vector w is orthogonal to V. We also prove the corresponding statement for a subgroup P of the lattice ι → ℤ: P contains no nonzero nonnegative element exactly when P is orthogonal to a strictly positive real vector. This relies on a rationality statement that is not formal: if the only nonnegative element of P is 0, then the same holds for the real span of P, even though a real point of that span need not be a real multiple of a lattice point.

The lattice form is what is used for Heegaard diagrams: it turns weak admissibility, a condition on the integral periodic domains, into the existence of an area form for which every periodic domain has signed area zero.

Main results

• TauCeti.exists_pos_forall_sum_mul_eq_zero_iff: Stiemke's lemma for a real subspace.
• TauCeti.exists_mem_ne_zero_support_subset_of_mem_span_intCast: a nonzero vector in the real span of a subgroup of ι → ℤ has the support of a nonzero element of the subgroup inside its support.
• TauCeti.eq_zero_of_mem_span_intCast_of_nonneg: a subgroup of ι → ℤ whose only nonnegative element is 0 spans a real subspace whose only nonnegative element is 0.
• TauCeti.exists_pos_forall_sum_mul_intCast_eq_zero_iff: Stiemke's lemma for a subgroup of ι → ℤ.

References

• E. Stiemke, Über positive Lösungen homogener linearer Gleichungen, Math. Ann. 76 (1915), 340–342.

theorem TauCeti.exists_pos_forall_sum_mul_eq_zero_iff {ι : Type u_1} [Fintype ι] {V : Submodule ℝ (ι → ℝ)} : (∃ (w : ι → ℝ), (∀ (i : ι), 0 < w i) ∧ ∀ v ∈ V, ∑ i : ι, w i * v i = 0) ↔ ∀ v ∈ V, 0 ≤ v → v = 0

Stiemke's lemma. A real subspace V of ι → ℝ meets the closed nonnegative orthant only in 0 exactly when some strictly positive vector is orthogonal to every element of V.

theorem TauCeti.exists_mem_ne_zero_support_subset_of_mem_span_intCast {ι : Type u_1} [Finite ι] {P : AddSubgroup (ι → ℤ)} {v : ι → ℝ} (hv : v ∈ Submodule.span ℝ ((fun (p : ι → ℤ) (i : ι) => ↑(p i)) '' ↑P)) (hv₀ : v ≠ 0) : ∃ q ∈ P, q ≠ 0 ∧ Function.support q ⊆ Function.support v

A nonzero vector in the real span of a subgroup P of ι → ℤ has the support of a nonzero element of P inside its own support.

theorem TauCeti.eq_zero_of_mem_span_intCast_of_nonneg {ι : Type u_1} [Finite ι] {P : AddSubgroup (ι → ℤ)} (hP : ∀ p ∈ P, 0 ≤ p → p = 0) {v : ι → ℝ} (hv : v ∈ Submodule.span ℝ ((fun (p : ι → ℤ) (i : ι) => ↑(p i)) '' ↑P)) (hv₀ : 0 ≤ v) : v = 0

A subgroup P of ι → ℤ whose only nonnegative element is 0 spans a real subspace of ι → ℝ whose only nonnegative element is 0.

theorem TauCeti.exists_pos_forall_sum_mul_intCast_eq_zero_iff {ι : Type u_1} [Fintype ι] {P : AddSubgroup (ι → ℤ)} : (∃ (w : ι → ℝ), (∀ (i : ι), 0 < w i) ∧ ∀ p ∈ P, ∑ i : ι, w i * ↑(p i) = 0) ↔ ∀ p ∈ P, 0 ≤ p → p = 0

Stiemke's lemma for a lattice. A subgroup P of ι → ℤ has 0 as its only nonnegative element exactly when some strictly positive real vector is orthogonal to every element of P.