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_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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_3} [Semiring R] {β : Type u_5} (u : α → β) : (lmapDomain R R u).range = Submodule.span R (Set.range fun (x : α) => single (u x) 1)

theorem Finsupp.span_single_eq_top {α : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : Submodule.span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x} = ⊤

theorem Submodule.exists_finset_of_mem_iSup {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} (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_3} {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

theorem Submodule.range_lsum_smul {R : Type u_1} {M : Type u_2} {N : Type u_3} {σ : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (φ : M →ₗ[R] N) (f : σ → R) : ((Finsupp.lsum R) fun (x : σ) => f x • φ).range = Set.range f • φ.range

theorem Submodule.image_smul_top_eq_range_lsum {R : Type u_1} {M : Type u_2} {σ : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set σ) (f : σ → R) : f '' s • ⊤ = ((Finsupp.lsum R) fun (i : ↑s) => f ↑i • LinearMap.id).range

theorem Submodule.smul_top_eq_range_lsum {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) : s • ⊤ = ((Finsupp.lsum R) fun (i : ↑s) => ↑i • LinearMap.id).range