Group actions on DFinsupp

Main results

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

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

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

Equations

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

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

@[simp]

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

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

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

instance DFinsupp.isCentralScalar {ι : Type u} {γ : Type w} {β : ι → Type v} [Monoid γ] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] [(i : ι) → DistribMulAction γᵐᵒᵖ (β 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 = Module.mk ⋯ ⋯

@[simp]

theorem DFinsupp.filter_smul {ι : Type u} {γ : Type w} {β : ι → Type v} [Monoid γ] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] (p : ι → Prop) [DecidablePred p] (r : γ) (f : Π₀ (i : ι), β i) : DFinsupp.filter p (r • f) = r • DFinsupp.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) : (DFinsupp.filterLinearMap γ β p) x = DFinsupp.filter p x

@[simp]

theorem DFinsupp.subtypeDomain_smul {ι : Type u} {γ : Type w} {β : ι → Type v} [Monoid γ] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] {p : ι → Prop} [DecidablePred p] (r : γ) (f : Π₀ (i : ι), β i) : DFinsupp.subtypeDomain p (r • f) = r • DFinsupp.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) : (DFinsupp.subtypeDomainLinearMap γ β p) x = DFinsupp.subtypeDomain p x

@[simp]

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

@[simp]

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

theorem DFinsupp.support_smul {ι : Type u} {β : ι → Type v} [DecidableEq ι] {γ : Type w} [Semiring γ] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Module γ (β 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} [Monoid γ] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] (h : κ → ι) (hh : Function.Injective h) (r : γ) (f : Π₀ (i : ι), β i) : DFinsupp.comapDomain h hh (r • f) = r • DFinsupp.comapDomain h hh f

@[simp]

theorem DFinsupp.comapDomain'_smul {ι : Type u} {γ : Type w} {β : ι → Type v} {κ : Type u_1} [Monoid γ] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] (h : κ → ι) {h' : ι → κ} (hh' : Function.LeftInverse h' h) (r : γ) (f : Π₀ (i : ι), β i) : DFinsupp.comapDomain' h hh' (r • f) = r • DFinsupp.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} [Monoid γ] [(i : Option ι) → AddMonoid (α i)] [(i : Option ι) → DistribMulAction γ (α i)] (r : γ) (f : Π₀ (i : Option ι), α i) : DFinsupp.equivProdDFinsupp (r • f) = r • DFinsupp.equivProdDFinsupp f