Group actions on DFinsupp

Main results

• DFinsupp.module: pointwise scalar multiplication on DFinsupp gives a module structure

instance DFinsupp.instSMulZeroClass {ι : Type u} {γ : Type w} {β : ι → Type v} [(i : ι) → Zero (β i)] [(i : ι) → SMulZeroClass γ (β i)] : SMulZeroClass γ (Π₀ (i : ι), β i)

Dependent functions with finite support inherit a semiring action from an action on each coordinate.

Equations

• DFinsupp.instSMulZeroClass = { smul := fun (c : γ) (v : Π₀ (i : ι), β i) => DFinsupp.mapRange (fun (x : ι) (x_1 : β x) => c • x_1) ⋯ v, smul_zero := ⋯ }

theorem DFinsupp.smul_apply {ι : Type u} {γ : Type w} {β : ι → Type v} [(i : ι) → Zero (β i)] [(i : ι) → SMulZeroClass γ (β i)] (b : γ) (v : Π₀ (i : ι), β i) (i : ι) : (b • v) i = b • v i

@[simp]

theorem DFinsupp.coe_smul {ι : Type u} {γ : Type w} {β : ι → Type v} [(i : ι) → Zero (β i)] [(i : ι) → SMulZeroClass γ (β i)] (b : γ) (v : Π₀ (i : ι), β i) : ⇑(b • v) = b • ⇑v

instance DFinsupp.smulCommClass {ι : Type u} {γ : Type w} {β : ι → Type v} {δ : Type u_1} [(i : ι) → Zero (β i)] [(i : ι) → SMulZeroClass γ (β i)] [(i : ι) → SMulZeroClass δ (β i)] [∀ (i : ι), SMulCommClass γ δ (β i)] : SMulCommClass γ δ (Π₀ (i : ι), β i)

instance DFinsupp.isScalarTower {ι : Type u} {γ : Type w} {β : ι → Type v} {δ : Type u_1} [(i : ι) → Zero (β i)] [(i : ι) → SMulZeroClass γ (β i)] [(i : ι) → SMulZeroClass δ (β i)] [SMul γ δ] [∀ (i : ι), IsScalarTower γ δ (β i)] : IsScalarTower γ δ (Π₀ (i : ι), β i)

instance DFinsupp.isCentralScalar {ι : Type u} {γ : Type w} {β : ι → Type v} [(i : ι) → Zero (β i)] [(i : ι) → SMulZeroClass γ (β i)] [(i : ι) → SMulZeroClass γᵐᵒᵖ (β i)] [∀ (i : ι), IsCentralScalar γ (β i)] : IsCentralScalar γ (Π₀ (i : ι), β i)

instance DFinsupp.distribMulAction {ι : Type u} {γ : Type w} {β : ι → Type v} [Monoid γ] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] : DistribMulAction γ (Π₀ (i : ι), β i)

Dependent functions with finite support inherit a DistribMulAction structure from such a structure on each coordinate.

Equations

• DFinsupp.distribMulAction = Function.Injective.distribMulAction DFinsupp.coeFnAddMonoidHom ⋯ ⋯

instance DFinsupp.module {ι : Type u} {γ : Type w} {β : ι → Type v} [Semiring γ] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Module γ (β i)] : Module γ (Π₀ (i : ι), β i)

Dependent functions with finite support inherit a module structure from such a structure on each coordinate.

Equations

• DFinsupp.module = { toDistribMulAction := inferInstanceAs (DistribMulAction γ (Π₀ (i : ι), β i)), add_smul := ⋯, zero_smul := ⋯ }

def DFinsupp.coeFnLinearMap {ι : Type u} (γ : Type w) {β : ι → Type v} [Semiring γ] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Module γ (β i)] : (Π₀ (i : ι), β i) →ₗ[γ] (i : ι) → β i

Coercion from a DFinsupp to a pi type is a LinearMap.

Equations

• DFinsupp.coeFnLinearMap γ = { toFun := DFunLike.coe, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem DFinsupp.coeFnLinearMap_apply {ι : Type u} {γ : Type w} {β : ι → Type v} [Semiring γ] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Module γ (β i)] (v : Π₀ (i : ι), β i) : (coeFnLinearMap γ) v = ⇑v

@[simp]

theorem DFinsupp.filter_smul {ι : Type u} {γ : Type w} {β : ι → Type v} [(i : ι) → Zero (β i)] [(i : ι) → SMulZeroClass γ (β i)] (p : ι → Prop) [DecidablePred p] (r : γ) (f : Π₀ (i : ι), β i) : filter p (r • f) = r • filter p f

