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 MonoidHom
s:
fst M N : M × N →* M
,snd M N : M × N →* N
: projectionsProd.fst
andProd.snd
asMonoidHom
s;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
: sendsx
to(f x, g x)
;f.coprod g : M × N →* P
: sends(x, y)
tof x * g y
;f.prodMap g : M × N → M' × N'
:prod.map f g
as aMonoidHom
, sends(x, y)
to(f x, g y)
.
Main declarations #
mulMulHom
/mulMonoidHom
/mulMonoidWithZeroHom
: Multiplication bundled as a multiplicative/monoid/monoid with zero homomorphism.divMonoidHom
/divMonoidWithZeroHom
: Division bundled as a monoid/monoid with zero homomorphism.
Given additive monoids A
, B
, the natural projection homomorphism
from A × B
to A
Instances For
Given monoids M
, N
, the natural projection homomorphism from M × N
to M
.
Instances For
Given additive monoids A
, B
, the natural projection homomorphism
from A × B
to B
Instances For
Given monoids M
, N
, the natural projection homomorphism from M × N
to N
.
Instances For
Given additive monoids A
, B
, the natural inclusion homomorphism
from A
to A × B
.
Instances For
Given monoids M
, N
, the natural inclusion homomorphism from M
to M × N
.
Instances For
Given additive monoids A
, B
, the natural inclusion homomorphism
from B
to A × B
.
Instances For
Given monoids M
, N
, the natural inclusion homomorphism from N
to M × N
.
Instances For
Combine two AddMonoidHom
s f : M →+ N
, g : M →+ P
into
f.prod g : M →+ N × P
given by (f.prod g) x = (f x, g x)
Instances For
Combine two MonoidHom
s f : M →* N
, g : M →* P
into f.prod g : M →* N × P
given by (f.prod g) x = (f x, g x)
.
Instances For
prod.map
as an AddMonoidHom
.
Instances For
prod.map
as a MonoidHom
.
Instances For
Coproduct of two AddMonoidHom
s with the same codomain:
f.coprod g (p : M × N) = f p.1 + g p.2
.
Instances For
Coproduct of two MonoidHom
s with the same codomain:
f.coprod g (p : M × N) = f p.1 * g p.2
.
Instances For
The equivalence between M × N
and N × M
given by swapping the
components is additive.
Instances For
The equivalence between M × N
and N × M
given by swapping the components
is multiplicative.
Instances For
Four-way commutativity of prod
.
The name matches mul_mul_mul_comm
Instances For
Four-way commutativity of prod
. The name matches mul_mul_mul_comm
.
Instances For
Product of additive isomorphisms; the maps come from Equiv.prodCongr
.
Instances For
Product of multiplicative isomorphisms; the maps come from Equiv.prodCongr
.
Instances For
Multiplying by the trivial monoid doesn't change the structure.
Instances For
Multiplying by the trivial monoid doesn't change the structure.
Instances For
Multiplying by the trivial monoid doesn't change the structure.
Instances For
Multiplying by the trivial monoid doesn't change the structure.
Instances For
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.
Instances For
Multiplication and division as homomorphisms #
Addition as an additive monoid homomorphism.
Instances For
Multiplication as a monoid homomorphism.
Instances For
Multiplication as a multiplicative homomorphism with zero.
Instances For
Subtraction as an additive monoid homomorphism.
Instances For
Division as a monoid homomorphism.
Instances For
Division as a multiplicative homomorphism with zero.