Mathlib.Algebra.GroupWithZero.Action.Pi

Pi.smulZeroClass instance

 (α) {n : ∀ i, Zero <| f i} [∀ i, SMulZeroClass α <| f i] : @SMulZeroClass α (∀ i : I, f i) (@Pi.instZero I f n)

Full source

instance smulZeroClass (α) {n : ∀ i, Zero <| f i} [∀ i, SMulZeroClass α <| f i] :
  @SMulZeroClass α (∀ i : I, f i) (@Pi.instZero I f n) where
  smul_zero _ := funext fun _ => smul_zero _

Componentwise Scalar Multiplication with Zero on Product Types

Informal description

For any type `α` and a family of types `f i` each equipped with a zero element and a scalar multiplication operation `SMulZeroClass α (f i)`, the product type `∀ i : I, f i` inherits a `SMulZeroClass` structure where scalar multiplication is defined componentwise.

Pi.smulZeroClass' instance

 {g : I → Type*} {n : ∀ i, Zero <| g i} [∀ i, SMulZeroClass (f i) (g i)] :
  @SMulZeroClass (∀ i, f i) (∀ i : I, g i) (@Pi.instZero I g n)

Full source

instance smulZeroClass' {g : I → Type*} {n : ∀ i, Zero <| g i} [∀ i, SMulZeroClass (f i) (g i)] :
  @SMulZeroClass (∀ i, f i) (∀ i : I, g i) (@Pi.instZero I g n) where
  smul_zero := by intros; ext x; exact smul_zero _

Componentwise Scalar Multiplication with Zero on Dependent Product Types

Informal description

For any family of types $(f_i)$ and $(g_i)$ where each $g_i$ has a zero element and each $f_i$ has a scalar multiplication operation on $g_i$ that preserves zero, the product type $\prod_i f_i$ has a scalar multiplication operation on $\prod_i g_i$ defined componentwise, which also preserves zero.

Pi.distribSMul instance

 (α) {n : ∀ i, AddZeroClass <| f i} [∀ i, DistribSMul α <| f i] : @DistribSMul α (∀ i : I, f i) (@Pi.addZeroClass I f n)

Full source

instance distribSMul (α) {n : ∀ i, AddZeroClass <| f i} [∀ i, DistribSMul α <| f i] :
  @DistribSMul α (∀ i : I, f i) (@Pi.addZeroClass I f n) where
  smul_zero _ := funext fun _ => smul_zero _
  smul_add _ _ _ := funext fun _ => smul_add _ _ _

Componentwise Distributive Scalar Multiplication on Product Types

Informal description

For any type $\alpha$ and a family of types $f_i$ each equipped with an additive zero class structure and a distributive scalar multiplication operation $\text{DistribSMul} \alpha (f_i)$, the product type $\prod_{i \in I} f_i$ inherits a $\text{DistribSMul}$ structure where scalar multiplication is defined componentwise.

Pi.distribSMul' instance

 {g : I → Type*} {n : ∀ i, AddZeroClass <| g i} [∀ i, DistribSMul (f i) (g i)] :
  @DistribSMul (∀ i, f i) (∀ i : I, g i) (@Pi.addZeroClass I g n)

Full source

instance distribSMul' {g : I → Type*} {n : ∀ i, AddZeroClass <| g i}
  [∀ i, DistribSMul (f i) (g i)] :
  @DistribSMul (∀ i, f i) (∀ i : I, g i) (@Pi.addZeroClass I g n) where
  smul_zero := by intros; ext x; exact smul_zero _
  smul_add := by intros; ext x; exact smul_add _ _ _

Componentwise Distributive Scalar Multiplication on Dependent Product Types

Informal description

For any family of types $(f_i)$ and $(g_i)$ where each $g_i$ has an additive zero class structure and each $f_i$ has a distributive scalar multiplication operation on $g_i$, the product type $\prod_i f_i$ has a distributive scalar multiplication operation on $\prod_i g_i$ defined componentwise.

