Documentation

Mathlib.GroupTheory.GroupAction.Prod

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_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] :

VAdd M (α × β)

Equations

Prod.vadd = { vadd := fun a p => (a +ᵥ p.fst, a +ᵥ p.snd) }

instance Prod.smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SMul M α] [inst : SMul M β] :

SMul M (α × β)

Equations

Prod.smul = { smul := fun a p => (a • p.fst, a • p.snd) }

@[simp]

theorem Prod.vadd_fst {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : VAdd M α] [inst : VAdd M β] (a : M) (x : α × β) :

(a +ᵥ x).fst = a +ᵥ x.fst

@[simp]

theorem Prod.smul_fst {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : SMul M α] [inst : SMul M β] (a : M) (x : α × β) :

(a • x).fst = a • x.fst

@[simp]

theorem Prod.vadd_snd {M : Type u_3} {α : Type u_2} {β : Type u_1} [inst : VAdd M α] [inst : VAdd M β] (a : M) (x : α × β) :

(a +ᵥ x).snd = a +ᵥ x.snd

@[simp]

theorem Prod.smul_snd {M : Type u_3} {α : Type u_2} {β : Type u_1} [inst : SMul M α] [inst : SMul M β] (a : M) (x : α × β) :

(a • x).snd = a • x.snd

@[simp]

theorem Prod.vadd_mk {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : VAdd M α] [inst : VAdd M β] (a : M) (b : α) (c : β) :

a +ᵥ (b, c) = (a +ᵥ b, a +ᵥ c)

@[simp]

theorem Prod.smul_mk {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : SMul M α] [inst : SMul M β] (a : M) (b : α) (c : β) :

a • (b, c) = (a • b, a • c)

theorem Prod.vadd_def {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : VAdd M α] [inst : VAdd M β] (a : M) (x : α × β) :

a +ᵥ x = (a +ᵥ x.fst, a +ᵥ x.snd)

theorem Prod.smul_def {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : SMul M α] [inst : SMul M β] (a : M) (x : α × β) :

a • x = (a • x.fst, a • x.snd)

@[simp]

theorem Prod.vadd_swap {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : VAdd M α] [inst : VAdd M β] (a : M) (x : α × β) :

Prod.swap (a +ᵥ x) = a +ᵥ Prod.swap x

@[simp]

theorem Prod.smul_swap {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : SMul M α] [inst : SMul M β] (a : M) (x : α × β) :

Prod.swap (a • x) = a • Prod.swap x

theorem Prod.smul_zero_mk {M : Type u_2} {β : Type u_3} [inst : SMul M β] {α : Type u_1} [inst : Monoid M] [inst : AddMonoid α] [inst : DistribMulAction M α] (a : M) (c : β) :

a • (0, c) = (0, a • c)

theorem Prod.smul_mk_zero {M : Type u_2} {α : Type u_3} [inst : SMul M α] {β : Type u_1} [inst : Monoid M] [inst : AddMonoid β] [inst : DistribMulAction M β] (a : M) (b : α) :

a • (b, 0) = (a • b, 0)

instance Prod.pow {E : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Pow α E] [inst : Pow β E] :

Pow (α × β) E

Equations

Prod.pow = { pow := fun p c => (p.fst ^ c, p.snd ^ c) }

@[simp]

theorem Prod.pow_fst {E : Type u_3} {α : Type u_1} {β : Type u_2} [inst : Pow α E] [inst : Pow β E] (p : α × β) (c : E) :

(p ^ c).fst = p.fst ^ c

@[simp]

theorem Prod.pow_snd {E : Type u_3} {α : Type u_1} {β : Type u_2} [inst : Pow α E] [inst : Pow β E] (p : α × β) (c : E) :

(p ^ c).snd = p.snd ^ c

@[simp]

theorem Prod.pow_mk {E : Type u_3} {α : Type u_1} {β : Type u_2} [inst : Pow α E] [inst : Pow β E] (c : E) (a : α) (b : β) :

(a, b) ^ c = (a ^ c, b ^ c)

theorem Prod.pow_def {E : Type u_3} {α : Type u_1} {β : Type u_2} [inst : Pow α E] [inst : Pow β E] (p : α × β) (c : E) :

p ^ c = (p.fst ^ c, p.snd ^ c)

@[simp]

theorem Prod.pow_swap {E : Type u_3} {α : Type u_1} {β : Type u_2} [inst : Pow α E] [inst : 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_3} {β : Type u_4} [inst : VAdd M α] [inst : VAdd M β] [inst : VAdd N α] [inst : VAdd N β] [inst : VAdd M N] [inst : VAddAssocClass M N α] [inst : VAddAssocClass M N β] :

VAddAssocClass M N (α × β)

Equations

@Prod.vaddAssocClass = @Prod.vaddAssocClass.proof_1

