def Function.supported {α : Type u_1} (M : Type u_4) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) : Submodule R (α → M)

The R-submodule of all functions from α to M with support contained in s : Set α.

Equations

• Function.supported M R s = { carrier := {f : α → M | ∀ i ∉ s, f i = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem Function.coe_supported {α : Type u_1} (M : Type u_4) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) : ↑(supported M R s) = {f : α → M | ∀ i ∉ s, f i = 0}

@[simp]

theorem Function.mem_supported_iff {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set α} {x : α → M} : x ∈ supported M R s ↔ ∀ i ∉ s, x i = 0

theorem Function.mem_supported {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set α} {x : α → M} : x ∈ supported M R s ↔ support x ⊆ s

noncomputable def Function.supportedEquivFun {α : Type u_1} (M : Type u_4) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) : ↥(supported M R s) ≃ₗ[R] ↑s → M

Function.supported M R s is linearly equivalent to the type ↥s → M.

Equations

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

@[simp]

theorem Function.supportedEquivFun_apply {α : Type u_1} (M : Type u_4) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (i : ↑s) (x : ↥(supported M R s)) : (supportedEquivFun M R s) x i = ↑x ↑i

theorem Function.supportedEquivFun_symm_apply_mem {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set α} {i : α} (hi : i ∈ s) (x : ↑s → M) : ↑((supportedEquivFun M R s).symm x) i = x ⟨i, hi⟩

theorem Function.supportedEquivFun_symm_apply_notMem {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set α} {i : α} (hi : i ∉ s) (x : ↑s → M) : ↑((supportedEquivFun M R s).symm x) i = 0

noncomputable def Finsupp.supportedCoeFunSupported {α : Type u_1} (M : Type u_4) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) : ↥(supported M R s) →ₗ[R] ↥(Function.supported M R s)

Forget that a function in Finsupp.supported M R s has finite support.

Equations

• Finsupp.supportedCoeFunSupported M R s = { toFun := fun (x : ↥(Finsupp.supported M R s)) => ⟨Finsupp.lcoeFun ↑x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Finsupp.supportedCoeFunSupported_apply_coe {α : Type u_1} (M : Type u_4) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (x : ↥(supported M R s)) (a✝ : α) : ↑((supportedCoeFunSupported M R s) x) a✝ = lcoeFun (↑x) a✝

theorem Finsupp.supportedCoeFunSupported_injective {α : Type u_1} (M : Type u_4) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) : Function.Injective ⇑(supportedCoeFunSupported M R s)

noncomputable def Finsupp.supportedEquivFunSupported {α : Type u_1} {s : Set α} (M : Type u_4) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (hs : s.Finite) : ↥(supported M R s) ≃ₗ[R] ↥(Function.supported M R s)

If s is finite, then Finsupp.supported M R s and Function.supported M R s are the same.

Equations

• Finsupp.supportedEquivFunSupported M R hs = Finsupp.supportedEquivFinsupp s ≪≫ₗ Finsupp.linearEquivFunOnFinite R M ↑s ≪≫ₗ (Function.supportedEquivFun M R s).symm

@[simp]

theorem Finsupp.supportedEquivFunSupported_apply {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set α} {hs : s.Finite} (x : ↥(supported M R s)) (i : α) : ↑((supportedEquivFunSupported M R hs) x) i = ↑x i

@[simp]

theorem Finsupp.supportedEquivFunSupported_apply_symm {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set α} {hs : s.Finite} (x : ↥(Function.supported M R s)) (i : α) : ↑((supportedEquivFunSupported M R hs).symm x) i = ↑x i

def Finsupp.lExtendDomain {α : Type u_1} {M : Type u_4} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (P : α → Prop) [DecidablePred P] : (Subtype P →₀ M) →ₗ[R] α →₀ M

Equations

• Finsupp.lExtendDomain R P = { toFun := fun (x : Subtype P →₀ M) => x.extendDomain, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Finsupp.lExtendDomain_apply {α : Type u_1} {M : Type u_4} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (P : α → Prop) [DecidablePred P] (x : Subtype P →₀ M) : (lExtendDomain R P) x = x.extendDomain

noncomputable def Finsupp.lEmbDomain {α : Type u_4} {β : Type u_5} {M : Type u_6} (R : Type u_7) [Semiring R] [AddCommMonoid M] [Module R M] (f : α ↪ β) : (α →₀ M) →ₗ[R] β →₀ M

Equations

• Finsupp.lEmbDomain R f = { toFun := Finsupp.embDomain f, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Finsupp.lEmbDomain_apply {α : Type u_4} {β : Type u_5} {M : Type u_6} (R : Type u_7) [Semiring R] [AddCommMonoid M] [Module R M] (f : α ↪ β) (v : α →₀ M) : (lEmbDomain R f) v = embDomain f v

@[simp]

theorem Finsupp.toENat_rank_supported {α : Type u_1} (R : Type u_4) [Semiring R] [StrongRankCondition R] (s : Set α) : Cardinal.toENat (Module.rank R ↥(supported R R s)) = s.encard

@[simp]

theorem Finsupp.finrank_supported {α : Type u_1} (R : Type u_4) [Semiring R] [StrongRankCondition R] (s : Set α) : Module.finrank R ↥(supported R R s) = s.ncard

@[simp]

theorem Function.toENat_rank_supported {α : Type u_1} (R : Type u_4) [Semiring R] [StrongRankCondition R] (s : Set α) : Cardinal.toENat (Module.rank R ↥(supported R R s)) = s.encard

@[simp]

theorem Function.finrank_supported {α : Type u_1} (R : Type u_4) [Semiring R] [StrongRankCondition R] (s : Set α) : Module.finrank R ↥(supported R R s) = s.ncard

noncomputable def Function.dualEvalSingle (α : Type u_4) (R : Type u_5) [DecidableEq α] [CommSemiring R] : Module.Dual R (α → R) →ₗ[R] α → R

Equations

• Function.dualEvalSingle α R = { toFun := fun (φ : Module.Dual R (α → R)) (a : α) => φ (Pi.single a 1), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Function.dualEvalSingle_apply (α : Type u_4) (R : Type u_5) [DecidableEq α] [CommSemiring R] (φ : Module.Dual R (α → R)) (a : α) : (dualEvalSingle α R) φ a = φ (Pi.single a 1)

noncomputable def Finsupp.dualEvalSingle (α : Type u_4) (R : Type u_5) [CommSemiring R] : Module.Dual R (α →₀ R) →ₗ[R] α → R

Equations

• Finsupp.dualEvalSingle α R = { toFun := fun (φ : Module.Dual R (α →₀ R)) (a : α) => φ (Finsupp.single a 1), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Finsupp.dualEvalSingle_apply (α : Type u_4) (R : Type u_5) [CommSemiring R] (φ : Module.Dual R (α →₀ R)) (a : α) : (dualEvalSingle α R) φ a = φ (single a 1)

noncomputable def Function.supportedDualEvalSingle {α : Type u_4} [DecidableEq α] (R : Type u_5) [CommSemiring R] (s : Set α) : Module.Dual R ↥(supported R R s) →ₗ[R] ↥(supported R R s)

Equations

• Function.supportedDualEvalSingle R s = ↑(Function.supportedEquivFun R R s).symm ∘ₗ Function.dualEvalSingle (↑s) R ∘ₗ ↑(Function.supportedEquivFun R R s).symm.dualMap