Pi.distribMulAction instance

 (α) {m : Monoid α} {n : ∀ i, AddMonoid <| f i} [∀ i, DistribMulAction α <| f i] :
  @DistribMulAction α (∀ i : I, f i) m (@Pi.addMonoid I f n)

Full source

instance distribMulAction (α) {m : Monoid α} {n : ∀ i, AddMonoid <| f i}
    [∀ i, DistribMulAction α <| f i] : @DistribMulAction α (∀ i : I, f i) m (@Pi.addMonoid I f n) :=
  { Pi.mulAction _, Pi.distribSMul _ with }

Componentwise Distributive Multiplicative Action on Product Types

Informal description

For any monoid $\alpha$ and a family of additive monoids $(f_i)_{i \in I}$ where each $f_i$ has a distributive multiplicative action of $\alpha$, the product type $\prod_{i \in I} f_i$ inherits a distributive multiplicative action structure from $\alpha$, where the action is defined componentwise.

Pi.distribMulAction' instance

 {g : I → Type*} {m : ∀ i, Monoid (f i)} {n : ∀ i, AddMonoid <| g i} [∀ i, DistribMulAction (f i) (g i)] :
  @DistribMulAction (∀ i, f i) (∀ i : I, g i) (@Pi.monoid I f m) (@Pi.addMonoid I g n)

Full source

instance distribMulAction' {g : I → Type*} {m : ∀ i, Monoid (f i)} {n : ∀ i, AddMonoid <| g i}
    [∀ i, DistribMulAction (f i) (g i)] :
    @DistribMulAction (∀ i, f i) (∀ i : I, g i) (@Pi.monoid I f m) (@Pi.addMonoid I g n) :=
  { Pi.mulAction', Pi.distribSMul' with }

Componentwise Distributive Multiplicative Action on Product Types

Informal description

For any family of monoids $(f_i)_{i \in I}$ and a family of additive monoids $(g_i)_{i \in I}$ where each $f_i$ has a distributive multiplicative action on $g_i$, the product type $\prod_{i \in I} f_i$ has a distributive multiplicative action on $\prod_{i \in I} g_i$ defined componentwise.

Pi.single_smul theorem

 {α} [Monoid α] [∀ i, AddMonoid <| f i] [∀ i, DistribMulAction α <| f i] [DecidableEq I] (i : I) (r : α) (x : f i) :
  single i (r • x) = r • single i x

Full source

theorem single_smul {α} [Monoid α] [∀ i, AddMonoid <| f i] [∀ i, DistribMulAction α <| f i]
    [DecidableEq I] (i : I) (r : α) (x : f i) : single i (r • x) = r • single i x :=
  single_op (fun i : I => (r • · : f i → f i)) (fun _ => smul_zero _) _ _

Scalar Multiplication Commutes with Single Function in Product Types

Informal description

Let $I$ be a type with decidable equality, $\alpha$ be a monoid, and $(f_i)_{i \in I}$ be a family of additive monoids where each $f_i$ has a distributive multiplicative action of $\alpha$. For any index $i \in I$, scalar $r \in \alpha$, and element $x \in f_i$, the single function (which creates a vector with $x$ at position $i$ and zeros elsewhere) satisfies: \[ \text{single}_i(r \cdot x) = r \cdot \text{single}_i(x) \] where $\cdot$ denotes the scalar multiplication action.

Pi.single_smul' theorem

 {α β} [Monoid α] [AddMonoid β] [DistribMulAction α β] [DecidableEq I] (i : I) (r : α) (x : β) :
  single (f := fun _ => β) i (r • x) = r • single (f := fun _ => β) i x

Full source

/-- A version of `Pi.single_smul` for non-dependent functions. It is useful in cases where Lean
fails to apply `Pi.single_smul`. -/
theorem single_smul' {α β} [Monoid α] [AddMonoid β] [DistribMulAction α β] [DecidableEq I] (i : I)
    (r : α) (x : β) : single (f := fun _ => β) i (r • x) = r • single (f := fun _ => β) i x :=
  single_smul (f := fun _ => β) i r x

Scalar Multiplication Commutes with Single Function in Non-Dependent Product Types

Informal description

