English
Another form: Independent f is equivalent to iSupIndep (Projectivization.submodule ∘ f).
Русский
Еще одна форма: Независимость f эквивалентна iSupIndep (Projectivization.submodule ∘ f).
LaTeX
$$$Independent(f) \\iff iSupIndep (fun i => (f(i)).submodule)$$$
Lean4
/-- A family of points in projective space is independent if and only if the family of
submodules which the points determine is independent in the lattice-theoretic sense. -/
theorem independent_iff_iSupIndep : Independent f ↔ iSupIndep fun i => (f i).submodule :=
by
refine ⟨?_, fun h => ?_⟩
· rintro ⟨f, hf, hi⟩
simp only [submodule_mk]
exact (iSupIndep_iff_linearIndependent_of_ne_zero (R := K) hf).mpr hi
· rw [independent_iff]
refine h.linearIndependent (Projectivization.submodule ∘ f) (fun i => ?_) fun i => ?_
· simpa only [Function.comp_apply, submodule_eq] using Submodule.mem_span_singleton_self _
· exact rep_nonzero (f i)
