Group isomorphism between a group and its opposite #
Inversion on a group is a MulEquiv
to the opposite group. When G
is commutative, there is
MulEquiv.inv
.
Equations
Instances For
Negation on an additive group is an AddEquiv
to the opposite group. When G
is commutative, there is AddEquiv.inv
.
Equations
Instances For
An additive semigroup homomorphism f : AddHom M N
such that f x
additively
commutes with f y
for all x, y
defines an additive semigroup homomorphism to Sᵃᵒᵖ
.
Equations
Instances For
An additive semigroup homomorphism f : AddHom M N
such that f x
additively
commutes with f y
for all x
, y
defines an additive semigroup homomorphism from Mᵃᵒᵖ
.
Equations
Instances For
A monoid homomorphism f : M →* N
such that f x
commutes with f y
for all x, y
defines
a monoid homomorphism to Nᵐᵒᵖ
.
Equations
Instances For
An additive monoid homomorphism f : M →+ N
such that f x
additively commutes
with f y
for all x, y
defines an additive monoid homomorphism to Sᵃᵒᵖ
.
Equations
Instances For
A monoid homomorphism f : M →* N
such that f x
commutes with f y
for all x, y
defines
a monoid homomorphism from Mᵐᵒᵖ
.
Equations
Instances For
An additive monoid homomorphism f : M →+ N
such that f x
additively commutes
with f y
for all x
, y
defines an additive monoid homomorphism from Mᵃᵒᵖ
.
Equations
Instances For
A monoid homomorphism M →* N
can equivalently be viewed as a monoid homomorphism
Mᵐᵒᵖ →* Nᵐᵒᵖ
. This is the action of the (fully faithful) ᵐᵒᵖ
-functor on morphisms.
Equations
Instances For
An additive monoid homomorphism M →+ N
can equivalently be viewed as an additive monoid
homomorphism Mᵃᵒᵖ →+ Nᵃᵒᵖ
. This is the action of the (fully faithful)
ᵃᵒᵖ
-functor on morphisms.
Equations
Instances For
The 'unopposite' of a monoid homomorphism Mᵐᵒᵖ →* Nᵐᵒᵖ
. Inverse to MonoidHom.op
.
Equations
Instances For
The 'unopposite' of an additive monoid homomorphism Mᵃᵒᵖ →+ Nᵃᵒᵖ
. Inverse to AddMonoidHom.op
.
Equations
Instances For
An additive homomorphism M →+ N
can equivalently be viewed as an additive homomorphism
Mᵐᵒᵖ →+ Nᵐᵒᵖ
. This is the action of the (fully faithful) ᵐᵒᵖ
-functor on morphisms.
Equations
Instances For
The 'unopposite' of an additive monoid hom αᵐᵒᵖ →+ βᵐᵒᵖ
. Inverse to
AddMonoidHom.mul_op
.
Equations
Instances For
This ext lemma changes equalities on αᵐᵒᵖ →+ β
to equalities on α →+ β
.
This is useful because there are often ext lemmas for specific α
s that will apply
to an equality of α →+ β
such as Finsupp.addHom_ext'
.