Let $\alpha$ be a monoid, $\beta$ an additive monoid with a distributive multiplicative action of $\alpha$ on $\beta$, and $I$ a type with decidable equality. For any index $i \in I$, scalar $r \in \alpha$, and element $x \in \beta$, the function `single` (which is zero everywhere except at $i$) satisfies: \[ \text{single}_i (r \cdot x) = r \cdot \text{single}_i x. \]

Pi.single_smul₀ theorem

 {g : I → Type*} [∀ i, MonoidWithZero (f i)] [∀ i, AddMonoid (g i)] [∀ i, DistribMulAction (f i) (g i)] [DecidableEq I]
  (i : I) (r : f i) (x : g i) : single i (r • x) = single i r • single i x

Full source

theorem single_smul₀ {g : I → Type*} [∀ i, MonoidWithZero (f i)] [∀ i, AddMonoid (g i)]
    [∀ i, DistribMulAction (f i) (g i)] [DecidableEq I] (i : I) (r : f i) (x : g i) :
    single i (r • x) = single i r • single i x :=
  single_op₂ (fun i : I => ((· • ·) : f i → g i → g i)) (fun _ => smul_zero _) _ _ _

Componentwise Scalar Multiplication of Single Elements in Product Types with Zero

Informal description

Let $I$ be a type, and for each $i \in I$, let $f_i$ be a monoid with zero and $g_i$ be an additive monoid, equipped with a distributive multiplicative action of $f_i$ on $g_i$. For any $i \in I$, $r \in f_i$, and $x \in g_i$, the function `single` (which constructs a function that is zero everywhere except at $i$) satisfies the identity: \[ \text{single}_i (r \cdot x) = \text{single}_i r \cdot \text{single}_i x. \]

Pi.mulDistribMulAction instance

 (α) {m : Monoid α} {n : ∀ i, Monoid <| f i} [∀ i, MulDistribMulAction α <| f i] :
  @MulDistribMulAction α (∀ i : I, f i) m (@Pi.monoid I f n)

Full source

instance mulDistribMulAction (α) {m : Monoid α} {n : ∀ i, Monoid <| f i}
    [∀ i, MulDistribMulAction α <| f i] :
    @MulDistribMulAction α (∀ i : I, f i) m (@Pi.monoid I f n) :=
  { Pi.mulAction _ with
    smul_one := fun _ => funext fun _ => smul_one _
    smul_mul := fun _ _ _ => funext fun _ => smul_mul' _ _ _ }

Pointwise Multiplicative Distributive Action on Product Types

Informal description

For any monoid $\alpha$ and a family of monoids $(f_i)_{i \in I}$ where each $f_i$ has a multiplicative distributive action by $\alpha$, the product type $\prod_{i \in I} f_i$ inherits a multiplicative distributive action structure from $\alpha$, where the action is defined pointwise.

Pi.mulDistribMulAction' instance

 {g : I → Type*} {m : ∀ i, Monoid (f i)} {n : ∀ i, Monoid <| g i} [∀ i, MulDistribMulAction (f i) (g i)] :
  @MulDistribMulAction (∀ i, f i) (∀ i : I, g i) (@Pi.monoid I f m) (@Pi.monoid I g n)

Full source

instance mulDistribMulAction' {g : I → Type*} {m : ∀ i, Monoid (f i)} {n : ∀ i, Monoid <| g i}
    [∀ i, MulDistribMulAction (f i) (g i)] :
    @MulDistribMulAction (∀ i, f i) (∀ i : I, g i) (@Pi.monoid I f m) (@Pi.monoid I g n) where
  smul_mul := by
    intros
    ext x
    apply smul_mul'
  smul_one := by
    intros
    ext x
    apply smul_one

Componentwise Multiplicative Distributive Action on Product Monoids

Informal description

For any family of monoids $(f_i)_{i \in I}$ and a family of monoids $(g_i)_{i \in I}$ where each $f_i$ has a multiplicative distributive action on $g_i$, the product monoid $\prod_{i \in I} f_i$ has a multiplicative distributive action on the product monoid $\prod_{i \in I} g_i$ defined componentwise.

See also