Finitely supported functions and spans

Tags

function with finite support, module, linear algebra

@[simp]

theorem Finsupp.ker_lsingle {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (a : α) : (lsingle a).ker = ⊥

theorem Finsupp.lsingle_range_le_ker_lapply {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s t : Set α) (h : Disjoint s t) : ⨆ a ∈ s, (lsingle a).range ≤ ⨅ a ∈ t, (lapply a).ker

theorem Finsupp.iInf_ker_lapply_le_bot {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] : ⨅ (a : α), (lapply a).ker ≤ ⊥

theorem Finsupp.iSup_lsingle_range {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] : ⨆ (a : α), (lsingle a).range = ⊤

theorem Finsupp.disjoint_lsingle_lsingle {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s t : Set α) (hs : Disjoint s t) : Disjoint (⨆ a ∈ s, (lsingle a).range) (⨆ a ∈ t, (lsingle a).range)

theorem Finsupp.span_single_image {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) (a : α) : Submodule.span R (single a '' s) = Submodule.map (lsingle a) (Submodule.span R s)

theorem Finsupp.range_lmapDomain {α : Type u_1} {R : Type u_5} [Semiring R] {β : Type u_7} (u : α → β) : (lmapDomain R R u).range = Submodule.span R (Set.range fun (x : α) => single (u x) 1)

theorem Submodule.exists_finset_of_mem_iSup {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} (p : ι → Submodule R M) {m : M} (hm : m ∈ ⨆ (i : ι), p i) : ∃ (s : Finset ι), m ∈ ⨆ i ∈ s, p i

theorem Submodule.mem_iSup_iff_exists_finset {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} {p : ι → Submodule R M} {m : M} : m ∈ ⨆ (i : ι), p i ↔ ∃ (s : Finset ι), m ∈ ⨆ i ∈ s, p i

Submodule.exists_finset_of_mem_iSup as an iff

theorem Submodule.mem_sSup_iff_exists_finset {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {S : Set (Submodule R M)} {m : M} : m ∈ sSup S ↔ ∃ (s : Finset (Submodule R M)), ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i