Monoid, group etc structures on `M × N` #

In this file we define one-binop (Monoid, Group etc) structures on M × N. We also prove trivial simp lemmas, and define the following operations on MonoidHoms:

fst M N : M × N →* M, snd M N : M × N →* N: projections Prod.fst and Prod.snd as MonoidHoms;
inl M N : M →* M × N, inr M N : N →* M × N: inclusions of first/second monoid into the product;
f.prod g : M →* N × P: sends x to (f x, g x);
When P is commutative, f.coprod g : M × N →* P sends (x, y) to f x * g y (without the commutativity assumption on P, see MonoidHom.noncommPiCoprod);
f.prodMap g : M × N → M' × N': prod.map f g as a MonoidHom, sends (x, y) to (f x, g y).

Main declarations #

mulMulHom/mulMonoidHom: Multiplication bundled as a multiplicative/monoid homomorphism.
divMonoidHom: Division bundled as a monoid homomorphism.

source

instance Prod.instAdd {M : Type u_3} {N : Type u_4} [Add M] [Add N] :

Add (M × N)

Equations

Prod.instAdd = { add := fun (p q : M × N) => (p.1 + q.1, p.2 + q.2) }

source

instance Prod.instMul {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] :

Mul (M × N)

Equations

Prod.instMul = { mul := fun (p q : M × N) => (p.1 * q.1, p.2 * q.2) }

source

@[simp]

theorem Prod.fst_add {M : Type u_3} {N : Type u_4} [Add M] [Add N] (p : M × N) (q : M × N) :

(p + q).1 = p.1 + q.1

source

@[simp]

theorem Prod.fst_mul {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (p : M × N) (q : M × N) :

(p * q).1 = p.1 * q.1

source

@[simp]

theorem Prod.snd_add {M : Type u_3} {N : Type u_4} [Add M] [Add N] (p : M × N) (q : M × N) :

(p + q).2 = p.2 + q.2

source

@[simp]

theorem Prod.snd_mul {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (p : M × N) (q : M × N) :

(p * q).2 = p.2 * q.2

source

@[simp]

theorem Prod.mk_add_mk {M : Type u_3} {N : Type u_4} [Add M] [Add N] (a₁ : M) (a₂ : M) (b₁ : N) (b₂ : N) :

(a₁, b₁) + (a₂, b₂) = (a₁ + a₂, b₁ + b₂)

source

@[simp]

theorem Prod.mk_mul_mk {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (a₁ : M) (a₂ : M) (b₁ : N) (b₂ : N) :

(a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)

source

@[simp]

theorem Prod.swap_add {M : Type u_3} {N : Type u_4} [Add M] [Add N] (p : M × N) (q : M × N) :

(p + q).swap = p.swap + q.swap

source

@[simp]

theorem Prod.swap_mul {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (p : M × N) (q : M × N) :

(p * q).swap = p.swap * q.swap

source

theorem Prod.add_def {M : Type u_3} {N : Type u_4} [Add M] [Add N] (p : M × N) (q : M × N) :

p + q = (p.1 + q.1, p.2 + q.2)

source

theorem Prod.mul_def {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (p : M × N) (q : M × N) :

p * q = (p.1 * q.1, p.2 * q.2)

source

theorem Prod.zero_mk_add_zero_mk {M : Type u_3} {N : Type u_4} [AddMonoid M] [Add N] (b₁ : N) (b₂ : N) :

(0, b₁) + (0, b₂) = (0, b₁ + b₂)

source

theorem Prod.one_mk_mul_one_mk {M : Type u_3} {N : Type u_4} [Monoid M] [Mul N] (b₁ : N) (b₂ : N) :

(1, b₁) * (1, b₂) = (1, b₁ * b₂)

source

theorem Prod.mk_zero_add_mk_zero {M : Type u_3} {N : Type u_4} [Add M] [AddMonoid N] (a₁ : M) (a₂ : M) :

(a₁, 0) + (a₂, 0) = (a₁ + a₂, 0)

source

theorem Prod.mk_one_mul_mk_one {M : Type u_3} {N : Type u_4} [Mul M] [Monoid N] (a₁ : M) (a₂ : M) :

(a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)

source

instance Prod.instZero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] :

Zero (M × N)

Equations

Prod.instZero = { zero := (0, 0) }

source

instance Prod.instOne {M : Type u_3} {N : Type u_4} [One M] [One N] :

One (M × N)

Equations

Prod.instOne = { one := (1, 1) }

source

@[simp]

theorem Prod.fst_zero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] :

0.1 = 0

source

@[simp]

theorem Prod.fst_one {M : Type u_3} {N : Type u_4} [One M] [One N] :

1.1 = 1

source

@[simp]

theorem Prod.snd_zero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] :

0.2 = 0

source

@[simp]

theorem Prod.snd_one {M : Type u_3} {N : Type u_4} [One M] [One N] :

1.2 = 1

source

theorem Prod.zero_eq_mk {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] :

0 = (0, 0)

source

theorem Prod.one_eq_mk {M : Type u_3} {N : Type u_4} [One M] [One N] :

1 = (1, 1)

source

@[simp]

theorem Prod.mk_zero_zero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] :

(0, 0) = 0

source

@[simp]

theorem Prod.mk_one_one {M : Type u_3} {N : Type u_4} [One M] [One N] :

(1, 1) = 1

source

@[simp]

theorem Prod.mk_eq_zero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] {x : M} {y : N} :

(x, y) = 0 ↔ x = 0 ∧ y = 0

source

@[simp]

theorem Prod.mk_eq_one {M : Type u_3} {N : Type u_4} [One M] [One N] {x : M} {y : N} :

(x, y) = 1 ↔ x = 1 ∧ y = 1

source

@[simp]

theorem Prod.swap_zero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] :

Prod.swap 0 = 0

source

@[simp]

theorem Prod.swap_one {M : Type u_3} {N : Type u_4} [One M] [One N] :

Prod.swap 1 = 1

source

theorem Prod.fst_add_snd {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] (p : M × N) :

(p.1, 0) + (0, p.2) = p

source

theorem Prod.fst_mul_snd {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] (p : M × N) :

(p.1, 1) * (1, p.2) = p

source

instance Prod.instNeg {M : Type u_3} {N : Type u_4} [Neg M] [Neg N] :

Neg (M × N)

Equations

Prod.instNeg = { neg := fun (p : M × N) => (-p.1, -p.2) }

source

instance Prod.instInv {M : Type u_3} {N : Type u_4} [Inv M] [Inv N] :

Inv (M × N)

Equations

Prod.instInv = { inv := fun (p : M × N) => (p.1⁻¹, p.2⁻¹) }

source

@[simp]

