Properties of the module α →₀ M

• Finsupp.linearEquivFunOnFinite: α →₀ β and a → β are equivalent if α is finite

Tags

function with finite support, module, linear algebra

noncomputable def Finsupp.LinearEquiv.finsuppUnique (R : Type u_1) (M : Type u_3) [AddCommMonoid M] [Semiring R] [Module R M] (α : Type u_4) [Unique α] : (α →₀ M) ≃ₗ[R] M

If α has a unique term, then the type of finitely supported functions α →₀ M is R-linearly equivalent to M.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Finsupp.LinearEquiv.finsuppUnique_apply {R : Type u_1} {M : Type u_3} [AddCommMonoid M] [Semiring R] [Module R M] (α : Type u_4) [Unique α] (f : α →₀ M) : (finsuppUnique R M α) f = f default

@[simp]

theorem Finsupp.LinearEquiv.finsuppUnique_symm_apply {R : Type u_1} {M : Type u_3} [AddCommMonoid M] [Semiring R] [Module R M] {α : Type u_4} [Unique α] (m : M) : (finsuppUnique R M α).symm m = single default m

def Finsupp.lcoeFun {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] : (α →₀ M) →ₗ[R] α → M

Forget that a function is finitely supported.

This is the linear version of Finsupp.toFun.

Equations

• Finsupp.lcoeFun = { toFun := DFunLike.coe, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Finsupp.lcoeFun_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (a✝ : α →₀ M) (a : α) : lcoeFun a✝ a = a✝ a

def LinearMap.splittingOfFunOnFintypeSurjective {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} [Finite α] (f : M →ₗ[R] α → R) (s : Function.Surjective ⇑f) : (α → R) →ₗ[R] M

A surjective linear map to functions on a finite type has a splitting.

Equations

• f.splittingOfFunOnFintypeSurjective s = ((Finsupp.lift M R α) fun (x : α) => ⋯.choose) ∘ₗ ↑(Finsupp.linearEquivFunOnFinite R R α).symm

theorem LinearMap.splittingOfFunOnFintypeSurjective_splits {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} [Finite α] (f : M →ₗ[R] α → R) (s : Function.Surjective ⇑f) : f ∘ₗ f.splittingOfFunOnFintypeSurjective s = id

theorem LinearMap.leftInverse_splittingOfFunOnFintypeSurjective {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} [Finite α] (f : M →ₗ[R] α → R) (s : Function.Surjective ⇑f) : Function.LeftInverse ⇑f ⇑(f.splittingOfFunOnFintypeSurjective s)

theorem LinearMap.splittingOfFunOnFintypeSurjective_injective {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} [Finite α] (f : M →ₗ[R] α → R) (s : Function.Surjective ⇑f) : Function.Injective ⇑(f.splittingOfFunOnFintypeSurjective s)

def Finsupp.submodule {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} (S : α → Submodule R M) : Submodule R (α →₀ M)

Given a family Sᵢ of R-submodules of M indexed by a type α, this is the R-submodule of α →₀ M of functions f such that f i ∈ Sᵢ for all i : α.

Equations

• Finsupp.submodule S = { carrier := {x : α →₀ M | ∀ (i : α), x i ∈ S i}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem Finsupp.mem_submodule_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} (S : α → Submodule R M) (x : α →₀ M) : x ∈ submodule S ↔ ∀ (i : α), x i ∈ S i

theorem Finsupp.ker_mapRange {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (I : Type u_5) : LinearMap.ker (mapRange.linearMap f) = submodule fun (x : I) => LinearMap.ker f

theorem Finsupp.range_mapRange_linearMap {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (hf : LinearMap.ker f = ⊥) (I : Type u_5) : LinearMap.range (mapRange.linearMap f) = submodule fun (x : I) => LinearMap.range f