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.GroupTheory.GroupAction.OptionMathlib.GroupTheory.GroupAction.PiMathlib.GroupTheory.GroupAction.SigmaMathlib.GroupTheory.GroupAction.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.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 (α × β)
Equations
- ⋯ = ⋯
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 (α × β)
Equations
- ⋯ = ⋯
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 (α × β)
Equations
- ⋯ = ⋯
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 (α × β)
Equations
- ⋯ = ⋯
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 (α × β)
Equations
- ⋯ = ⋯
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 (α × β)
Equations
- ⋯ = ⋯
instance
Prod.faithfulVAddLeft
{M : Type u_1}
{α : Type u_5}
{β : Type u_6}
[VAdd M α]
[VAdd M β]
[FaithfulVAdd M α]
[Nonempty β]
:
FaithfulVAdd M (α × β)
Equations
- ⋯ = ⋯
instance
Prod.faithfulSMulLeft
{M : Type u_1}
{α : Type u_5}
{β : Type u_6}
[SMul M α]
[SMul M β]
[FaithfulSMul M α]
[Nonempty β]
:
FaithfulSMul M (α × β)
Equations
- ⋯ = ⋯
instance
Prod.faithfulVAddRight
{M : Type u_1}
{α : Type u_5}
{β : Type u_6}
[VAdd M α]
[VAdd M β]
[Nonempty α]
[FaithfulVAdd M β]
:
FaithfulVAdd M (α × β)
Equations
- ⋯ = ⋯
instance
Prod.faithfulSMulRight
{M : Type u_1}
{α : Type u_5}
{β : Type u_6}
[SMul M α]
[SMul M β]
[Nonempty α]
[FaithfulSMul M β]
:
FaithfulSMul M (α × β)
Equations
- ⋯ = ⋯
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)
Equations
- ⋯ = ⋯
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)
Equations
- ⋯ = ⋯
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)
Equations
- ⋯ = ⋯
instance
Prod.smulZeroClass
{R : Type u_7}
{M : Type u_8}
{N : Type u_9}
[Zero M]
[Zero N]
[SMulZeroClass R M]
[SMulZeroClass R N]
:
SMulZeroClass R (M × N)
Equations
- Prod.smulZeroClass = SMulZeroClass.mk ⋯
instance
Prod.distribSMul
{R : Type u_7}
{M : Type u_8}
{N : Type u_9}
[AddZeroClass M]
[AddZeroClass N]
[DistribSMul R M]
[DistribSMul R N]
:
DistribSMul R (M × N)
Equations
- Prod.distribSMul = DistribSMul.mk ⋯
instance
Prod.distribMulAction
{M : Type u_1}
{N : Type u_2}
{R : Type u_7}
[Monoid R]
[AddMonoid M]
[AddMonoid N]
[DistribMulAction R M]
[DistribMulAction R N]
:
DistribMulAction R (M × N)
Equations
- Prod.distribMulAction = let __src := Prod.mulAction; let __src_1 := Prod.distribSMul; DistribMulAction.mk ⋯ ⋯
instance
Prod.mulDistribMulAction
{M : Type u_1}
{N : Type u_2}
{R : Type u_7}
[Monoid R]
[Monoid M]
[Monoid N]
[MulDistribMulAction R M]
[MulDistribMulAction R N]
:
MulDistribMulAction R (M × N)
Equations
- Prod.mulDistribMulAction = MulDistribMulAction.mk ⋯ ⋯
Scalar multiplication as a homomorphism #
@[simp]
theorem
smulMulHom_apply
{α : Type u_5}
{β : Type u_6}
[Monoid α]
[Mul β]
[MulAction α β]
[IsScalarTower α β β]
[SMulCommClass α β β]
(a : α × β)
:
def
smulMulHom
{α : Type u_5}
{β : Type u_6}
[Monoid α]
[Mul β]
[MulAction α β]
[IsScalarTower α β β]
[SMulCommClass α β β]
:
Scalar multiplication as a multiplicative homomorphism.
Instances For
@[simp]
theorem
smulMonoidHom_apply
{α : Type u_5}
{β : Type u_6}
[Monoid α]
[MulOneClass β]
[MulAction α β]
[IsScalarTower α β β]
[SMulCommClass α β β]
:
def
smulMonoidHom
{α : Type u_5}
{β : Type u_6}
[Monoid α]
[MulOneClass β]
[MulAction α β]
[IsScalarTower α β β]
[SMulCommClass α β β]
:
Scalar multiplication as a monoid homomorphism.
Equations
- smulMonoidHom = let __src := smulMulHom; { toOneHom := { toFun := __src.toFun, map_one' := ⋯ }, map_mul' := ⋯ }
Instances For
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 ⋯ ⋯
Instances For
@[inline, reducible]
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 ⋯ ⋯
Instances For
theorem
AddAction.prodEquiv.proof_2
(M : Type u_3)
(N : Type u_2)
(α : Type u_1)
[AddMonoid M]
[AddMonoid N]
(_insts : (x : AddAction M α) ×' (x_1 : AddAction N α) ×' VAddCommClass M N α)
:
VAddCommClass M N α
theorem
AddAction.prodEquiv.proof_3
(M : Type u_3)
(N : Type u_2)
(α : Type u_1)
[AddMonoid M]
[AddMonoid N]
:
∀ (x : AddAction (M × N) α),
(fun (_insts : (x : AddAction M α) ×' (x_1 : AddAction N α) ×' VAddCommClass M N α) =>
let_fun this := ⋯;
AddAction.prodOfVAddCommClass M N α)
((fun (x : AddAction (M × N) α) =>
{ fst := AddAction.compHom α (AddMonoidHom.inl M N),
snd := { fst := AddAction.compHom α (AddMonoidHom.inr M N), snd := ⋯ } })
x) = x
theorem
AddAction.prodEquiv.proof_4
(M : Type u_1)
(N : Type u_3)
(α : Type u_2)
[AddMonoid M]
[AddMonoid N]
:
∀ (x : (x : AddAction M α) ×' (x_1 : AddAction N α) ×' VAddCommClass M N α),
(fun (x : AddAction (M × N) α) =>
{ fst := AddAction.compHom α (AddMonoidHom.inl M N),
snd := { fst := AddAction.compHom α (AddMonoidHom.inr M N), snd := ⋯ } })
((fun (_insts : (x : AddAction M α) ×' (x_1 : AddAction N α) ×' VAddCommClass M N α) =>
let_fun this := ⋯;
AddAction.prodOfVAddCommClass M N α)
x) = x
theorem
AddAction.prodEquiv.proof_1
(M : Type u_3)
(N : Type u_2)
(α : Type u_1)
[AddMonoid M]
[AddMonoid N]
:
∀ (x : AddAction (M × N) α), VAddCommClass M N α
@[inline, reducible]
abbrev
DistribMulAction.prodOfSMulCommClass
(M : Type u_1)
(N : Type u_2)
(α : Type u_5)
[Monoid M]
[Monoid N]
[AddMonoid α]
[DistribMulAction M α]
[DistribMulAction N α]
[SMulCommClass M N α]
:
DistribMulAction (M × N) α
Construct a DistribMulAction by a product monoid from DistribMulActions by the factors.
Equations
- DistribMulAction.prodOfSMulCommClass M N α = let __spread.0 := MulAction.prodOfSMulCommClass M N α; DistribMulAction.mk ⋯ ⋯
Instances For
def
DistribMulAction.prodEquiv
(M : Type u_1)
(N : Type u_2)
(α : Type u_5)
[Monoid M]
[Monoid N]
[AddMonoid α]
:
DistribMulAction (M × N) α ≃ (x : DistribMulAction M α) ×' (x_1 : DistribMulAction N α) ×' SMulCommClass M N α
A DistribMulAction by a product monoid is equivalent to
commuting DistribMulActions by the factors.
Equations
- One or more equations did not get rendered due to their size.