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.Option
• Mathlib.GroupTheory.GroupAction.Pi
• Mathlib.GroupTheory.GroupAction.Sigma
• Mathlib.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.vadd {M : Type u_1} {α : Type u_5} {β : Type u_6} [VAdd M α] [VAdd M β] : VAdd M (α × β)

Equations

• Prod.vadd = { vadd := fun (a : M) (p : α × β) => (a +ᵥ p.1, a +ᵥ p.2) }

instance Prod.smul {M : Type u_1} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] : SMul M (α × β)

Equations

• Prod.smul = { smul := fun (a : M) (p : α × β) => (a • p.1, a • p.2) }

@[simp]

theorem Prod.vadd_fst {M : Type u_1} {α : Type u_5} {β : Type u_6} [VAdd M α] [VAdd M β] (a : M) (x : α × β) : (a +ᵥ x).1 = a +ᵥ x.1

@[simp]

theorem Prod.smul_fst {M : Type u_1} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] (a : M) (x : α × β) : (a • x).1 = a • x.1

@[simp]

theorem Prod.vadd_snd {M : Type u_1} {α : Type u_5} {β : Type u_6} [VAdd M α] [VAdd M β] (a : M) (x : α × β) : (a +ᵥ x).2 = a +ᵥ x.2

@[simp]

theorem Prod.smul_snd {M : Type u_1} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] (a : M) (x : α × β) : (a • x).2 = a • x.2

@[simp]

theorem Prod.vadd_mk {M : Type u_1} {α : Type u_5} {β : Type u_6} [VAdd M α] [VAdd M β] (a : M) (b : α) (c : β) : a +ᵥ (b, c) = (a +ᵥ b, a +ᵥ c)

@[simp]

theorem Prod.smul_mk {M : Type u_1} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] (a : M) (b : α) (c : β) : a • (b, c) = (a • b, a • c)

theorem Prod.vadd_def {M : Type u_1} {α : Type u_5} {β : Type u_6} [VAdd M α] [VAdd M β] (a : M) (x : α × β) : a +ᵥ x = (a +ᵥ x.1, a +ᵥ x.2)

theorem Prod.smul_def {M : Type u_1} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] (a : M) (x : α × β) : a • x = (a • x.1, a • x.2)

@[simp]

theorem Prod.vadd_swap {M : Type u_1} {α : Type u_5} {β : Type u_6} [VAdd M α] [VAdd M β] (a : M) (x : α × β) : Prod.swap (a +ᵥ x) = a +ᵥ Prod.swap x

@[simp]

theorem Prod.smul_swap {M : Type u_1} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] (a : M) (x : α × β) : Prod.swap (a • x) = a • Prod.swap x

theorem Prod.smul_zero_mk {M : Type u_1} {β : Type u_6} [SMul M β] {α : Type u_7} [Monoid M] [AddMonoid α] [DistribMulAction M α] (a : M) (c : β) : a • (0, c) = (0, a • c)

theorem Prod.smul_mk_zero {M : Type u_1} {α : Type u_5} [SMul M α] {β : Type u_7} [Monoid M] [AddMonoid β] [DistribMulAction M β] (a : M) (b : α) : a • (b, 0) = (a • b, 0)

instance Prod.pow {E : Type u_4} {α : Type u_5} {β : Type u_6} [Pow α E] [Pow β E] : Pow (α × β) E

Equations

• Prod.pow = { pow := fun (p : α × β) (c : E) => (p.1 ^ c, p.2 ^ c) }

@[simp]

theorem Prod.pow_fst {E : Type u_4} {α : Type u_5} {β : Type u_6} [Pow α E] [Pow β E] (p : α × β) (c : E) : (p ^ c).1 = p.1 ^ c

@[simp]

theorem Prod.pow_snd {E : Type u_4} {α : Type u_5} {β : Type u_6} [Pow α E] [Pow β E] (p : α × β) (c : E) : (p ^ c).2 = p.2 ^ c

@[simp]