def Prod.vaddAssocClass.proof_1 {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [inst : VAdd M α] [inst : VAdd M β] [inst : VAdd N α] [inst : VAdd N β] [inst : VAdd M N] [inst : VAddAssocClass M N α] [inst : 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_3} {β : Type u_4} [inst : SMul M α] [inst : SMul M β] [inst : SMul N α] [inst : SMul N β] [inst : SMul M N] [inst : IsScalarTower M N α] [inst : IsScalarTower M N β] :

IsScalarTower M N (α × β)

Equations

@Prod.isScalarTower = @Prod.isScalarTower.proof_1

instance Prod.vaddCommClass {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [inst : VAdd M α] [inst : VAdd M β] [inst : VAdd N α] [inst : VAdd N β] [inst : VAddCommClass M N α] [inst : VAddCommClass M N β] :

VAddCommClass M N (α × β)

Equations

@Prod.vaddCommClass = @Prod.vaddCommClass.proof_1

def Prod.vaddCommClass.proof_1 {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [inst : VAdd M α] [inst : VAdd M β] [inst : VAdd N α] [inst : VAdd N β] [inst : VAddCommClass M N α] [inst : 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_3} {β : Type u_4} [inst : SMul M α] [inst : SMul M β] [inst : SMul N α] [inst : SMul N β] [inst : SMulCommClass M N α] [inst : SMulCommClass M N β] :

SMulCommClass M N (α × β)

Equations

@Prod.smulCommClass = @Prod.smulCommClass.proof_1

def Prod.isCentralVAdd.proof_1 {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : VAdd Mᵃᵒᵖ α] [inst : VAdd Mᵃᵒᵖ β] [inst : IsCentralVAdd M α] [inst : IsCentralVAdd M β] :

IsCentralVAdd M (α × β)

Equations

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

instance Prod.isCentralVAdd {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : VAdd Mᵃᵒᵖ α] [inst : VAdd Mᵃᵒᵖ β] [inst : IsCentralVAdd M α] [inst : IsCentralVAdd M β] :

IsCentralVAdd M (α × β)

Equations

@Prod.isCentralVAdd = @Prod.isCentralVAdd.proof_1

instance Prod.isCentralScalar {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SMul M α] [inst : SMul M β] [inst : SMul Mᵐᵒᵖ α] [inst : SMul Mᵐᵒᵖ β] [inst : IsCentralScalar M α] [inst : IsCentralScalar M β] :

IsCentralScalar M (α × β)

Equations

@Prod.isCentralScalar = @Prod.isCentralScalar.proof_1

instance Prod.faithfulVAddLeft {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : FaithfulVAdd M α] [inst : Nonempty β] :

FaithfulVAdd M (α × β)

Equations

@Prod.faithfulVAddLeft = @Prod.faithfulVAddLeft.proof_1

def Prod.faithfulVAddLeft.proof_1 {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : FaithfulVAdd M α] [inst : Nonempty β] :

FaithfulVAdd M (α × β)

Equations

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

abbrev Prod.faithfulVAddLeft.match_1 {β : Type u_1} (motive : Nonempty β → Prop) :

(x : Nonempty β) → ((b : β) → motive (_ : Nonempty β)) → motive x

Equations

Prod.faithfulVAddLeft.match_1 motive x h_1 = Nonempty.casesOn x fun val => h_1 val

instance Prod.faithfulSMulLeft {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SMul M α] [inst : SMul M β] [inst : FaithfulSMul M α] [inst : Nonempty β] :

FaithfulSMul M (α × β)

Equations

@Prod.faithfulSMulLeft = @Prod.faithfulSMulLeft.proof_1

def Prod.faithfulVAddRight.proof_1 {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : Nonempty α] [inst : FaithfulVAdd M β] :

FaithfulVAdd M (α × β)

Equations

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

instance Prod.faithfulVAddRight {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : Nonempty α] [inst : FaithfulVAdd M β] :

FaithfulVAdd M (α × β)

Equations

@Prod.faithfulVAddRight = @Prod.faithfulVAddRight.proof_1

instance Prod.faithfulSMulRight {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SMul M α] [inst : SMul M β] [inst : Nonempty α] [inst : FaithfulSMul M β] :

FaithfulSMul M (α × β)

Equations

@Prod.faithfulSMulRight = @Prod.faithfulSMulRight.proof_1

def Prod.vaddCommClassBoth.proof_1 {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add N] [inst : Add P] [inst : VAdd M N] [inst : VAdd M P] [inst : VAddCommClass M N N] [inst : 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.vaddCommClassBoth {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add N] [inst : Add P] [inst : VAdd M N] [inst : VAdd M P] [inst : VAddCommClass M N N] [inst : VAddCommClass M P P] :

VAddCommClass M (N × P) (N × P)

Equations

@Prod.vaddCommClassBoth = @Prod.vaddCommClassBoth.proof_1

instance Prod.smulCommClassBoth {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul N] [inst : Mul P] [inst : SMul M N] [inst : SMul M P] [inst : SMulCommClass M N N] [inst : SMulCommClass M P P] :

SMulCommClass M (N × P) (N × P)

Equations

@Prod.smulCommClassBoth = @Prod.smulCommClassBoth.proof_1

instance Prod.isScalarTowerBoth {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul N] [inst : Mul P] [inst : SMul M N] [inst : SMul M P] [inst : IsScalarTower M N N] [inst : IsScalarTower M P P] :

IsScalarTower M (N × P) (N × P)

Equations

@Prod.isScalarTowerBoth = @Prod.isScalarTowerBoth.proof_1

instance Prod.addAction {M : Type u_1} {α : Type u_2} {β : Type u_3} :

{x : AddMonoid M} → [inst : AddAction M α] → [inst : AddAction M β] → AddAction M (α × β)

Equations

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

def Prod.addAction.proof_2 {M : Type u_3} {α : Type u_1} {β : Type u_2} :

∀ {x : AddMonoid M} [inst : AddAction M α] [inst_1 : AddAction M β] (x_1 x_2 : M) (x_3 : α × β), ((x_1 + x_2 +ᵥ x_3).fst, (x_1 + x_2 +ᵥ x_3).snd) = ((x_1 +ᵥ (x_2 +ᵥ x_3)).fst, (x_1 +ᵥ (x_2 +ᵥ x_3)).snd)

Equations

(_ : ((x + x +ᵥ x).fst, (x + x +ᵥ x).snd) = ((x +ᵥ (x +ᵥ x)).fst, (x +ᵥ (x +ᵥ x)).snd)) = (_ : ((x + x +ᵥ x).fst, (x + x +ᵥ x).snd) = ((x +ᵥ (x +ᵥ x)).fst, (x +ᵥ (x +ᵥ x)).snd))

abbrev Prod.addAction.match_1 {α : Type u_1} {β : Type u_2} (motive : α × β → Prop) :

(x : α × β) → ((fst : α) → (snd : β) → motive (fst, snd)) → motive x

Equations

Prod.addAction.match_1 motive x h_1 = Prod.casesOn x fun fst snd => h_1 fst snd

def Prod.addAction.proof_1 {M : Type u_3} {α : Type u_1} {β : Type u_2} :

∀ {x : AddMonoid M} [inst : AddAction M α] [inst_1 : AddAction M β] (x_1 : α × β), 0 +ᵥ x_1 = x_1

Equations

(_ : 0 +ᵥ x = x) = (_ : 0 +ᵥ x = x)

instance Prod.mulAction {M : Type u_1} {α : Type u_2} {β : Type u_3} :

{x : Monoid M} → [inst : MulAction M α] → [inst : MulAction M β] → MulAction M (α × β)

Equations

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

instance Prod.smulZeroClass {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Zero M] [inst : Zero N] [inst : SMulZeroClass R M] [inst : SMulZeroClass R N] :

SMulZeroClass R (M × N)

Equations

Prod.smulZeroClass = SMulZeroClass.mk (_ : ∀ (x : R), ((x • 0).fst, (x • 0).snd) = (0.fst, 0.snd))

instance Prod.distribSMul {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : DistribSMul R M] [inst : 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)).fst, (x • (x_1 + x_2)).snd) = ((x • x_1 + x • x_2).fst, (x • x_1 + x • x_2).snd))

instance Prod.distribMulAction {R : Type u_1} {M : Type u_2} {N : Type u_3} :

{x : Monoid R} → [inst : AddMonoid M] → [inst_1 : AddMonoid N] → [inst_2 : DistribMulAction R M] → [inst_3 : 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 {R : Type u_1} {M : Type u_2} {N : Type u_3} :

{x : Monoid R} → [inst : Monoid M] → [inst_1 : Monoid N] → [inst_2 : MulDistribMulAction R M] → [inst_3 : 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_1} {β : Type u_2} [inst : Monoid α] [inst : Mul β] [inst : MulAction α β] [inst : IsScalarTower α β β] [inst : SMulCommClass α β β] (a : α × β) :

↑smulMulHom a = a.fst • a.snd

def smulMulHom {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst : Mul β] [inst : MulAction α β] [inst : IsScalarTower α β β] [inst : SMulCommClass α β β] :

α × β →ₙ* β

Scalar multiplication as a multiplicative homomorphism.

Equations

smulMulHom = { toFun := fun a => a.fst • a.snd, map_mul' := (_ : ∀ (x x_1 : α × β), (x.fst * x_1.fst) • (x.snd * x_1.snd) = x.fst • x.snd * x_1.fst • x_1.snd) }

@[simp]

theorem smulMonoidHom_apply {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst : MulOneClass β] [inst : MulAction α β] [inst : IsScalarTower α β β] [inst : SMulCommClass α β β] :

∀ (a : α × β), ↑smulMonoidHom a = MulHom.toFun smulMulHom a

def smulMonoidHom {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst : MulOneClass β] [inst : MulAction α β] [inst : IsScalarTower α β β] [inst : SMulCommClass α β β] :

α × β →* β

Scalar multiplication as a monoid homomorphism.

Equations

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