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 : α) : LinearMap.ker (Finsupp.lsingle a) = ⊥

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, LinearMap.range (Finsupp.lsingle a) ≤ ⨅ a ∈ t, LinearMap.ker (Finsupp.lapply a)

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 : α), LinearMap.ker (Finsupp.lapply a) ≤ ⊥

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

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, LinearMap.range (Finsupp.lsingle a)) (⨆ a ∈ t, LinearMap.range (Finsupp.lsingle a))

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 (Finsupp.single a '' s) = Submodule.map (Finsupp.lsingle a) (Submodule.span R s)

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