theorem Prod.fst_neg {G : Type u_1} {H : Type u_2} [Neg G] [Neg H] (p : G × H) :

(-p).1 = -p.1

source

@[simp]

theorem Prod.fst_inv {G : Type u_1} {H : Type u_2} [Inv G] [Inv H] (p : G × H) :

p⁻¹.1 = p.1⁻¹

source

@[simp]

theorem Prod.snd_neg {G : Type u_1} {H : Type u_2} [Neg G] [Neg H] (p : G × H) :

(-p).2 = -p.2

source

@[simp]

theorem Prod.snd_inv {G : Type u_1} {H : Type u_2} [Inv G] [Inv H] (p : G × H) :

p⁻¹.2 = p.2⁻¹

source

@[simp]

theorem Prod.neg_mk {G : Type u_1} {H : Type u_2} [Neg G] [Neg H] (a : G) (b : H) :

-(a, b) = (-a, -b)

source

@[simp]

theorem Prod.inv_mk {G : Type u_1} {H : Type u_2} [Inv G] [Inv H] (a : G) (b : H) :

(a, b)⁻¹ = (a⁻¹, b⁻¹)

source

@[simp]

theorem Prod.swap_neg {G : Type u_1} {H : Type u_2} [Neg G] [Neg H] (p : G × H) :

(-p).swap = -p.swap

source

@[simp]

theorem Prod.swap_inv {G : Type u_1} {H : Type u_2} [Inv G] [Inv H] (p : G × H) :

p⁻¹.swap = p.swap⁻¹

source

instance Prod.instInvolutiveNeg {M : Type u_3} {N : Type u_4} [InvolutiveNeg M] [InvolutiveNeg N] :

InvolutiveNeg (M × N)

Equations

Prod.instInvolutiveNeg = InvolutiveNeg.mk ⋯

source

instance Prod.instInvolutiveInv {M : Type u_3} {N : Type u_4} [InvolutiveInv M] [InvolutiveInv N] :

InvolutiveInv (M × N)

Equations

Prod.instInvolutiveInv = InvolutiveInv.mk ⋯

source

instance Prod.instSub {M : Type u_3} {N : Type u_4} [Sub M] [Sub N] :

Sub (M × N)

Equations

Prod.instSub = { sub := fun (p q : M × N) => (p.1 - q.1, p.2 - q.2) }

source

instance Prod.instDiv {M : Type u_3} {N : Type u_4} [Div M] [Div N] :

Div (M × N)

Equations

Prod.instDiv = { div := fun (p q : M × N) => (p.1 / q.1, p.2 / q.2) }

source

@[simp]

theorem Prod.fst_sub {G : Type u_1} {H : Type u_2} [Sub G] [Sub H] (a : G × H) (b : G × H) :

(a - b).1 = a.1 - b.1

source

@[simp]

theorem Prod.fst_div {G : Type u_1} {H : Type u_2} [Div G] [Div H] (a : G × H) (b : G × H) :

(a / b).1 = a.1 / b.1

source

@[simp]

theorem Prod.snd_sub {G : Type u_1} {H : Type u_2} [Sub G] [Sub H] (a : G × H) (b : G × H) :

(a - b).2 = a.2 - b.2

source

@[simp]

theorem Prod.snd_div {G : Type u_1} {H : Type u_2} [Div G] [Div H] (a : G × H) (b : G × H) :

(a / b).2 = a.2 / b.2

source

@[simp]

theorem Prod.mk_sub_mk {G : Type u_1} {H : Type u_2} [Sub G] [Sub H] (x₁ : G) (x₂ : G) (y₁ : H) (y₂ : H) :

(x₁, y₁) - (x₂, y₂) = (x₁ - x₂, y₁ - y₂)

source

@[simp]

theorem Prod.mk_div_mk {G : Type u_1} {H : Type u_2} [Div G] [Div H] (x₁ : G) (x₂ : G) (y₁ : H) (y₂ : H) :

(x₁, y₁) / (x₂, y₂) = (x₁ / x₂, y₁ / y₂)

source

@[simp]

theorem Prod.swap_sub {G : Type u_1} {H : Type u_2} [Sub G] [Sub H] (a : G × H) (b : G × H) :

(a - b).swap = a.swap - b.swap

source

@[simp]

theorem Prod.swap_div {G : Type u_1} {H : Type u_2} [Div G] [Div H] (a : G × H) (b : G × H) :

(a / b).swap = a.swap / b.swap

source

instance Prod.instAddSemigroup {M : Type u_3} {N : Type u_4} [AddSemigroup M] [AddSemigroup N] :

AddSemigroup (M × N)

Equations

Prod.instAddSemigroup = AddSemigroup.mk ⋯

source

instance Prod.instSemigroup {M : Type u_3} {N : Type u_4} [Semigroup M] [Semigroup N] :

Semigroup (M × N)

Equations

Prod.instSemigroup = Semigroup.mk ⋯

source

instance Prod.instAddCommSemigroup {G : Type u_1} {H : Type u_2} [AddCommSemigroup G] [AddCommSemigroup H] :

AddCommSemigroup (G × H)

Equations

Prod.instAddCommSemigroup = AddCommSemigroup.mk ⋯

source

instance Prod.instCommSemigroup {G : Type u_1} {H : Type u_2} [CommSemigroup G] [CommSemigroup H] :

CommSemigroup (G × H)

Equations

Prod.instCommSemigroup = CommSemigroup.mk ⋯

source