def DFinsupp.filterLinearMap {ι : Type u} (γ : Type w) (β : ι → Type v) [Semiring γ] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Module γ (β i)] (p : ι → Prop) [DecidablePred p] : (Π₀ (i : ι), β i) →ₗ[γ] Π₀ (i : ι), β i

DFinsupp.filter as a LinearMap.

Equations

• DFinsupp.filterLinearMap γ β p = { toFun := DFinsupp.filter p, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem DFinsupp.filterLinearMap_apply {ι : Type u} (γ : Type w) (β : ι → Type v) [Semiring γ] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Module γ (β i)] (p : ι → Prop) [DecidablePred p] (x : Π₀ (i : ι), β i) : (filterLinearMap γ β p) x = filter p x

@[simp]

theorem DFinsupp.subtypeDomain_smul {ι : Type u} {γ : Type w} {β : ι → Type v} [(i : ι) → Zero (β i)] [(i : ι) → SMulZeroClass γ (β i)] {p : ι → Prop} [DecidablePred p] (r : γ) (f : Π₀ (i : ι), β i) : subtypeDomain p (r • f) = r • subtypeDomain p f

def DFinsupp.subtypeDomainLinearMap {ι : Type u} (γ : Type w) (β : ι → Type v) [Semiring γ] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Module γ (β i)] (p : ι → Prop) [DecidablePred p] : (Π₀ (i : ι), β i) →ₗ[γ] Π₀ (i : Subtype p), β ↑i

DFinsupp.subtypeDomain as a LinearMap.

Equations

• DFinsupp.subtypeDomainLinearMap γ β p = { toFun := DFinsupp.subtypeDomain p, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem DFinsupp.subtypeDomainLinearMap_apply {ι : Type u} (γ : Type w) (β : ι → Type v) [Semiring γ] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Module γ (β i)] (p : ι → Prop) [DecidablePred p] (x : Π₀ (i : ι), β i) : (subtypeDomainLinearMap γ β p) x = subtypeDomain p x

@[simp]

theorem DFinsupp.mk_smul {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → SMulZeroClass γ (β i)] {s : Finset ι} (c : γ) (x : (i : ↑↑s) → β ↑i) : mk s (c • x) = c • mk s x

@[simp]

theorem DFinsupp.single_smul {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → SMulZeroClass γ (β i)] {i : ι} (c : γ) (x : β i) : single i (c • x) = c • single i x

theorem DFinsupp.support_smul {ι : Type u} {β : ι → Type v} [DecidableEq ι] {γ : Type w} [(i : ι) → Zero (β i)] [(i : ι) → SMulZeroClass γ (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (b : γ) (v : Π₀ (i : ι), β i) : (b • v).support ⊆ v.support

@[simp]

theorem DFinsupp.comapDomain_smul {ι : Type u} {γ : Type w} {β : ι → Type v} {κ : Type u_1} [(i : ι) → Zero (β i)] [(i : ι) → SMulZeroClass γ (β i)] (h : κ → ι) (hh : Function.Injective h) (r : γ) (f : Π₀ (i : ι), β i) : comapDomain h hh (r • f) = r • comapDomain h hh f

@[simp]

theorem DFinsupp.comapDomain'_smul {ι : Type u} {γ : Type w} {β : ι → Type v} {κ : Type u_1} [(i : ι) → Zero (β i)] [(i : ι) → SMulZeroClass γ (β i)] (h : κ → ι) {h' : ι → κ} (hh' : Function.LeftInverse h' h) (r : γ) (f : Π₀ (i : ι), β i) : comapDomain' h hh' (r • f) = r • comapDomain' h hh' f

instance DFinsupp.distribMulAction₂ {ι : Type u} {γ : Type w} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [Monoid γ] [(i : ι) → (j : α i) → AddMonoid (δ i j)] [(i : ι) → (j : α i) → DistribMulAction γ (δ i j)] : DistribMulAction γ (Π₀ (i : ι) (j : α i), δ i j)

Equations

• DFinsupp.distribMulAction₂ = DFinsupp.distribMulAction

theorem DFinsupp.equivProdDFinsupp_smul {ι : Type u} {γ : Type w} {α : Option ι → Type v} [(i : Option ι) → Zero (α i)] [(i : Option ι) → SMulZeroClass γ (α i)] (r : γ) (f : Π₀ (i : Option ι), α i) : equivProdDFinsupp (r • f) = r • equivProdDFinsupp f