theorem Prod.pow_mk {E : Type u_4} {α : Type u_5} {β : Type u_6} [Pow α E] [Pow β E] (c : E) (a : α) (b : β) : (a, b) ^ c = (a ^ c, b ^ c)

theorem Prod.pow_def {E : Type u_4} {α : Type u_5} {β : Type u_6} [Pow α E] [Pow β E] (p : α × β) (c : E) : p ^ c = (p.1 ^ c, p.2 ^ c)

@[simp]

theorem Prod.pow_swap {E : Type u_4} {α : Type u_5} {β : Type u_6} [Pow α E] [Pow β E] (p : α × β) (c : E) : Prod.swap (p ^ c) = Prod.swap p ^ c

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

• (_ : VAddAssocClass M N (α × β)) = (_ : VAddAssocClass M N (α × β))

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

• (_ : IsScalarTower M N (α × β)) = (_ : IsScalarTower 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 (α × β)

Equations

• (_ : VAddCommClass M N (α × β)) = (_ : VAddCommClass 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 (α × β)

Equations

• (_ : SMulCommClass M N (α × β)) = (_ : SMulCommClass M N (α × β))

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

• (_ : IsCentralVAdd M (α × β)) = (_ : IsCentralVAdd M (α × β))

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

• (_ : IsCentralScalar M (α × β)) = (_ : IsCentralScalar M (α × β))

abbrev Prod.faithfulVAddLeft.match_1 {β : Type u_1} (motive : Nonempty β → Prop) : ∀ (x : Nonempty β), (∀ (b : β), motive (_ : Nonempty β)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

instance Prod.faithfulVAddLeft {M : Type u_1} {α : Type u_5} {β : Type u_6} [VAdd M α] [VAdd M β] [FaithfulVAdd M α] [Nonempty β] : FaithfulVAdd M (α × β)

Equations

• (_ : FaithfulVAdd M (α × β)) = (_ : FaithfulVAdd M (α × β))

instance Prod.faithfulSMulLeft {M : Type u_1} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] [FaithfulSMul M α] [Nonempty β] : FaithfulSMul M (α × β)

Equations

• (_ : 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 (α × β)

Equations

• (_ : FaithfulVAdd M (α × β)) = (_ : FaithfulVAdd M (α × β))

instance Prod.faithfulSMulRight {M : Type u_1} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] [Nonempty α] [FaithfulSMul M β] : FaithfulSMul M (α × β)

Equations

• (_ : FaithfulSMul M (α × β)) = (_ : FaithfulSMul M (α × β))

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

• (_ : VAddCommClass M (N × P) (N × P)) = (_ : VAddCommClass M (N × P) (N × P))

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

• (_ : SMulCommClass M (N × P) (N × P)) = (_ : SMulCommClass 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)

Equations

• (_ : IsScalarTower M (N × P) (N × P)) = (_ : IsScalarTower M (N × P) (N × P))

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

Equations

• Prod.addAction = AddAction.mk (_ : ∀ (x : α × β), 0 +ᵥ x = x) (_ : ∀ (x x_1 : M) (x_2 : α × β), (x + x_1 +ᵥ x_2.1, x + x_1 +ᵥ x_2.2) = (x +ᵥ (x_1 +ᵥ x_2).1, x +ᵥ (x_1 +ᵥ x_2).2))

theorem Prod.addAction.proof_1 {M : Type u_3} {α : Type u_1} {β : Type u_2} [AddMonoid M] [AddAction M α] [AddAction M β] : ∀ (x : α × β), 0 +ᵥ x = x

abbrev Prod.addAction.match_1 {α : Type u_1} {β : Type u_2} (motive : α × β → Prop) : ∀ (x : α × β), (∀ (fst : α) (snd : β), motive (fst, snd)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

theorem Prod.addAction.proof_2 {M : Type u_3} {α : Type u_1} {β : Type u_2} [AddMonoid M] [AddAction M α] [AddAction M β] : ∀ (x x_1 : M) (x_2 : α × β), (x + x_1 +ᵥ x_2.1, x + x_1 +ᵥ x_2.2) = (x +ᵥ (x_1 +ᵥ x_2).1, x +ᵥ (x_1 +ᵥ x_2).2)

instance Prod.mulAction {M : Type u_1} {α : Type u_5} {β : Type u_6} [Monoid M] [MulAction M α] [MulAction M β] : MulAction M (α × β)

Equations

• Prod.mulAction = MulAction.mk (_ : ∀ (x : α × β), 1 • x = x) (_ : ∀ (x x_1 : M) (x_2 : α × β), ((x * x_1) • x_2.1, (x * x_1) • x_2.2) = (x • (x_1 • x_2).1, x • (x_1 • x_2).2))

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 (_ : ∀ (x : R), (x • 0.1, x • 0.2) = (0, 0))

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 (_ : ∀ (x : R) (x_1 x_2 : M × N), (x • (x_1 + x_2).1, x • (x_1 + x_2).2) = ((x • x_1).1 + (x • x_2).1, (x • x_1).2 + (x • x_2).2))

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 (_ : ∀ (a : R), a • 0 = 0) (_ : ∀ (a : R) (x y : M × N), a • (x + y) = a • x + a • y)

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

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

Scalar multiplication as a homomorphism

@[simp]

theorem smulMulHom_apply {α : Type u_5} {β : Type u_6} [Monoid α] [Mul β] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] (a : α × β) : smulMulHom a = a.1 • a.2

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' := (_ : ∀ (x x_1 : α × β), (x.1 * x_1.1) • (x.2 * x_1.2) = x.1 • x.2 * x_1.1 • x_1.2) }

@[simp]

theorem smulMonoidHom_apply {α : Type u_5} {β : Type u_6} [Monoid α] [MulOneClass β] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] : ∀ (a : α × β), smulMonoidHom a = smulMulHom.toFun a

def smulMonoidHom {α : Type u_5} {β : Type u_6} [Monoid α] [MulOneClass β] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] : α × β →* β

