Properties of the module α →₀ M
#
Finsupp.linearEquivFunOnFinite
:α →₀ β
anda → β
are equivalent ifα
is finiteFunOnFinite.map
: the map(X → M) → (Y → M)
induced by a mapf : X ⟶ Y
whenX
andY
are finite.FunOnFinite.linearMmap
: the linear map(X → M) →ₗ[R] (Y → M)
induced by a mapf : X ⟶ Y
whenX
andY
are 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 α]
:
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
@[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)
:
@[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)
:
def
Finsupp.lcoeFun
{α : Type u_1}
{M : Type u_2}
{R : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module 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
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)
:
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
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)
:
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)
:
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)
:
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)
:
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
Instances For
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)
:
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)
:
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
Instances For
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)
:
@[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)
:
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)
:
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
@[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)
:
@[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]
: