Mathlib.Algebra.Group.Action.Pi

Pi.smul' instance

[∀ i, SMul (α i) (β i)] : SMul (∀ i, α i) (∀ i, β i)

Full source

@[to_additive]
instance smul' [∀ i, SMul (α i) (β i)] : SMul (∀ i, α i) (∀ i, β i) where smul s x i := s i • x i

Componentwise Scalar Multiplication on Product Types

Informal description

For any family of types $(\alpha_i)$ and $(\beta_i)$ where each $\alpha_i$ has a scalar multiplication operation on $\beta_i$, the product type $\prod_i \alpha_i$ has a scalar multiplication operation on $\prod_i \beta_i$ defined componentwise.

Pi.smul_def' theorem

[∀ i, SMul (α i) (β i)] (s : ∀ i, α i) (x : ∀ i, β i) : s • x = fun i ↦ s i • x i

Full source

@[to_additive]
lemma smul_def' [∀ i, SMul (α i) (β i)] (s : ∀ i, α i) (x : ∀ i, β i) : s • x = fun i ↦ s i • x i :=
  rfl

Componentwise Definition of Scalar Multiplication on Product Types

Informal description

For any family of types $(\alpha_i)$ and $(\beta_i)$ where each $\alpha_i$ has a scalar multiplication operation on $\beta_i$, the scalar multiplication of $s \in \prod_i \alpha_i$ and $x \in \prod_i \beta_i$ is defined componentwise as $(s \bullet x)_i = s_i \bullet x_i$ for each index $i$.

Pi.smul_apply' theorem

[∀ i, SMul (α i) (β i)] (s : ∀ i, α i) (x : ∀ i, β i) : (s • x) i = s i • x i

Full source

@[to_additive (attr := simp)]
lemma smul_apply' [∀ i, SMul (α i) (β i)] (s : ∀ i, α i) (x : ∀ i, β i) : (s • x) i = s i • x i :=
  rfl

Componentwise Scalar Multiplication Formula for Product Types

Informal description

For any family of types $(\alpha_i)$ and $(\beta_i)$ where each $\alpha_i$ has a scalar multiplication operation on $\beta_i$, and for any elements $s \in \prod_i \alpha_i$ and $x \in \prod_i \beta_i$, the $i$-th component of the scalar product $s \bullet x$ is equal to the scalar product of the $i$-th components of $s$ and $x$, i.e., $(s \bullet x)_i = s_i \bullet x_i$.

Pi.isScalarTower instance

 [SMul M N] [∀ i, SMul N (α i)] [∀ i, SMul M (α i)] [∀ i, IsScalarTower M N (α i)] : IsScalarTower M N (∀ i, α i)

Full source

@[to_additive]
instance isScalarTower [SMul M N] [∀ i, SMul N (α i)] [∀ i, SMul M (α i)]
    [∀ i, IsScalarTower M N (α i)] : IsScalarTower M N (∀ i, α i) where
  smul_assoc x y z := funext fun i ↦ smul_assoc x y (z i)

Scalar Tower Condition for Pointwise Scalar Multiplication on Product Types

Informal description

For any type families $\alpha$ and $\beta$ indexed by $I$, if for each $i \in I$ there is a scalar multiplication operation between $M$ and $\alpha_i$, between $N$ and $\alpha_i$, and between $M$ and $N$, and if these operations satisfy the scalar tower condition for each $i$, then the pointwise scalar multiplication operations on the product types $\prod_{i} \alpha_i$ and $\prod_{i} \beta_i$ also satisfy the scalar tower condition.

Pi.isScalarTower' instance

 [∀ i, SMul M (α i)] [∀ i, SMul (α i) (β i)] [∀ i, SMul M (β i)] [∀ i, IsScalarTower M (α i) (β i)] :
  IsScalarTower M (∀ i, α i) (∀ i, β i)

Full source

@[to_additive]
instance isScalarTower' [∀ i, SMul M (α i)] [∀ i, SMul (α i) (β i)] [∀ i, SMul M (β i)]
    [∀ i, IsScalarTower M (α i) (β i)] : IsScalarTower M (∀ i, α i) (∀ i, β i) where
  smul_assoc x y z := funext fun i ↦ smul_assoc x (y i) (z i)

Scalar Tower Condition for Pointwise Scalar Multiplication on Product Types

Informal description

For any family of types $(\alpha_i)$ and $(\beta_i)$ where each $\alpha_i$ has a scalar multiplication operation on $\beta_i$, and for any scalar type $M$ such that for each $i$, $M$ has a scalar multiplication operation on $\alpha_i$ and $\beta_i$, and these operations satisfy the scalar tower condition for each $i$, then the pointwise scalar multiplication operations on the product types $\prod_i \alpha_i$ and $\prod_i \beta_i$ also satisfy the scalar tower condition.

Pi.isScalarTower'' instance

 [∀ i, SMul (α i) (β i)] [∀ i, SMul (β i) (γ i)] [∀ i, SMul (α i) (γ i)] [∀ i, IsScalarTower (α i) (β i) (γ i)] :
  IsScalarTower (∀ i, α i) (∀ i, β i) (∀ i, γ i)

Full source

@[to_additive]
instance isScalarTower'' [∀ i, SMul (α i) (β i)] [∀ i, SMul (β i) (γ i)] [∀ i, SMul (α i) (γ i)]
    [∀ i, IsScalarTower (α i) (β i) (γ i)] : IsScalarTower (∀ i, α i) (∀ i, β i) (∀ i, γ i) where
  smul_assoc x y z := funext fun i ↦ smul_assoc (x i) (y i) (z i)

Scalar Tower Condition for Pointwise Scalar Multiplication on Triple Product Types

Informal description

For any family of types $(\alpha_i)$, $(\beta_i)$, and $(\gamma_i)$ where each $\alpha_i$ has a scalar multiplication operation on $\beta_i$, each $\beta_i$ has a scalar multiplication operation on $\gamma_i$, and each $\alpha_i$ has a scalar multiplication operation on $\gamma_i$, if these operations satisfy the scalar tower condition for each $i$ (i.e., $a \cdot (b \cdot c) = (a \cdot b) \cdot c$ for all $a \in \alpha_i$, $b \in \beta_i$, $c \in \gamma_i$), then the pointwise scalar multiplication operations on the product types $\prod_i \alpha_i$, $\prod_i \beta_i$, and $\prod_i \gamma_i$ also satisfy the scalar tower condition.

Pi.smulCommClass instance

[∀ i, SMul M (α i)] [∀ i, SMul N (α i)] [∀ i, SMulCommClass M N (α i)] : SMulCommClass M N (∀ i, α i)

Full source

@[to_additive]
instance smulCommClass [∀ i, SMul M (α i)] [∀ i, SMul N (α i)] [∀ i, SMulCommClass M N (α i)] :
    SMulCommClass M N (∀ i, α i) where
  smul_comm x y z := funext fun i ↦ smul_comm x y (z i)

Commutativity of Scalar Multiplication on Product Types

Informal description

For any type families $\alpha_i$ and scalar types $M$, $N$, if for each $i$ the scalar multiplication operations of $M$ and $N$ on $\alpha_i$ commute (i.e., $m \cdot (n \cdot a_i) = n \cdot (m \cdot a_i)$ for all $m \in M$, $n \in N$, $a_i \in \alpha_i$), then the scalar multiplications of $M$ and $N$ on the product type $\forall i, \alpha_i$ also commute.

Pi.smulCommClass' instance

 [∀ i, SMul M (β i)] [∀ i, SMul (α i) (β i)] [∀ i, SMulCommClass M (α i) (β i)] : SMulCommClass M (∀ i, α i) (∀ i, β i)

Full source

@[to_additive]
instance smulCommClass' [∀ i, SMul M (β i)] [∀ i, SMul (α i) (β i)]
    [∀ i, SMulCommClass M (α i) (β i)] : SMulCommClass M (∀ i, α i) (∀ i, β i) :=
  ⟨fun x y z => funext fun i ↦ smul_comm x (y i) (z i)⟩

Commutativity of Scalar Multiplication on Product Types with Mixed Scalars

Informal description

For any family of types $(\alpha_i)$ and $(\beta_i)$ indexed by $i \in \iota$, if each $\beta_i$ has a scalar multiplication by $M$ and by $\alpha_i$, and if the scalar multiplications of $M$ and $\alpha_i$ commute on each $\beta_i$ (i.e., $m \cdot (a_i \cdot b_i) = a_i \cdot (m \cdot b_i)$ for all $m \in M$, $a_i \in \alpha_i$, $b_i \in \beta_i$), then the scalar multiplications of $M$ and $\prod_i \alpha_i$ commute on $\prod_i \beta_i$.

Pi.smulCommClass'' instance

 [∀ i, SMul (β i) (γ i)] [∀ i, SMul (α i) (γ i)] [∀ i, SMulCommClass (α i) (β i) (γ i)] :
  SMulCommClass (∀ i, α i) (∀ i, β i) (∀ i, γ i)

Full source

@[to_additive]
instance smulCommClass'' [∀ i, SMul (β i) (γ i)] [∀ i, SMul (α i) (γ i)]
    [∀ i, SMulCommClass (α i) (β i) (γ i)] : SMulCommClass (∀ i, α i) (∀ i, β i) (∀ i, γ i) where
  smul_comm x y z := funext fun i ↦ smul_comm (x i) (y i) (z i)

Commutativity of Componentwise Scalar Multiplication on Triple Product Types

Informal description

For any family of types $(\alpha_i)$, $(\beta_i)$, and $(\gamma_i)$ where for each $i$, $\alpha_i$ and $\beta_i$ have scalar multiplication operations on $\gamma_i$ that commute (i.e., $a \cdot (b \cdot c) = b \cdot (a \cdot c)$ for all $a \in \alpha_i$, $b \in \beta_i$, $c \in \gamma_i$), then the scalar multiplications of $\prod_i \alpha_i$ and $\prod_i \beta_i$ on $\prod_i \gamma_i$ also commute.

Pi.isCentralScalar instance

 [∀ i, SMul M (α i)] [∀ i, SMul Mᵐᵒᵖ (α i)] [∀ i, IsCentralScalar M (α i)] : IsCentralScalar M (∀ i, α i)

Full source

@[to_additive]
instance isCentralScalar [∀ i, SMul M (α i)] [∀ i, SMul Mᵐᵒᵖ (α i)] [∀ i, IsCentralScalar M (α i)] :
    IsCentralScalar M (∀ i, α i) where
  op_smul_eq_smul _ _ := funext fun _ ↦ op_smul_eq_smul _ _

Central Scalar Multiplication on Product Types

Informal description

For any family of types $\alpha_i$ indexed by $i \in \iota$, if each $\alpha_i$ has a scalar multiplication by $M$ and by the opposite monoid $M^{\text{op}}$, and if the scalar multiplication by $M$ is central for each $\alpha_i$, then the scalar multiplication by $M$ is also central for the product type $\forall i, \alpha_i$.

Pi.faithfulSMul_at theorem

[∀ i, SMul M (α i)] [∀ i, Nonempty (α i)] (i : ι) [FaithfulSMul M (α i)] : FaithfulSMul M (∀ i, α i)

Full source