Scalar multiplication as a monoid homomorphism.

Equations

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

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 AddActions by the factors. This is not an instance to avoid diamonds for example when α := M × N.

Equations

• AddAction.prodOfVAddCommClass M N α = AddAction.mk (_ : ∀ (a : α), 0 +ᵥ (0.2 +ᵥ a) = a) (_ : ∀ (x y : M × N) (a : α), x.1 + y.1 +ᵥ (x.2 + y.2 +ᵥ a) = x.1 +ᵥ (x.2 +ᵥ (y.1 +ᵥ (y.2 +ᵥ a))))

theorem AddAction.prodOfVAddCommClass.proof_1 (M : Type u_2) (N : Type u_3) (α : Type u_1) [AddMonoid M] [AddMonoid N] [AddAction M α] [AddAction N α] (a : α) : 0 +ᵥ (0.2 +ᵥ a) = a

theorem AddAction.prodOfVAddCommClass.proof_2 (M : Type u_1) (N : Type u_2) (α : Type u_3) [AddMonoid M] [AddMonoid N] [AddAction M α] [AddAction N α] [VAddCommClass M N α] (x : M × N) (y : M × N) (a : α) : x.1 + y.1 +ᵥ (x.2 + y.2 +ᵥ a) = x.1 +ᵥ (x.2 +ᵥ (y.1 +ᵥ (y.2 +ᵥ a)))

@[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 α] : MulAction (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 (_ : ∀ (a : α), 1 • 1.2 • a = a) (_ : ∀ (x y : M × N) (a : α), (x.1 * y.1) • (x.2 * y.2) • a = x.1 • x.2 • y.1 • y.2 • a)

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 := (_ : VAddCommClass M N α); 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 := (_ : VAddCommClass M N α) } }) 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 := (_ : VAddCommClass M N α) } }) ((fun (_insts : (x : AddAction M α) ×' (x_1 : AddAction N α) ×' VAddCommClass M N α) => let_fun this := (_ : VAddCommClass M N α); AddAction.prodOfVAddCommClass M N α) x) = x

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 AddActions by the factors.

Equations

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

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 α

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 MulActions by the factors.

Equations

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

@[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

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

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.