# Prod instances for additive and multiplicative actions #

This file defines instances for binary product of additive and multiplicative actions and provides scalar multiplication as a homomorphism from `α × β` to `β`.

## Main declarations #

- `smulMulHom`/`smulMonoidHom`: Scalar multiplication bundled as a multiplicative/monoid homomorphism.

## See also #

- `Mathlib/Algebra/Group/Action/Option.lean`
- `Mathlib/Algebra/Group/Action/Pi.lean`
- `Mathlib/Algebra/Group/Action/Sigma.lean`
- `Mathlib/Algebra/Group/Action/Sum.lean`

## Porting notes #

The `to_additive` attribute can be used to generate both the `smul` and `vadd` lemmas from the corresponding `pow` lemmas, as explained on zulip here: https://leanprover.zulipchat.com/#narrow/near/316087838

This was not done as part of the port in order to stay as close as possible to the mathlib3 code.

source
instance Prod.isScalarTower {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] [SMul N α] [SMul N β] [SMul M N] [IsScalarTower M N α] [IsScalarTower M N β] :
IsScalarTower M N (α × β)
source
instance Prod.vaddAssocClass {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [VAdd M α] [VAdd M β] [VAdd N α] [VAdd N β] [VAdd M N] [VAddAssocClass M N α] [VAddAssocClass M N β] :
VAddAssocClass M N (α × β)
source
instance Prod.smulCommClass {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] [SMul N α] [SMul N β] [SMulCommClass M N α] [SMulCommClass M N β] :
SMulCommClass M N (α × β)
source
instance Prod.vaddCommClass {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [VAdd M α] [VAdd M β] [VAdd N α] [VAdd N β] [VAddCommClass M N α] [VAddCommClass M N β] :
VAddCommClass M N (α × β)
source
instance Prod.isCentralScalar {M : Type u_1} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] [SMul M ᵐᵒᵖ α] [SMul M ᵐᵒᵖ β] [IsCentralScalar M α] [IsCentralScalar M β] :
IsCentralScalar M (α × β)
source
instance Prod.isCentralVAdd {M : Type u_1} {α : Type u_5} {β : Type u_6} [VAdd M α] [VAdd M β] [VAdd M ᵃᵒᵖ α] [VAdd M ᵃᵒᵖ β] [IsCentralVAdd M α] [IsCentralVAdd M β] :
IsCentralVAdd M (α × β)
source
instance Prod.faithfulSMulLeft {M : Type u_1} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] [FaithfulSMul M α] [Nonempty β] :
FaithfulSMul M (α × β)
source
instance Prod.faithfulVAddLeft {M : Type u_1} {α : Type u_5} {β : Type u_6} [VAdd M α] [VAdd M β] [FaithfulVAdd M α] [Nonempty β] :
FaithfulVAdd M (α × β)
source
instance Prod.faithfulSMulRight {M : Type u_1} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] [Nonempty α] [FaithfulSMul M β] :
FaithfulSMul M (α × β)
source
instance Prod.faithfulVAddRight {M : Type u_1} {α : Type u_5} {β : Type u_6} [VAdd M α] [VAdd M β] [Nonempty α] [FaithfulVAdd M β] :
FaithfulVAdd M (α × β)
source
instance Prod.smulCommClassBoth {M : Type u_1} {N : Type u_2} {P : Type u_3} [Mul N] [Mul P] [SMul M N] [SMul M P] [SMulCommClass M N N] [SMulCommClass M P P] :
SMulCommClass M (N × P) (N × P)
source
instance Prod.vaddCommClassBoth {M : Type u_1} {N : Type u_2} {P : Type u_3} [Add N] [Add P] [VAdd M N] [VAdd M P] [VAddCommClass M N N] [VAddCommClass M P P] :
VAddCommClass M (N × P) (N × P)
source
instance Prod.isScalarTowerBoth {M : Type u_1} {N : Type u_2} {P : Type u_3} [Mul N] [Mul P] [SMul M N] [SMul M P] [IsScalarTower M N N] [IsScalarTower M P P] :
IsScalarTower M (N × P) (N × P)
source
instance Prod.mulAction {M : Type u_1} {α : Type u_5} {β : Type u_6} [Monoid M] [MulAction M α] [MulAction M β] :
MulAction M (α × β)
Equations