instance Prod.instAddZeroClass {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :

AddZeroClass (M × N)

Equations

Prod.instAddZeroClass = AddZeroClass.mk ⋯ ⋯

source

instance Prod.instMulOneClass {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :

MulOneClass (M × N)

Equations

Prod.instMulOneClass = MulOneClass.mk ⋯ ⋯

source

instance Prod.instAddMonoid {M : Type u_3} {N : Type u_4} [AddMonoid M] [AddMonoid N] :

AddMonoid (M × N)

Equations

Prod.instAddMonoid = AddMonoid.mk ⋯ ⋯ (fun (z : ℕ) (a : M × N) => (AddMonoid.nsmul z a.1, AddMonoid.nsmul z a.2)) ⋯ ⋯

source

instance Prod.instMonoid {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] :

Monoid (M × N)

Equations

Prod.instMonoid = Monoid.mk ⋯ ⋯ (fun (z : ℕ) (a : M × N) => (Monoid.npow z a.1, Monoid.npow z a.2)) ⋯ ⋯

source

instance Prod.subNegMonoid {G : Type u_1} {H : Type u_2} [SubNegMonoid G] [SubNegMonoid H] :

SubNegMonoid (G × H)

Equations

Prod.subNegMonoid = SubNegMonoid.mk ⋯ (fun (z : ℤ) (a : G × H) => (SubNegMonoid.zsmul z a.1, SubNegMonoid.zsmul z a.2)) ⋯ ⋯ ⋯

source

instance Prod.instDivInvMonoid {G : Type u_1} {H : Type u_2} [DivInvMonoid G] [DivInvMonoid H] :

DivInvMonoid (G × H)

Equations

Prod.instDivInvMonoid = DivInvMonoid.mk ⋯ (fun (z : ℤ) (a : G × H) => (DivInvMonoid.zpow z a.1, DivInvMonoid.zpow z a.2)) ⋯ ⋯ ⋯

source

instance Prod.instSubtractionMonoid {G : Type u_1} {H : Type u_2} [SubtractionMonoid G] [SubtractionMonoid H] :

SubtractionMonoid (G × H)

Equations

Prod.instSubtractionMonoid = SubtractionMonoid.mk ⋯ ⋯ ⋯

source

instance Prod.instDivisionMonoid {G : Type u_1} {H : Type u_2} [DivisionMonoid G] [DivisionMonoid H] :

DivisionMonoid (G × H)

Equations

Prod.instDivisionMonoid = DivisionMonoid.mk ⋯ ⋯ ⋯

source

instance Prod.SubtractionCommMonoid {G : Type u_1} {H : Type u_2} [SubtractionCommMonoid G] [SubtractionCommMonoid H] :

SubtractionCommMonoid (G × H)

Equations

Prod.SubtractionCommMonoid = SubtractionCommMonoid.mk ⋯

source

instance Prod.instDivisionCommMonoid {G : Type u_1} {H : Type u_2} [DivisionCommMonoid G] [DivisionCommMonoid H] :

DivisionCommMonoid (G × H)

Equations

Prod.instDivisionCommMonoid = DivisionCommMonoid.mk ⋯

source

instance Prod.instAddGroup {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] :

AddGroup (G × H)

Equations

Prod.instAddGroup = AddGroup.mk ⋯

source

instance Prod.instGroup {G : Type u_1} {H : Type u_2} [Group G] [Group H] :

Group (G × H)

Equations

Prod.instGroup = Group.mk ⋯

source

instance Prod.instIsAddLeftCancel {G : Type u_1} {H : Type u_2} [Add G] [Add H] [IsLeftCancelAdd G] [IsLeftCancelAdd H] :

IsLeftCancelAdd (G × H)

Equations

⋯ = ⋯

source

instance Prod.instIsLeftCancelMul {G : Type u_1} {H : Type u_2} [Mul G] [Mul H] [IsLeftCancelMul G] [IsLeftCancelMul H] :

IsLeftCancelMul (G × H)

Equations

⋯ = ⋯

source

instance Prod.instIsAddRightCancel {G : Type u_1} {H : Type u_2} [Add G] [Add H] [IsRightCancelAdd G] [IsRightCancelAdd H] :

IsRightCancelAdd (G × H)

Equations

⋯ = ⋯

source

instance Prod.instIsRightCancelMul {G : Type u_1} {H : Type u_2} [Mul G] [Mul H] [IsRightCancelMul G] [IsRightCancelMul H] :

IsRightCancelMul (G × H)

Equations

⋯ = ⋯

source

instance Prod.instIsAddCancel {G : Type u_1} {H : Type u_2} [Add G] [Add H] [IsCancelAdd G] [IsCancelAdd H] :

IsCancelAdd (G × H)

Equations

⋯ = ⋯

source

instance Prod.instIsCancelMul {G : Type u_1} {H : Type u_2} [Mul G] [Mul H] [IsCancelMul G] [IsCancelMul H] :

IsCancelMul (G × H)

Equations

⋯ = ⋯

source

instance Prod.instAddLeftCancelSemigroup {G : Type u_1} {H : Type u_2} [AddLeftCancelSemigroup G] [AddLeftCancelSemigroup H] :

AddLeftCancelSemigroup (G × H)

Equations

Prod.instAddLeftCancelSemigroup = AddLeftCancelSemigroup.mk ⋯

source

instance Prod.instLeftCancelSemigroup {G : Type u_1} {H : Type u_2} [LeftCancelSemigroup G] [LeftCancelSemigroup H] :

LeftCancelSemigroup (G × H)

Equations

Prod.instLeftCancelSemigroup = LeftCancelSemigroup.mk ⋯

source

instance Prod.instAddRightCancelSemigroup {G : Type u_1} {H : Type u_2} [AddRightCancelSemigroup G] [AddRightCancelSemigroup H] :

AddRightCancelSemigroup (G × H)

Equations

Prod.instAddRightCancelSemigroup = AddRightCancelSemigroup.mk ⋯

source

instance Prod.instRightCancelSemigroup {G : Type u_1} {H : Type u_2} [RightCancelSemigroup G] [RightCancelSemigroup H] :

RightCancelSemigroup (G × H)

Equations

Prod.instRightCancelSemigroup = RightCancelSemigroup.mk ⋯

source

instance Prod.instAddLeftCancelMonoid {M : Type u_3} {N : Type u_4} [AddLeftCancelMonoid M] [AddLeftCancelMonoid N] :

AddLeftCancelMonoid (M × N)

Equations

Prod.instAddLeftCancelMonoid = AddLeftCancelMonoid.mk ⋯

source

instance Prod.instLeftCancelMonoid {M : Type u_3} {N : Type u_4} [LeftCancelMonoid M] [LeftCancelMonoid N] :

LeftCancelMonoid (M × N)

Equations

Prod.instLeftCancelMonoid = LeftCancelMonoid.mk ⋯

source

instance Prod.instAddRightCancelMonoid {M : Type u_3} {N : Type u_4} [AddRightCancelMonoid M] [AddRightCancelMonoid N] :

AddRightCancelMonoid (M × N)

Equations

Prod.instAddRightCancelMonoid = AddRightCancelMonoid.mk ⋯

source

instance Prod.instRightCancelMonoid {M : Type u_3} {N : Type u_4} [RightCancelMonoid M] [RightCancelMonoid N] :

RightCancelMonoid (M × N)

Equations

Prod.instRightCancelMonoid = RightCancelMonoid.mk ⋯

source

instance Prod.instAddCancelMonoid {M : Type u_3} {N : Type u_4} [AddCancelMonoid M] [AddCancelMonoid N] :

AddCancelMonoid (M × N)

Equations

Prod.instAddCancelMonoid = AddCancelMonoid.mk ⋯

source

instance Prod.instCancelMonoid {M : Type u_3} {N : Type u_4} [CancelMonoid M] [CancelMonoid N] :

CancelMonoid (M × N)

Equations

Prod.instCancelMonoid = CancelMonoid.mk ⋯

source

instance Prod.instAddCommMonoid {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [AddCommMonoid N] :

AddCommMonoid (M × N)

Equations

Prod.instAddCommMonoid = AddCommMonoid.mk ⋯

source

instance Prod.instCommMonoid {M : Type u_3} {N : Type u_4} [CommMonoid M] [CommMonoid N] :

CommMonoid (M × N)

Equations

Prod.instCommMonoid = CommMonoid.mk ⋯

source

instance Prod.instAddCancelCommMonoid {M : Type u_3} {N : Type u_4} [AddCancelCommMonoid M] [AddCancelCommMonoid N] :

AddCancelCommMonoid (M × N)

Equations

Prod.instAddCancelCommMonoid = AddCancelCommMonoid.mk ⋯

source

instance Prod.instCancelCommMonoid {M : Type u_3} {N : Type u_4} [CancelCommMonoid M] [CancelCommMonoid N] :

CancelCommMonoid (M × N)

Equations

Prod.instCancelCommMonoid = CancelCommMonoid.mk ⋯

source

instance Prod.instAddCommGroup {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddCommGroup H] :

AddCommGroup (G × H)

Equations

Prod.instAddCommGroup = AddCommGroup.mk ⋯

source

instance Prod.instCommGroup {G : Type u_1} {H : Type u_2} [CommGroup G] [CommGroup H] :

CommGroup (G × H)

Equations

Prod.instCommGroup = CommGroup.mk ⋯

source

theorem AddSemiconjBy.prod {M : Type u_3} {N : Type u_4} [Add M] [Add N] {x : M × N} {y : M × N} {z : M × N} (hm : AddSemiconjBy x.1 y.1 z.1) (hn : AddSemiconjBy x.2 y.2 z.2) :

AddSemiconjBy x y z

source

theorem SemiconjBy.prod {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] {x : M × N} {y : M × N} {z : M × N} (hm : SemiconjBy x.1 y.1 z.1) (hn : SemiconjBy x.2 y.2 z.2) :

SemiconjBy x y z

source

theorem Prod.addSemiconjBy_iff {M : Type u_3} {N : Type u_4} [Add M] [Add N] {x : M × N} {y : M × N} {z : M × N} :

AddSemiconjBy x y z ↔ AddSemiconjBy x.1 y.1 z.1 ∧ AddSemiconjBy x.2 y.2 z.2

source

theorem Prod.semiconjBy_iff {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] {x : M × N} {y : M × N} {z : M × N} :

SemiconjBy x y z ↔ SemiconjBy x.1 y.1 z.1 ∧ SemiconjBy x.2 y.2 z.2

source

theorem AddCommute.prod {M : Type u_3} {N : Type u_4} [Add M] [Add N] {x : M × N} {y : M × N} (hm : AddCommute x.1 y.1) (hn : AddCommute x.2 y.2) :

AddCommute x y

source

theorem Commute.prod {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] {x : M × N} {y : M × N} (hm : Commute x.1 y.1) (hn : Commute x.2 y.2) :

Commute x y

source

theorem Prod.addCommute_iff {M : Type u_3} {N : Type u_4} [Add M] [Add N] {x : M × N} {y : M × N} :

AddCommute x y ↔ AddCommute x.1 y.1 ∧ AddCommute x.2 y.2

source

theorem Prod.commute_iff {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] {x : M × N} {y : M × N} :

Commute x y ↔ Commute x.1 y.1 ∧ Commute x.2 y.2

source

def AddHom.fst (M : Type u_3) (N : Type u_4) [Add M] [Add N] :

AddHom (M × N) M

Given additive magmas A, B, the natural projection homomorphism from A × B to A

Equations

AddHom.fst M N = { toFun := Prod.fst, map_add' := ⋯ }

Instances For

source

def MulHom.fst (M : Type u_3) (N : Type u_4) [Mul M] [Mul N] :

M × N →ₙ* M

Given magmas M, N, the natural projection homomorphism from M × N to M.

Equations

MulHom.fst M N = { toFun := Prod.fst, map_mul' := ⋯ }

Instances For

source

def AddHom.snd (M : Type u_3) (N : Type u_4) [Add M] [Add N] :

AddHom (M × N) N

Given additive magmas A, B, the natural projection homomorphism from A × B to B

Equations

AddHom.snd M N = { toFun := Prod.snd, map_add' := ⋯ }

Instances For

source

def MulHom.snd (M : Type u_3) (N : Type u_4) [Mul M] [Mul N] :

M × N →ₙ* N

Given magmas M, N, the natural projection homomorphism from M × N to N.

Equations

MulHom.snd M N = { toFun := Prod.snd, map_mul' := ⋯ }

Instances For

source

@[simp]

theorem AddHom.coe_fst {M : Type u_3} {N : Type u_4} [Add M] [Add N] :

⇑(AddHom.fst M N) = Prod.fst

source

@[simp]

theorem MulHom.coe_fst {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] :

⇑(MulHom.fst M N) = Prod.fst

source

@[simp]

theorem AddHom.coe_snd {M : Type u_3} {N : Type u_4} [Add M] [Add N] :

⇑(AddHom.snd M N) = Prod.snd

source

@[simp]

theorem MulHom.coe_snd {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] :

⇑(MulHom.snd M N) = Prod.snd

source

def AddHom.prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [Add P] (f : AddHom M N) (g : AddHom M P) :

AddHom M (N × P)

Combine two AddMonoidHoms f : AddHom M N, g : AddHom M P into f.prod g : AddHom M (N × P) given by (f.prod g) x = (f x, g x)

Equations

f.prod g = { toFun := Pi.prod ⇑f ⇑g, map_add' := ⋯ }

Instances For

source

def MulHom.prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [Mul N] [Mul P] (f : M →ₙ* N) (g : M →ₙ* P) :

M →ₙ* N × P

Combine two MonoidHoms f : M →ₙ* N, g : M →ₙ* P into f.prod g : M →ₙ* (N × P) given by (f.prod g) x = (f x, g x).

Equations

f.prod g = { toFun := Pi.prod ⇑f ⇑g, map_mul' := ⋯ }

Instances For

source

theorem AddHom.coe_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [Add P] (f : AddHom M N) (g : AddHom M P) :

⇑(f.prod g) = Pi.prod ⇑f ⇑g

source

theorem MulHom.coe_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [Mul N] [Mul P] (f : M →ₙ* N) (g : M →ₙ* P) :

⇑(f.prod g) = Pi.prod ⇑f ⇑g

source

@[simp]

theorem AddHom.prod_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [Add P] (f : AddHom M N) (g : AddHom M P) (x : M) :

(f.prod g) x = (f x, g x)

source

@[simp]

theorem MulHom.prod_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [Mul N] [Mul P] (f : M →ₙ* N) (g : M →ₙ* P) (x : M) :

(f.prod g) x = (f x, g x)

source

@[simp]

theorem AddHom.fst_comp_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [Add P] (f : AddHom M N) (g : AddHom M P) :

(AddHom.fst N P).comp (f.prod g) = f

source

@[simp]

theorem MulHom.fst_comp_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [Mul N] [Mul P] (f : M →ₙ* N) (g : M →ₙ* P) :

(MulHom.fst N P).comp (f.prod g) = f

source

@[simp]

theorem AddHom.snd_comp_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [Add P] (f : AddHom M N) (g : AddHom M P) :

(AddHom.snd N P).comp (f.prod g) = g

source

@[simp]

theorem MulHom.snd_comp_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [Mul N] [Mul P] (f : M →ₙ* N) (g : M →ₙ* P) :

(MulHom.snd N P).comp (f.prod g) = g

source

@[simp]

theorem AddHom.prod_unique {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [Add P] (f : AddHom M (N × P)) :

((AddHom.fst N P).comp f).prod ((AddHom.snd N P).comp f) = f

source

@[simp]

theorem MulHom.prod_unique {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [Mul N] [Mul P] (f : M →ₙ* N × P) :

((MulHom.fst N P).comp f).prod ((MulHom.snd N P).comp f) = f

source

def AddHom.prodMap {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [Add M] [Add N] [Add M'] [Add N'] (f : AddHom M M') (g : AddHom N N') :

AddHom (M × N) (M' × N')

Prod.map as an AddMonoidHom

Equations

f.prodMap g = (f.comp (AddHom.fst M N)).prod (g.comp (AddHom.snd M N))

Instances For

source

def MulHom.prodMap {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [Mul M] [Mul N] [Mul M'] [Mul N'] (f : M →ₙ* M') (g : N →ₙ* N') :

M × N →ₙ* M' × N'

Prod.map as a MonoidHom.

Equations

f.prodMap g = (f.comp (MulHom.fst M N)).prod (g.comp (MulHom.snd M N))

Instances For

source

theorem AddHom.prodMap_def {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [Add M] [Add N] [Add M'] [Add N'] (f : AddHom M M') (g : AddHom N N') :

f.prodMap g = (f.comp (AddHom.fst M N)).prod (g.comp (AddHom.snd M N))

source

theorem MulHom.prodMap_def {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [Mul M] [Mul N] [Mul M'] [Mul N'] (f : M →ₙ* M') (g : N →ₙ* N') :

f.prodMap g = (f.comp (MulHom.fst M N)).prod (g.comp (MulHom.snd M N))

source

@[simp]

theorem AddHom.coe_prodMap {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [Add M] [Add N] [Add M'] [Add N'] (f : AddHom M M') (g : AddHom N N') :

⇑(f.prodMap g) = Prod.map ⇑f ⇑g

source

@[simp]

theorem MulHom.coe_prodMap {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [Mul M] [Mul N] [Mul M'] [Mul N'] (f : M →ₙ* M') (g : N →ₙ* N') :

⇑(f.prodMap g) = Prod.map ⇑f ⇑g

source

theorem AddHom.prod_comp_prodMap {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} {N' : Type u_7} [Add M] [Add N] [Add M'] [Add N'] [Add P] (f : AddHom P M) (g : AddHom P N) (f' : AddHom M M') (g' : AddHom N N') :

(f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)

source

theorem MulHom.prod_comp_prodMap {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} {N' : Type u_7} [Mul M] [Mul N] [Mul M'] [Mul N'] [Mul P] (f : P →ₙ* M) (g : P →ₙ* N) (f' : M →ₙ* M') (g' : N →ₙ* N') :

(f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)

source

def AddHom.coprod {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [AddCommSemigroup P] (f : AddHom M P) (g : AddHom N P) :

AddHom (M × N) P

Coproduct of two AddHoms with the same codomain: f.coprod g (p : M × N) = f p.1 + g p.2. (Commutative codomain; for the general case, see AddHom.noncommCoprod)

Equations

f.coprod g = f.comp (AddHom.fst M N) + g.comp (AddHom.snd M N)

Instances For

source

def MulHom.coprod {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [Mul N] [CommSemigroup P] (f : M →ₙ* P) (g : N →ₙ* P) :

M × N →ₙ* P

Coproduct of two MulHoms with the same codomain: f.coprod g (p : M × N) = f p.1 * g p.2. (Commutative codomain; for the general case, see MulHom.noncommCoprod)

Equations

f.coprod g = f.comp (MulHom.fst M N) * g.comp (MulHom.snd M N)

Instances For

source

@[simp]

theorem AddHom.coprod_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [AddCommSemigroup P] (f : AddHom M P) (g : AddHom N P) (p : M × N) :

(f.coprod g) p = f p.1 + g p.2

source

@[simp]

theorem MulHom.coprod_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [Mul N] [CommSemigroup P] (f : M →ₙ* P) (g : N →ₙ* P) (p : M × N) :

(f.coprod g) p = f p.1 * g p.2

source

theorem AddHom.comp_coprod {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [AddCommSemigroup P] {Q : Type u_6} [AddCommSemigroup Q] (h : AddHom P Q) (f : AddHom M P) (g : AddHom N P) :

h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)

source

theorem MulHom.comp_coprod {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [Mul N] [CommSemigroup P] {Q : Type u_6} [CommSemigroup Q] (h : P →ₙ* Q) (f : M →ₙ* P) (g : N →ₙ* P) :

h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)

source

def AddMonoidHom.fst (M : Type u_3) (N : Type u_4) [AddZeroClass M] [AddZeroClass N] :

M × N →+ M

Given additive monoids A, B, the natural projection homomorphism from A × B to A

Equations

AddMonoidHom.fst M N = { toFun := Prod.fst, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

def MonoidHom.fst (M : Type u_3) (N : Type u_4) [MulOneClass M] [MulOneClass N] :

M × N →* M

Given monoids M, N, the natural projection homomorphism from M × N to M.

Equations

MonoidHom.fst M N = { toFun := Prod.fst, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

def AddMonoidHom.snd (M : Type u_3) (N : Type u_4) [AddZeroClass M] [AddZeroClass N] :

M × N →+ N

Given additive monoids A, B, the natural projection homomorphism from A × B to B

Equations

AddMonoidHom.snd M N = { toFun := Prod.snd, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

def MonoidHom.snd (M : Type u_3) (N : Type u_4) [MulOneClass M] [MulOneClass N] :

M × N →* N

Given monoids M, N, the natural projection homomorphism from M × N to N.

Equations

MonoidHom.snd M N = { toFun := Prod.snd, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

def AddMonoidHom.inl (M : Type u_3) (N : Type u_4) [AddZeroClass M] [AddZeroClass N] :

M →+ M × N

Given additive monoids A, B, the natural inclusion homomorphism from A to A × B.

Equations

AddMonoidHom.inl M N = { toFun := fun (x : M) => (x, 0), map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

def MonoidHom.inl (M : Type u_3) (N : Type u_4) [MulOneClass M] [MulOneClass N] :

M →* M × N

Given monoids M, N, the natural inclusion homomorphism from M to M × N.

Equations

MonoidHom.inl M N = { toFun := fun (x : M) => (x, 1), map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

def AddMonoidHom.inr (M : Type u_3) (N : Type u_4) [AddZeroClass M] [AddZeroClass N] :

N →+ M × N

Given additive monoids A, B, the natural inclusion homomorphism from B to A × B.

Equations

AddMonoidHom.inr M N = { toFun := fun (y : N) => (0, y), map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

def MonoidHom.inr (M : Type u_3) (N : Type u_4) [MulOneClass M] [MulOneClass N] :

N →* M × N

Given monoids M, N, the natural inclusion homomorphism from N to M × N.

Equations

MonoidHom.inr M N = { toFun := fun (y : N) => (1, y), map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

@[simp]

theorem AddMonoidHom.coe_fst {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :

⇑(AddMonoidHom.fst M N) = Prod.fst

source

@[simp]

theorem MonoidHom.coe_fst {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :

⇑(MonoidHom.fst M N) = Prod.fst

source

@[simp]

theorem AddMonoidHom.coe_snd {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :

⇑(AddMonoidHom.snd M N) = Prod.snd

source

@[simp]

theorem MonoidHom.coe_snd {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :

⇑(MonoidHom.snd M N) = Prod.snd

source

@[simp]

theorem AddMonoidHom.inl_apply {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] (x : M) :

(AddMonoidHom.inl M N) x = (x, 0)

source

@[simp]

theorem MonoidHom.inl_apply {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] (x : M) :

(MonoidHom.inl M N) x = (x, 1)

source

@[simp]

theorem AddMonoidHom.inr_apply {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] (y : N) :

(AddMonoidHom.inr M N) y = (0, y)

source

@[simp]

theorem MonoidHom.inr_apply {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] (y : N) :

(MonoidHom.inr M N) y = (1, y)

source

@[simp]

theorem AddMonoidHom.fst_comp_inl {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :

(AddMonoidHom.fst M N).comp (AddMonoidHom.inl M N) = AddMonoidHom.id M

source

@[simp]

theorem MonoidHom.fst_comp_inl {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :

(MonoidHom.fst M N).comp (MonoidHom.inl M N) = MonoidHom.id M

source

@[simp]

theorem AddMonoidHom.snd_comp_inl {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :

(AddMonoidHom.snd M N).comp (AddMonoidHom.inl M N) = 0

source

@[simp]

theorem MonoidHom.snd_comp_inl {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :

(MonoidHom.snd M N).comp (MonoidHom.inl M N) = 1

source

@[simp]

theorem AddMonoidHom.fst_comp_inr {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :

(AddMonoidHom.fst M N).comp (AddMonoidHom.inr M N) = 0

source

@[simp]

theorem MonoidHom.fst_comp_inr {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :

(MonoidHom.fst M N).comp (MonoidHom.inr M N) = 1

source

@[simp]

theorem AddMonoidHom.snd_comp_inr {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :

(AddMonoidHom.snd M N).comp (AddMonoidHom.inr M N) = AddMonoidHom.id N

source

@[simp]

theorem MonoidHom.snd_comp_inr {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :

(MonoidHom.snd M N).comp (MonoidHom.inr M N) = MonoidHom.id N

source

theorem AddMonoidHom.addCommute_inl_inr {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] (m : M) (n : N) :

AddCommute ((AddMonoidHom.inl M N) m) ((AddMonoidHom.inr M N) n)

source

theorem MonoidHom.commute_inl_inr {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] (m : M) (n : N) :

Commute ((MonoidHom.inl M N) m) ((MonoidHom.inr M N) n)

source

def AddMonoidHom.prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : M →+ N) (g : M →+ P) :

M →+ N × P

Combine two AddMonoidHoms f : M →+ N, g : M →+ P into f.prod g : M →+ N × P given by (f.prod g) x = (f x, g x)

Equations

f.prod g = { toFun := Pi.prod ⇑f ⇑g, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

def MonoidHom.prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : M →* N) (g : M →* P) :

M →* N × P

Combine two MonoidHoms f : M →* N, g : M →* P into f.prod g : M →* N × P given by (f.prod g) x = (f x, g x).

Equations

f.prod g = { toFun := Pi.prod ⇑f ⇑g, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

theorem AddMonoidHom.coe_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : M →+ N) (g : M →+ P) :

⇑(f.prod g) = Pi.prod ⇑f ⇑g

source

theorem MonoidHom.coe_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : M →* N) (g : M →* P) :

⇑(f.prod g) = Pi.prod ⇑f ⇑g

source

@[simp]

theorem AddMonoidHom.prod_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : M →+ N) (g : M →+ P) (x : M) :

(f.prod g) x = (f x, g x)

source

@[simp]

theorem MonoidHom.prod_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : M →* N) (g : M →* P) (x : M) :

(f.prod g) x = (f x, g x)

source

@[simp]

theorem AddMonoidHom.fst_comp_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : M →+ N) (g : M →+ P) :

(AddMonoidHom.fst N P).comp (f.prod g) = f

source

@[simp]

theorem MonoidHom.fst_comp_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : M →* N) (g : M →* P) :

(MonoidHom.fst N P).comp (f.prod g) = f

source

@[simp]

theorem AddMonoidHom.snd_comp_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : M →+ N) (g : M →+ P) :

(AddMonoidHom.snd N P).comp (f.prod g) = g

source

@[simp]

theorem MonoidHom.snd_comp_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : M →* N) (g : M →* P) :

(MonoidHom.snd N P).comp (f.prod g) = g

source

@[simp]

theorem AddMonoidHom.prod_unique {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : M →+ N × P) :

((AddMonoidHom.fst N P).comp f).prod ((AddMonoidHom.snd N P).comp f) = f

source

@[simp]

theorem MonoidHom.prod_unique {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : M →* N × P) :

((MonoidHom.fst N P).comp f).prod ((MonoidHom.snd N P).comp f) = f

source

def AddMonoidHom.prodMap {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] {M' : Type u_6} {N' : Type u_7} [AddZeroClass M'] [AddZeroClass N'] (f : M →+ M') (g : N →+ N') :

M × N →+ M' × N'

prod.map as an AddMonoidHom.

Equations

f.prodMap g = (f.comp (AddMonoidHom.fst M N)).prod (g.comp (AddMonoidHom.snd M N))

Instances For

source

def MonoidHom.prodMap {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] {M' : Type u_6} {N' : Type u_7} [MulOneClass M'] [MulOneClass N'] (f : M →* M') (g : N →* N') :

M × N →* M' × N'

prod.map as a MonoidHom.

Equations

f.prodMap g = (f.comp (MonoidHom.fst M N)).prod (g.comp (MonoidHom.snd M N))

Instances For

source

theorem AddMonoidHom.prodMap_def {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] {M' : Type u_6} {N' : Type u_7} [AddZeroClass M'] [AddZeroClass N'] (f : M →+ M') (g : N →+ N') :

f.prodMap g = (f.comp (AddMonoidHom.fst M N)).prod (g.comp (AddMonoidHom.snd M N))

source

theorem MonoidHom.prodMap_def {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] {M' : Type u_6} {N' : Type u_7} [MulOneClass M'] [MulOneClass N'] (f : M →* M') (g : N →* N') :

f.prodMap g = (f.comp (MonoidHom.fst M N)).prod (g.comp (MonoidHom.snd M N))

source

@[simp]

theorem AddMonoidHom.coe_prodMap {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] {M' : Type u_6} {N' : Type u_7} [AddZeroClass M'] [AddZeroClass N'] (f : M →+ M') (g : N →+ N') :

⇑(f.prodMap g) = Prod.map ⇑f ⇑g

source

@[simp]

theorem MonoidHom.coe_prodMap {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] {M' : Type u_6} {N' : Type u_7} [MulOneClass M'] [MulOneClass N'] (f : M →* M') (g : N →* N') :

⇑(f.prodMap g) = Prod.map ⇑f ⇑g

source

theorem AddMonoidHom.prod_comp_prodMap {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] {M' : Type u_6} {N' : Type u_7} [AddZeroClass M'] [AddZeroClass N'] [AddZeroClass P] (f : P →+ M) (g : P →+ N) (f' : M →+ M') (g' : N →+ N') :

(f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)

source

theorem MonoidHom.prod_comp_prodMap {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] {M' : Type u_6} {N' : Type u_7} [MulOneClass M'] [MulOneClass N'] [MulOneClass P] (f : P →* M) (g : P →* N) (f' : M →* M') (g' : N →* N') :

(f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)

source

def AddMonoidHom.coprod {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] (f : M →+ P) (g : N →+ P) :

M × N →+ P

Coproduct of two AddMonoidHoms with the same codomain: f.coprod g (p : M × N) = f p.1 + g p.2. (Commutative case; for the general case, see AddHom.noncommCoprod.)

Equations

f.coprod g = f.comp (AddMonoidHom.fst M N) + g.comp (AddMonoidHom.snd M N)

Instances For

source

def MonoidHom.coprod {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [CommMonoid P] (f : M →* P) (g : N →* P) :

M × N →* P

Coproduct of two MonoidHoms with the same codomain: f.coprod g (p : M × N) = f p.1 * g p.2. (Commutative case; for the general case, see MonoidHom.noncommCoprod.)

Equations

f.coprod g = f.comp (MonoidHom.fst M N) * g.comp (MonoidHom.snd M N)

Instances For

source

@[simp]

theorem AddMonoidHom.coprod_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] (f : M →+ P) (g : N →+ P) (p : M × N) :

(f.coprod g) p = f p.1 + g p.2

source

@[simp]

theorem MonoidHom.coprod_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [CommMonoid P] (f : M →* P) (g : N →* P) (p : M × N) :

(f.coprod g) p = f p.1 * g p.2

source

@[simp]

theorem AddMonoidHom.coprod_comp_inl {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] (f : M →+ P) (g : N →+ P) :

(f.coprod g).comp (AddMonoidHom.inl M N) = f

source

@[simp]

theorem MonoidHom.coprod_comp_inl {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [CommMonoid P] (f : M →* P) (g : N →* P) :

(f.coprod g).comp (MonoidHom.inl M N) = f

source

@[simp]

theorem AddMonoidHom.coprod_comp_inr {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] (f : M →+ P) (g : N →+ P) :

(f.coprod g).comp (AddMonoidHom.inr M N) = g

source

@[simp]

theorem MonoidHom.coprod_comp_inr {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [CommMonoid P] (f : M →* P) (g : N →* P) :

(f.coprod g).comp (MonoidHom.inr M N) = g

source

@[simp]

theorem AddMonoidHom.coprod_unique {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] (f : M × N →+ P) :

(f.comp (AddMonoidHom.inl M N)).coprod (f.comp (AddMonoidHom.inr M N)) = f

source

@[simp]

theorem MonoidHom.coprod_unique {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [CommMonoid P] (f : M × N →* P) :

(f.comp (MonoidHom.inl M N)).coprod (f.comp (MonoidHom.inr M N)) = f

source

@[simp]

theorem AddMonoidHom.coprod_inl_inr {M : Type u_6} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] :

(AddMonoidHom.inl M N).coprod (AddMonoidHom.inr M N) = AddMonoidHom.id (M × N)

source

@[simp]

theorem MonoidHom.coprod_inl_inr {M : Type u_6} {N : Type u_7} [CommMonoid M] [CommMonoid N] :

(MonoidHom.inl M N).coprod (MonoidHom.inr M N) = MonoidHom.id (M × N)

source

theorem AddMonoidHom.comp_coprod {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] {Q : Type u_6} [AddCommMonoid Q] (h : P →+ Q) (f : M →+ P) (g : N →+ P) :

h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)

source

theorem MonoidHom.comp_coprod {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [CommMonoid P] {Q : Type u_6} [CommMonoid Q] (h : P →* Q) (f : M →* P) (g : N →* P) :

h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)

source

def AddEquiv.prodComm {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :

M × N ≃+ N × M

The equivalence between M × N and N × M given by swapping the components is additive.

Equations

AddEquiv.prodComm = { toEquiv := Equiv.prodComm M N, map_add' := ⋯ }

Instances For

source

def MulEquiv.prodComm {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :

M × N ≃* N × M

The equivalence between M × N and N × M given by swapping the components is multiplicative.

Equations

MulEquiv.prodComm = { toEquiv := Equiv.prodComm M N, map_mul' := ⋯ }

Instances For

source

@[simp]

theorem AddEquiv.coe_prodComm {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :

⇑AddEquiv.prodComm = Prod.swap

source

@[simp]

theorem MulEquiv.coe_prodComm {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :

⇑MulEquiv.prodComm = Prod.swap

source

@[simp]

theorem AddEquiv.coe_prodComm_symm {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :

⇑AddEquiv.prodComm.symm = Prod.swap

source

@[simp]

theorem MulEquiv.coe_prodComm_symm {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :

⇑MulEquiv.prodComm.symm = Prod.swap

source

def AddEquiv.prodAssoc {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] :

(M × N) × P ≃+ M × N × P

The equivalence between (M × N) × P and M × (N × P) is additive.

Equations

AddEquiv.prodAssoc = { toEquiv := Equiv.prodAssoc M N P, map_add' := ⋯ }

Instances For

source

def MulEquiv.prodAssoc {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] :

(M × N) × P ≃* M × N × P

The equivalence between (M × N) × P and M × (N × P) is multiplicative.

Equations

MulEquiv.prodAssoc = { toEquiv := Equiv.prodAssoc M N P, map_mul' := ⋯ }

Instances For

source

@[simp]

theorem AddEquiv.coe_prodAssoc {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] :

⇑AddEquiv.prodAssoc = ⇑(Equiv.prodAssoc M N P)

source

@[simp]

theorem MulEquiv.coe_prodAssoc {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] :

⇑MulEquiv.prodAssoc = ⇑(Equiv.prodAssoc M N P)

source

@[simp]

theorem AddEquiv.coe_prodAssoc_symm {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] :

⇑AddEquiv.prodAssoc.symm = ⇑(Equiv.prodAssoc M N P).symm

source

@[simp]

theorem MulEquiv.coe_prodAssoc_symm {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] :

⇑MulEquiv.prodAssoc.symm = ⇑(Equiv.prodAssoc M N P).symm

source

def AddEquiv.prodProdProdComm (M : Type u_3) (N : Type u_4) [AddZeroClass M] [AddZeroClass N] (M' : Type u_6) (N' : Type u_7) [AddZeroClass N'] [AddZeroClass M'] :

(M × N) × M' × N' ≃+ (M × M') × N × N'

Four-way commutativity of Prod. The name matches mul_mul_mul_comm

Equations

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

Instances For

source

@[simp]

theorem AddEquiv.prodProdProdComm_apply (M : Type u_3) (N : Type u_4) [AddZeroClass M] [AddZeroClass N] (M' : Type u_6) (N' : Type u_7) [AddZeroClass N'] [AddZeroClass M'] (mnmn : (M × N) × M' × N') :

(AddEquiv.prodProdProdComm M N M' N') mnmn = ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2)

source

@[simp]

theorem MulEquiv.prodProdProdComm_apply (M : Type u_3) (N : Type u_4) [MulOneClass M] [MulOneClass N] (M' : Type u_6) (N' : Type u_7) [MulOneClass N'] [MulOneClass M'] (mnmn : (M × N) × M' × N') :

(MulEquiv.prodProdProdComm M N M' N') mnmn = ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2)

source

def MulEquiv.prodProdProdComm (M : Type u_3) (N : Type u_4) [MulOneClass M] [MulOneClass N] (M' : Type u_6) (N' : Type u_7) [MulOneClass N'] [MulOneClass M'] :

(M × N) × M' × N' ≃* (M × M') × N × N'

Four-way commutativity of Prod. The name matches mul_mul_mul_comm.

Equations

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

Instances For

source

@[simp]

theorem AddEquiv.prodProdProdComm_toEquiv (M : Type u_3) (N : Type u_4) [AddZeroClass M] [AddZeroClass N] (M' : Type u_6) (N' : Type u_7) [AddZeroClass N'] [AddZeroClass M'] :

↑(AddEquiv.prodProdProdComm M N M' N') = Equiv.prodProdProdComm M N M' N'

source

@[simp]

theorem MulEquiv.prodProdProdComm_toEquiv (M : Type u_3) (N : Type u_4) [MulOneClass M] [MulOneClass N] (M' : Type u_6) (N' : Type u_7) [MulOneClass N'] [MulOneClass M'] :

↑(MulEquiv.prodProdProdComm M N M' N') = Equiv.prodProdProdComm M N M' N'

source

@[simp]

theorem MulEquiv.prodProdProdComm_symm (M : Type u_3) (N : Type u_4) [MulOneClass M] [MulOneClass N] (M' : Type u_6) (N' : Type u_7) [MulOneClass N'] [MulOneClass M'] :

(MulEquiv.prodProdProdComm M N M' N').symm = MulEquiv.prodProdProdComm M M' N N'

source

def AddEquiv.prodCongr {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] {M' : Type u_6} {N' : Type u_7} [AddZeroClass N'] [AddZeroClass M'] (f : M ≃+ M') (g : N ≃+ N') :

M × N ≃+ M' × N'

Product of additive isomorphisms; the maps come from Equiv.prodCongr.

Equations

f.prodCongr g = { toEquiv := f.prodCongr g.toEquiv, map_add' := ⋯ }

Instances For

source

def MulEquiv.prodCongr {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] {M' : Type u_6} {N' : Type u_7} [MulOneClass N'] [MulOneClass M'] (f : M ≃* M') (g : N ≃* N') :

M × N ≃* M' × N'

Product of multiplicative isomorphisms; the maps come from Equiv.prodCongr.

Equations

f.prodCongr g = { toEquiv := f.prodCongr g.toEquiv, map_mul' := ⋯ }

Instances For

source

def AddEquiv.uniqueProd {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] [Unique N] :

N × M ≃+ M

Multiplying by the trivial monoid doesn't change the structure.

Equations

AddEquiv.uniqueProd = { toEquiv := Equiv.uniqueProd M N, map_add' := ⋯ }

Instances For

source

def MulEquiv.uniqueProd {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] [Unique N] :

N × M ≃* M

Multiplying by the trivial monoid doesn't change the structure.

Equations

MulEquiv.uniqueProd = { toEquiv := Equiv.uniqueProd M N, map_mul' := ⋯ }

Instances For

source

def AddEquiv.prodUnique {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] [Unique N] :

M × N ≃+ M

Multiplying by the trivial monoid doesn't change the structure.

Equations

AddEquiv.prodUnique = { toEquiv := Equiv.prodUnique M N, map_add' := ⋯ }

Instances For

source

def MulEquiv.prodUnique {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] [Unique N] :

M × N ≃* M

Multiplying by the trivial monoid doesn't change the structure.

Equations

MulEquiv.prodUnique = { toEquiv := Equiv.prodUnique M N, map_mul' := ⋯ }

Instances For

source

def AddEquiv.prodAddUnits {M : Type u_3} {N : Type u_4} [AddMonoid M] [AddMonoid N] :

AddUnits (M × N) ≃+ AddUnits M × AddUnits N

The additive monoid equivalence between additive units of a product of two additive monoids, and the product of the additive units of each additive monoid.

Equations