English
A linear independent family i is maximal iff for every κ and every w : κ → M with i' linear independent and a map j: ι → κ such that w ∘ j = v, j is surjective.
Русский
Линейно независимое семейство i максимальное тогда и только тогда, когда для любого κ и любой w : κ → M, линейно независимого i' и отображения j: ι → κ такие, что w ∘ j = v, отображение j сюрьективно.
LaTeX
$$$i.Maximal \iff \forall \kappa (w: \kappa \to M) (_i' : LinearIndependent R w) (j: ι \to \kappa) (_h : w \circ j = v), Surjective j$$$
Lean4
/-- An alternative characterization of a maximal linearly independent family,
quantifying over types (in the same universe as `M`) into which the indexing family injects.
-/
theorem maximal_iff {ι : Type w} {R : Type u} [Semiring R] [Nontrivial R] {M : Type v} [AddCommMonoid M] [Module R M]
{v : ι → M} (i : LinearIndependent R v) :
i.Maximal ↔ ∀ (κ : Type v) (w : κ → M) (_i' : LinearIndependent R w) (j : ι → κ) (_h : w ∘ j = v), Surjective j :=
by
constructor
· rintro p κ w i' j rfl
specialize p (range w) i'.linearIndepOn_id (range_comp_subset_range _ _)
rw [range_comp, ← image_univ (f := w)] at p
exact range_eq_univ.mp (image_injective.mpr i'.injective p)
· intro p w i' h
specialize
p w ((↑) : w → M) i' (fun i => ⟨v i, range_subset_iff.mp h i⟩)
(by
ext
simp)
have q := congr_arg (fun s => ((↑) : w → M) '' s) p.range_eq
dsimp at q
rw [← image_univ, image_image] at q
simpa using q
