# Properties of the module `α →₀ M` #

- `Finsupp.linearEquivFunOnFinite`: `α →₀ β` and `a → β` are equivalent if `α` is finite
- `FunOnFinite.map`: the map `(X → M) → (Y → M)` induced by a map `f : X ⟶ Y` when `X` and `Y` are finite.
- `FunOnFinite.linearMmap`: the linear map `(X → M) →ₗ[R] (Y → M)` induced by a map `f : X ⟶ Y` when `X` and `Y` are finite.

## Tags #

function with finite support, module, linear algebra

source
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.

Instances For

source
@[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
source
@[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
source
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' := ⋯ }

Instances For

source
@[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
source
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

Instances For

source
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
source
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)
source
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)
source
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' := ⋯ }

Instances For

source
@[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
source
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
source
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
source
noncomputable def FunOnFinite.map {M : Type u_4} [AddCommMonoid M] {X : Type u_5} {Y : Type u_6} [Finite X] [Finite Y] (f : X → Y) (s : X → M) :
Y → M

The map `(X → M) → (Y → M)` induced by a map `X → Y` between finite types.

Equations

- FunOnFinite.map f s = Finsupp.equivFunOnFinite (Finsupp.mapDomain f (Finsupp.equivFunOnFinite.symm s))

Instances For

source
theorem FunOnFinite.map_apply_apply {M : Type u_4} [AddCommMonoid M] {X : Type u_5} {Y : Type u_6} [Fintype X] [Finite Y] [DecidableEq Y] (f : X → Y) (s : X → M) (y : Y) :
map f s y = ∑ x : X with f x = y, s x
source
@[simp]
theorem FunOnFinite.map_piSingle {M : Type u_4} [AddCommMonoid M] {X : Type u_5} {Y : Type u_6} [Finite X] [Finite Y] [DecidableEq X] [DecidableEq Y] (f : X → Y) (x : X) (m : M) :
map f (Pi.single x m) = Pi.single (f x) m
source
theorem FunOnFinite.map_id (M : Type u_4) [AddCommMonoid M] {X : Type u_5} [Finite X] :
map id = id
source
theorem FunOnFinite.map_comp {M : Type u_4} [AddCommMonoid M] {X : Type u_5} {Y : Type u_6} {Z : Type u_7} [Finite X] [Finite Y] [Finite Z] (g : Y → Z) (f : X → Y) :
map (g ∘ f) = map g ∘ map f
source
noncomputable def FunOnFinite.linearMap (R : Type u_4) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {X : Type u_6} {Y : Type u_7} [Finite X] [Finite Y] (f : X → Y) :
(X → M) →ₗ[R] Y → M

The linear map `(X → M) →ₗ[R] (Y → M)` induced by a map `X → Y` between finite types.

Equations

- FunOnFinite.linearMap R M f = (↑(Finsupp.linearEquivFunOnFinite R M Y) ∘ₗ Finsupp.lmapDomain M R f) ∘ₗ ↑(Finsupp.linearEquivFunOnFinite R M X).symm

Instances For

source
theorem FunOnFinite.linearMap_apply_apply (R : Type u_4) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {X : Type u_6} {Y : Type u_7} [Fintype X] [Finite Y] [DecidableEq Y] (f : X → Y) (s : X → M) (y : Y) :
(linearMap R M f) s y = {x : X | f x = y}.sum s
source
@[simp]
theorem FunOnFinite.linearMap_piSingle (R : Type u_4) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {X : Type u_6} {Y : Type u_7} [Finite X] [Finite Y] [DecidableEq X] [DecidableEq Y] (f : X → Y) (x : X) (m : M) :
(linearMap R M f) (Pi.single x m) = Pi.single (f x) m
source
@[simp]
theorem FunOnFinite.linearMap_id (R : Type u_4) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (X : Type u_6) [Finite X] :
linearMap R M id = LinearMap.id
source
theorem FunOnFinite.linearMap_comp (R : Type u_4) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {X : Type u_6} {Y : Type u_7} {Z : Type u_8} [Finite X] [Finite Y] [Finite Z] (f : X → Y) (g : Y → Z) :
linearMap R M (g ∘ f) = linearMap R M g ∘ₗ linearMap R M f