- Prod.mulAction = { toSMul := Prod.instSMul, one_smul := ⋯, mul_smul := ⋯ }

source
instance Prod.addAction {M : Type u_1} {α : Type u_5} {β : Type u_6} [AddMonoid M] [AddAction M α] [AddAction M β] :
AddAction M (α × β)
Equations

- Prod.addAction = { toVAdd := Prod.instVAdd, zero_vadd := ⋯, add_vadd := ⋯ }

### Scalar multiplication as a homomorphism #

source
def smulMulHom {α : Type u_5} {β : Type u_6} [Monoid α] [Mul β] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] :
α × β →ₙ* β

Scalar multiplication as a multiplicative homomorphism.

Equations

- smulMulHom = { toFun := fun (a : α × β) => a.1 • a.2, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem smulMulHom_apply {α : Type u_5} {β : Type u_6} [Monoid α] [Mul β] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] (a : α × β) :
smulMulHom a = a.1 • a.2
source
def smulMonoidHom {α : Type u_5} {β : Type u_6} [Monoid α] [MulOneClass β] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] :
α × β →* β

Scalar multiplication as a monoid homomorphism.

Equations

- smulMonoidHom = { toFun := smulMulHom.toFun, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem smulMonoidHom_apply {α : Type u_5} {β : Type u_6} [Monoid α] [MulOneClass β] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] (a✝ : α × β) :
smulMonoidHom a✝ = smulMulHom.toFun a✝
source
@[reducible, inline]
abbrev MulAction.prodOfSMulCommClass (M : Type u_1) (N : Type u_2) (α : Type u_5) [Monoid M] [Monoid N] [MulAction M α] [MulAction N α] [SMulCommClass M N α] :
MulAction (M × N) α

Construct a `MulAction` by a product monoid from `MulAction`s by the factors. This is not an instance to avoid diamonds for example when `α := M × N`.

Equations

- MulAction.prodOfSMulCommClass M N α = { smul := fun (mn : M × N) (a : α) => mn.1 • mn.2 • a, one_smul := ⋯, mul_smul := ⋯ }

Instances For

source
@[reducible, inline]
abbrev AddAction.prodOfVAddCommClass (M : Type u_1) (N : Type u_2) (α : Type u_5) [AddMonoid M] [AddMonoid N] [AddAction M α] [AddAction N α] [VAddCommClass M N α] :
AddAction (M × N) α

Construct an `AddAction` by a product monoid from `AddAction`s by the factors. This is not an instance to avoid diamonds for example when `α := M × N`.

Equations

- AddAction.prodOfVAddCommClass M N α = { vadd := fun (mn : M × N) (a : α) => mn.1 +ᵥ mn.2 +ᵥ a, zero_vadd := ⋯, add_vadd := ⋯ }

Instances For

source
def MulAction.prodEquiv (M : Type u_1) (N : Type u_2) (α : Type u_5) [Monoid M] [Monoid N] :
MulAction (M × N) α ≃ (x : MulAction M α) ×' (x_1 : MulAction N α) ×' SMulCommClass M N α

A `MulAction` by a product monoid is equivalent to commuting `MulAction`s by the factors.

Equations

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

Instances For

source
def AddAction.prodEquiv (M : Type u_1) (N : Type u_2) (α : Type u_5) [AddMonoid M] [AddMonoid N] :
AddAction (M × N) α ≃ (x : AddAction M α) ×' (x_1 : AddAction N α) ×' VAddCommClass M N α

An `AddAction` by a product monoid is equivalent to commuting `AddAction`s by the factors.

Equations

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

Instances For