Unions of `Submodule`s #

This file is a home for results about unions of submodules.

Main results: #

Submodule.iUnion_ssubset_of_forall_ne_top_of_card_lt: a finite union of proper submodules is a proper subset, provided the coefficients are a sufficiently large field.

theorem Submodule.iUnion_ssubset_of_forall_ne_top_of_card_lt {ι : Type u_1} {K : Type u_2} {M : Type u_3} [Field K] [AddCommGroup M] [Module K M] (s : Finset ι) (p : ι → Submodule K M) (h₁ : ∀ (i : ι), p i ≠ ⊤) (h₂ : ↑s.card < ENat.card K) :

⋃ i ∈ s, ↑(p i) ⊂ Set.univ

theorem Submodule.exists_forall_notMem_of_forall_ne_top {ι : Type u_1} {K : Type u_2} {M : Type u_3} [Field K] [AddCommGroup M] [Module K M] [Finite ι] [Infinite K] (p : ι → Submodule K M) (h : ∀ (i : ι), p i ≠ ⊤) :

∃ (x : M), ∀ (i : ι), x ∉ p i

theorem Module.Dual.exists_forall_ne_zero_of_forall_exists {ι : Type u_1} {K : Type u_2} {M : Type u_3} [Field K] [AddCommGroup M] [Module K M] [Finite ι] [Infinite K] (f : ι → Dual K M) (h : ∀ (i : ι), ∃ (x : M), (f i) x ≠ 0) :

∃ (x : M), ∀ (i : ι), (f i) x ≠ 0

theorem Module.Dual.exists_forall_mem_ne_zero_of_forall_exists {ι : Type u_1} {K : Type u_2} {M : Type u_3} [Field K] [AddCommGroup M] [Module K M] [Finite ι] [Infinite K] (p : Submodule K M) (f : ι → Dual K M) (h : ∀ (i : ι), ∃ x ∈ p, (f i) x ≠ 0) :

∃ x ∈ p, ∀ (i : ι), (f i) x ≠ 0

A convenience variation of Module.Dual.exists_forall_ne_zero_of_forall_exists where we are concerned only about behaviour on a fixed submodule.

theorem Module.exists_dual_forall_apply_ne_zero {ι : Type u_1} {K : Type u_2} {M : Type u_3} [Field K] [AddCommGroup M] [Module K M] [Finite ι] [Infinite K] (v : ι → M) (hv : ∀ (i : ι), v i ≠ 0) :

∃ (f : Dual K M), ∀ (i : ι), f (v i) ≠ 0