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.OptionMathlib.Algebra.Group.Action.PiMathlib.Algebra.Group.Action.SigmaMathlib.Algebra.Group.Action.Sum
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.
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 (α × β)
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 (α × β)
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 (α × β)
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 (α × β)
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 (α × β)
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 (α × β)
instance
Prod.faithfulSMulLeft
{M : Type u_1}
{α : Type u_5}
{β : Type u_6}
[SMul M α]
[SMul M β]
[FaithfulSMul M α]
[Nonempty β]
:
FaithfulSMul M (α × β)
instance
Prod.faithfulVAddLeft
{M : Type u_1}
{α : Type u_5}
{β : Type u_6}
[VAdd M α]
[VAdd M β]
[FaithfulVAdd M α]
[Nonempty β]
:
FaithfulVAdd M (α × β)
instance
Prod.faithfulSMulRight
{M : Type u_1}
{α : Type u_5}
{β : Type u_6}
[SMul M α]
[SMul M β]
[Nonempty α]
[FaithfulSMul M β]
:
FaithfulSMul M (α × β)
instance
Prod.faithfulVAddRight
{M : Type u_1}
{α : Type u_5}
{β : Type u_6}
[VAdd M α]
[VAdd M β]
[Nonempty α]
[FaithfulVAdd M β]
:
FaithfulVAdd M (α × β)
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)
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)
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)
Scalar multiplication as a homomorphism #
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' := ⋯ }
@[simp]
theorem
smulMulHom_apply
{α : Type u_5}
{β : Type u_6}
[Monoid α]
[Mul β]
[MulAction α β]
[IsScalarTower α β β]
[SMulCommClass α β β]
(a : α × β)
:
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' := ⋯ }
@[simp]
theorem
smulMonoidHom_apply
{α : Type u_5}
{β : Type u_6}
[Monoid α]
[MulOneClass β]
[MulAction α β]
[IsScalarTower α β β]
[SMulCommClass α β β]
(a✝ : α × β)
:
@[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 α]
:
Construct a MulAction by a product monoid from MulActions by the factors.
This is not an instance to avoid diamonds for example when α := M × N.
Equations
- MulAction.prodOfSMulCommClass M N α = MulAction.mk ⋯ ⋯
@[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 α]
:
Construct an AddAction by a product monoid from AddActions by the factors.
This is not an instance to avoid diamonds for example when α := M × N.
Equations
- AddAction.prodOfVAddCommClass M N α = AddAction.mk ⋯ ⋯