/-- If `α i` has a faithful scalar action for a given `i`, then so does `Π i, α i`. This is
not an instance as `i` cannot be inferred. -/
@[to_additive
"If `α i` has a faithful additive action for a given `i`, then
so does `Π i, α i`. This is not an instance as `i` cannot be inferred"]
lemma faithfulSMul_at [∀ i, SMul M (α i)] [∀ i, Nonempty (α i)] (i : ι) [FaithfulSMul M (α i)] :
    FaithfulSMul M (∀ i, α i) where
  eq_of_smul_eq_smul h := eq_of_smul_eq_smul fun a : α i => by
    classical
    simpa using
      congr_fun (h <| Function.update (fun j => Classical.choice (‹∀ i, Nonempty (α i)› j)) i a) i

Faithfulness of Scalar Multiplication on Product Types at a Fixed Index

Informal description

Let $M$ be a type with a scalar multiplication action on each type $\alpha_i$ in a family indexed by $\iota$, and suppose each $\alpha_i$ is nonempty. If for some fixed index $i \in \iota$, the scalar multiplication of $M$ on $\alpha_i$ is faithful (i.e., distinct elements of $M$ act differently on $\alpha_i$), then the scalar multiplication of $M$ on the product type $\forall i, \alpha_i$ is also faithful.

Pi.faithfulSMul instance

 [Nonempty ι] [∀ i, SMul M (α i)] [∀ i, Nonempty (α i)] [∀ i, FaithfulSMul M (α i)] : FaithfulSMul M (∀ i, α i)

Full source

@[to_additive]
instance faithfulSMul [Nonempty ι] [∀ i, SMul M (α i)] [∀ i, Nonempty (α i)]
    [∀ i, FaithfulSMul M (α i)] : FaithfulSMul M (∀ i, α i) :=
  let ⟨i⟩ := ‹Nonempty ι›
  faithfulSMul_at i

Faithfulness of Scalar Multiplication on Product Types

Informal description

For a nonempty index set $\iota$ and a family of types $\alpha_i$ each equipped with a scalar multiplication action by $M$, if each $\alpha_i$ is nonempty and the scalar multiplication action of $M$ on each $\alpha_i$ is faithful (i.e., distinct elements of $M$ act differently on $\alpha_i$), then the scalar multiplication action of $M$ on the product type $\forall i, \alpha_i$ is also faithful.

Pi.mulAction instance

(M) {m : Monoid M} [∀ i, MulAction M (α i)] : @MulAction M (∀ i, α i) m

Full source

@[to_additive]
instance mulAction (M) {m : Monoid M} [∀ i, MulAction M (α i)] : @MulAction M (∀ i, α i) m where
  smul := (· • ·)
  mul_smul _ _ _ := funext fun _ ↦ mul_smul _ _ _
  one_smul _ := funext fun _ ↦ one_smul _ _

Pointwise Multiplicative Action on Product Types

Informal description

For any monoid $M$ and a family of types $\alpha_i$ each equipped with a multiplicative action of $M$, the product type $\forall i, \alpha_i$ (i.e., the type of functions from the index set $I$ to $\bigcup_i \alpha_i$) inherits a multiplicative action structure from $M$, where the action is defined pointwise.

Pi.mulAction' instance

 {m : ∀ i, Monoid (α i)} [∀ i, MulAction (α i) (β i)] : @MulAction (∀ i, α i) (∀ i, β i) (@Pi.monoid ι α m)

Full source

@[to_additive]
instance mulAction' {m : ∀ i, Monoid (α i)} [∀ i, MulAction (α i) (β i)] :
    @MulAction (∀ i, α i) (∀ i, β i)
      (@Pi.monoid ι α m) where
  smul := (· • ·)
  mul_smul _ _ _ := funext fun _ ↦ mul_smul _ _ _
  one_smul _ := funext fun _ ↦ one_smul _ _

Componentwise Multiplicative Action on Product Types

Informal description

For any family of monoids $(\alpha_i)$ and a family of types $(\beta_i)$ where each $\alpha_i$ has a multiplicative action on $\beta_i$, the product type $\prod_i \alpha_i$ has a multiplicative action on $\prod_i \beta_i$ defined componentwise.

Function.hasSMul instance

{α : Type*} [SMul M α] : SMul M (ι → α)

Full source

/-- Non-dependent version of `Pi.smul`. Lean gets confused by the dependent instance if this
is not present. -/
@[to_additive
"Non-dependent version of `Pi.vadd`. Lean gets confused by the dependent instance
if this is not present."]
instance hasSMul {α : Type*} [SMul M α] : SMul M (ι → α) := Pi.instSMul

Scalar Multiplication on Function Spaces

Informal description

For any type $M$ with a scalar multiplication operation on a type $\alpha$, the function space $\iota \to \alpha$ inherits a scalar multiplication operation from $\alpha$, where $(c \cdot f)(i) = c \cdot f(i)$ for any $c \in M$, $f \in \iota \to \alpha$, and $i \in \iota$.

Function.smulCommClass instance

{α : Type*} [SMul M α] [SMul N α] [SMulCommClass M N α] : SMulCommClass M N (ι → α)

Full source

/-- Non-dependent version of `Pi.smulCommClass`. Lean gets confused by the dependent instance if
this is not present. -/
@[to_additive
  "Non-dependent version of `Pi.vaddCommClass`. Lean gets confused by the dependent
  instance if this is not present."]
instance smulCommClass {α : Type*} [SMul M α] [SMul N α] [SMulCommClass M N α] :
    SMulCommClass M N (ι → α) := Pi.smulCommClass

Commutativity of Scalar Multiplication on Function Spaces

Informal description

For any type $\alpha$ with scalar multiplication operations from types $M$ and $N$, if the scalar multiplications of $M$ and $N$ on $\alpha$ commute (i.e., $m \cdot (n \cdot a) = n \cdot (m \cdot a)$ for all $m \in M$, $n \in N$, $a \in \alpha$), then the scalar multiplications of $M$ and $N$ on the function space $\iota \to \alpha$ also commute.

Function.update_smul theorem

 [∀ i, SMul M (α i)] [DecidableEq ι] (c : M) (f₁ : ∀ i, α i) (i : ι) (x₁ : α i) :
  update (c • f₁) i (c • x₁) = c • update f₁ i x₁

Full source

@[to_additive]
lemma update_smul [∀ i, SMul M (α i)] [DecidableEq ι] (c : M) (f₁ : ∀ i, α i)
    (i : ι) (x₁ : α i) : update (c • f₁) i (c • x₁) = c • update f₁ i x₁ :=
  funext fun j => (apply_update (β := α) (fun _ ↦ (c • ·)) f₁ i x₁ j).symm

Scalar Multiplication Commutes with Function Update

Informal description

Let $M$ be a type with a scalar multiplication operation on a family of types $\alpha_i$ for each $i \in \iota$, and let $\iota$ have decidable equality. For any scalar $c \in M$, function $f_1 : \forall i, \alpha_i$, index $i \in \iota$, and value $x_1 \in \alpha_i$, the following equality holds: \[ \text{update}\, (c \cdot f_1)\, i\, (c \cdot x_1) = c \cdot (\text{update}\, f_1\, i\, x_1). \]

Function.extend_smul theorem

 {M α β : Type*} [SMul M β] (r : M) (f : ι → α) (g : ι → β) (e : α → β) : extend f (r • g) (r • e) = r • extend f g e

Full source

@[to_additive]
lemma extend_smul {M α β : Type*} [SMul M β] (r : M) (f : ι → α) (g : ι → β) (e : α → β) :
    extend f (r • g) (r • e) = r • extend f g e := by
  funext x
  classical
  simp only [extend_def, Pi.smul_apply]
  split_ifs <;> rfl

Scalar Multiplication Commutes with Function Extension

Informal description

Let $M$, $\alpha$, and $\beta$ be types, with a scalar multiplication operation $M$ on $\beta$. For any scalar $r \in M$, functions $f : \iota \to \alpha$, $g : \iota \to \beta$, and $e : \alpha \to \beta$, the extension of $f$ with the scaled functions $r \cdot g$ and $r \cdot e$ equals the scaling of the extension of $f$ with $g$ and $e$ by $r$. That is, \[ \text{extend}\,f\,(r \cdot g)\,(r \cdot e) = r \cdot \text{extend}\,f\,g\,e. \]

Set.piecewise_smul theorem

 [∀ i, SMul M (α i)] (s : Set ι) [∀ i, Decidable (i ∈ s)] (c : M) (f₁ g₁ : ∀ i, α i) :
  s.piecewise (c • f₁) (c • g₁) = c • s.piecewise f₁ g₁

Full source

@[to_additive]
lemma piecewise_smul [∀ i, SMul M (α i)] (s : Set ι) [∀ i, Decidable (i ∈ s)]
    (c : M) (f₁ g₁ : ∀ i, α i) : s.piecewise (c • f₁) (c • g₁) = c • s.piecewise f₁ g₁ :=
  s.piecewise_op (δ' := α) f₁ _ fun _ ↦ (c • ·)

Scalar Multiplication Commutes with Piecewise Function Construction

Informal description

Let $M$ be a type with a scalar multiplication operation on a family of types $\alpha_i$ for each $i \in \iota$. Given a set $s \subseteq \iota$ with decidable membership, a scalar $c \in M$, and two functions $f_1, g_1 : \forall i, \alpha_i$, the piecewise function defined by $s$ on the scaled functions $c \cdot f_1$ and $c \cdot g_1$ is equal to the scalar multiplication of $c$ with the piecewise function defined by $s$ on $f_1$ and $g_1$. That is, \[ s.\text{piecewise}\, (c \cdot f_1)\, (c \cdot g_1) = c \cdot (s.\text{piecewise}\, f_1\, g_1). \]

See also