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)