Group structures on the multiplicative and additive opposites #
Additive structures on αᵐᵒᵖ
#
Equations
- AddOpposite.natCast α = { natCast := fun n => { unop := ↑n } }
Equations
- MulOpposite.natCast α = { natCast := fun n => { unop := ↑n } }
Equations
- AddOpposite.intCast α = { intCast := fun n => { unop := ↑n } }
Equations
- MulOpposite.intCast α = { intCast := fun n => { unop := ↑n } }
Equations
- MulOpposite.addSemigroup α = Function.Injective.addSemigroup MulOpposite.unop (_ : Function.Injective MulOpposite.unop) (_ : ∀ (x x_1 : αᵐᵒᵖ), (x + x_1).unop = (x + x_1).unop)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- MulOpposite.addCommSemigroup α = Function.Injective.addCommSemigroup MulOpposite.unop (_ : Function.Injective MulOpposite.unop) (_ : ∀ (x x_1 : αᵐᵒᵖ), (x + x_1).unop = (x + x_1).unop)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- MulOpposite.addMonoidWithOne α = let src := MulOpposite.addMonoid α; let src_1 := MulOpposite.one α; let src_2 := MulOpposite.natCast α; AddMonoidWithOne.mk
Equations
- MulOpposite.addCommMonoidWithOne α = let src := MulOpposite.addMonoidWithOne α; let src_1 := MulOpposite.addCommMonoid α; AddCommMonoidWithOne.mk (_ : ∀ (a b : αᵐᵒᵖ), a + b = b + a)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- MulOpposite.addGroupWithOne α = let src := MulOpposite.addMonoidWithOne α; let src_1 := MulOpposite.addGroup α; AddGroupWithOne.mk SubNegMonoid.zsmul (_ : ∀ (a : αᵐᵒᵖ), -a + a = 0)
Equations
- MulOpposite.addCommGroupWithOne α = let src := MulOpposite.addGroupWithOne α; let src_1 := MulOpposite.addCommGroup α; AddCommGroupWithOne.mk
Multiplicative structures on αᵐᵒᵖ
#
We also generate additive structures on αᵃᵒᵖ
using to_additive
Equations
- AddOpposite.addSemigroup α = let src := AddOpposite.add α; AddSemigroup.mk (_ : ∀ (x y z : αᵃᵒᵖ), x + y + z = x + (y + z))
Equations
- MulOpposite.semigroup α = let src := MulOpposite.mul α; Semigroup.mk (_ : ∀ (x y z : αᵐᵒᵖ), x * y * z = x * (y * z))
Equations
- AddOpposite.addLeftCancelSemigroup α = let src := AddOpposite.addSemigroup α; AddLeftCancelSemigroup.mk (_ : ∀ (x x_1 x_2 : αᵃᵒᵖ), x + x_1 = x + x_2 → x_1 = x_2)
Equations
- MulOpposite.leftCancelSemigroup α = let src := MulOpposite.semigroup α; LeftCancelSemigroup.mk (_ : ∀ (x x_1 x_2 : αᵐᵒᵖ), x * x_1 = x * x_2 → x_1 = x_2)
Equations
- AddOpposite.addRightCancelSemigroup α = let src := AddOpposite.addSemigroup α; AddRightCancelSemigroup.mk (_ : ∀ (x x_1 x_2 : αᵃᵒᵖ), x + x_1 = x_2 + x_1 → x = x_2)
Equations
- MulOpposite.rightCancelSemigroup α = let src := MulOpposite.semigroup α; RightCancelSemigroup.mk (_ : ∀ (x x_1 x_2 : αᵐᵒᵖ), x * x_1 = x_2 * x_1 → x = x_2)
Equations
- AddOpposite.addCommSemigroup α = let src := AddOpposite.addSemigroup α; AddCommSemigroup.mk (_ : ∀ (x y : αᵃᵒᵖ), x + y = y + x)
Equations
- MulOpposite.commSemigroup α = let src := MulOpposite.semigroup α; CommSemigroup.mk (_ : ∀ (x y : αᵐᵒᵖ), x * y = y * x)
Equations
- AddOpposite.addZeroClass α = let src := AddOpposite.add α; let src_1 := AddOpposite.zero α; AddZeroClass.mk (_ : ∀ (x : αᵃᵒᵖ), 0 + x = x) (_ : ∀ (x : αᵃᵒᵖ), x + 0 = x)
Equations
- MulOpposite.mulOneClass α = let src := MulOpposite.mul α; let src_1 := MulOpposite.one α; MulOneClass.mk (_ : ∀ (x : αᵐᵒᵖ), 1 * x = x) (_ : ∀ (x : αᵐᵒᵖ), x * 1 = x)
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ∀ (n : ℕ) (x : αᵃᵒᵖ), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : αᵃᵒᵖ), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)
Equations
- (_ : ∀ (x : αᵃᵒᵖ), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : αᵃᵒᵖ), AddMonoid.nsmul 0 x = 0)
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ∀ (n : ℕ) (x : αᵃᵒᵖ), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : αᵃᵒᵖ), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)
Equations
- (_ : ∀ (x : αᵃᵒᵖ), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : αᵃᵒᵖ), AddMonoid.nsmul 0 x = 0)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- AddOpposite.addCancelMonoid α = let src := AddOpposite.addRightCancelMonoid α; let src_1 := AddOpposite.addLeftCancelMonoid α; AddCancelMonoid.mk (_ : ∀ (a b c : αᵃᵒᵖ), a + b = c + b → a = c)
Equations
- (_ : ∀ (x : αᵃᵒᵖ), AddRightCancelMonoid.nsmul 0 x = 0) = (_ : ∀ (x : αᵃᵒᵖ), AddRightCancelMonoid.nsmul 0 x = 0)
Equations
- One or more equations did not get rendered due to their size.
Equations
- MulOpposite.cancelMonoid α = let src := MulOpposite.rightCancelMonoid α; let src_1 := MulOpposite.leftCancelMonoid α; CancelMonoid.mk (_ : ∀ (a b c : αᵐᵒᵖ), a * b = c * b → a = c)
Equations
- (_ : ∀ (n : ℕ) (x : αᵃᵒᵖ), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : αᵃᵒᵖ), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)
Equations
- (_ : ∀ (x : αᵃᵒᵖ), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : αᵃᵒᵖ), AddMonoid.nsmul 0 x = 0)
Equations
- AddOpposite.addCommMonoid α = let src := AddOpposite.addMonoid α; let src_1 := AddOpposite.addCommSemigroup α; AddCommMonoid.mk (_ : ∀ (a b : αᵃᵒᵖ), a + b = b + a)
Equations
- MulOpposite.commMonoid α = let src := MulOpposite.monoid α; let src_1 := MulOpposite.commSemigroup α; CommMonoid.mk (_ : ∀ (a b : αᵐᵒᵖ), a * b = b * a)
Equations
- AddOpposite.addCancelCommMonoid α = let src := AddOpposite.addCancelMonoid α; let src_1 := AddOpposite.addCommMonoid α; AddCancelCommMonoid.mk (_ : ∀ (a b : αᵃᵒᵖ), a + b = b + a)
Equations
- MulOpposite.cancelCommMonoid α = let src := MulOpposite.cancelMonoid α; let src_1 := MulOpposite.commMonoid α; CancelCommMonoid.mk (_ : ∀ (a b : αᵐᵒᵖ), a * b = b * a)
Equations
- (_ : ∀ (n : ℕ) (x : αᵃᵒᵖ), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : αᵃᵒᵖ), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)
Equations
- AddOpposite.subNegMonoid α = let src := AddOpposite.addMonoid α; let src_1 := AddOpposite.neg α; SubNegMonoid.mk fun n x => { unop := n • x.unop }
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ∀ (x : αᵃᵒᵖ), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : αᵃᵒᵖ), AddMonoid.nsmul 0 x = 0)
Equations
- One or more equations did not get rendered due to their size.
Equations
- MulOpposite.divInvMonoid α = let src := MulOpposite.monoid α; let src_1 := MulOpposite.inv α; DivInvMonoid.mk fun n x => { unop := x.unop ^ n }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ∀ (a : αᵃᵒᵖ), SubNegMonoid.zsmul 0 a = 0) = (_ : ∀ (a : αᵃᵒᵖ), SubNegMonoid.zsmul 0 a = 0)
Equations
- One or more equations did not get rendered due to their size.
Equations
- AddOpposite.subtractionCommMonoid α = let src := AddOpposite.subtractionMonoid α; let src_1 := AddOpposite.addCommSemigroup α; SubtractionCommMonoid.mk (_ : ∀ (a b : αᵃᵒᵖ), a + b = b + a)
Equations
- MulOpposite.divisionCommMonoid α = let src := MulOpposite.divisionMonoid α; let src_1 := MulOpposite.commSemigroup α; DivisionCommMonoid.mk (_ : ∀ (a b : αᵐᵒᵖ), a * b = b * a)
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ∀ (a : αᵃᵒᵖ), SubNegMonoid.zsmul 0 a = 0) = (_ : ∀ (a : αᵃᵒᵖ), SubNegMonoid.zsmul 0 a = 0)
Equations
- One or more equations did not get rendered due to their size.
Equations
- AddOpposite.addGroup α = let src := AddOpposite.subNegMonoid α; AddGroup.mk (_ : ∀ (x : αᵃᵒᵖ), -x + x = 0)
Equations
- MulOpposite.group α = let src := MulOpposite.divInvMonoid α; Group.mk (_ : ∀ (x : αᵐᵒᵖ), x⁻¹ * x = 1)
Equations
- AddOpposite.addCommGroup α = let src := AddOpposite.addGroup α; let src_1 := AddOpposite.addCommMonoid α; AddCommGroup.mk (_ : ∀ (a b : αᵃᵒᵖ), a + b = b + a)
Equations
- MulOpposite.commGroup α = let src := MulOpposite.group α; let src_1 := MulOpposite.commMonoid α; CommGroup.mk (_ : ∀ (a b : αᵐᵒᵖ), a * b = b * a)
The function MulOpposite.op
is an additive equivalence.
Equations
- One or more equations did not get rendered due to their size.
Multiplicative structures on αᵃᵒᵖ
#
Equations
- AddOpposite.semigroup α = Function.Injective.semigroup AddOpposite.unop (_ : Function.Injective AddOpposite.unop) (_ : ∀ (x x_1 : αᵃᵒᵖ), (x * x_1).unop = (x * x_1).unop)
Equations
- AddOpposite.leftCancelSemigroup α = Function.Injective.leftCancelSemigroup AddOpposite.unop (_ : Function.Injective AddOpposite.unop) (_ : ∀ (x x_1 : αᵃᵒᵖ), (x * x_1).unop = (x * x_1).unop)
Equations
- AddOpposite.rightCancelSemigroup α = Function.Injective.rightCancelSemigroup AddOpposite.unop (_ : Function.Injective AddOpposite.unop) (_ : ∀ (x x_1 : αᵃᵒᵖ), (x * x_1).unop = (x * x_1).unop)
Equations
- AddOpposite.commSemigroup α = Function.Injective.commSemigroup AddOpposite.unop (_ : Function.Injective AddOpposite.unop) (_ : ∀ (x x_1 : αᵃᵒᵖ), (x * x_1).unop = (x * x_1).unop)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- AddOpposite.addCommGroupWithOne α = let src := AddOpposite.addCommMonoidWithOne α; let src_1 := AddOpposite.addCommGroup α; let src_2 := AddOpposite.intCast α; AddCommGroupWithOne.mk
The function AddOpposite.op
is a multiplicative equivalence.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Negation on an additive group is an AddEquiv
to the opposite group. When G
is commutative, there is AddEquiv.inv
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Inversion on a group is a MulEquiv
to the opposite group. When G
is commutative, there is
MulEquiv.inv
.
Equations
- One or more equations did not get rendered due to their size.
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ᵃᵒᵖ
.
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ᵃᵒᵖ
.
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
- One or more equations did not get rendered due to their size.
Equations
- (_ : { unop := ((AddOpposite.op ∘ ↑f) 0).unop } = { unop := 0.unop }) = (_ : { unop := ((AddOpposite.op ∘ ↑f) 0).unop } = { unop := 0.unop })
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
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
An additive semigroup homomorphism AddHom M N
can equivalently be viewed as an
additive semigroup homomorphism AddHom Mᵃᵒᵖ Nᵃᵒᵖ
. This is the action of the
(fully faithful)ᵃᵒᵖ
-functor on morphisms.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
A semigroup homomorphism M →ₙ* N
can equivalently be viewed as a semigroup homomorphism
Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ
. This is the action of the (fully faithful) ᵐᵒᵖ
-functor on morphisms.
Equations
- One or more equations did not get rendered due to their size.
An additive semigroup homomorphism AddHom M N
can equivalently be viewed as an additive
homomorphism AddHom Mᵐᵒᵖ Nᵐᵒᵖ
. This is the action of the (fully faithful) ᵐᵒᵖ
-functor on
morphisms.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : { unop := ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) 0).unop } = { unop := 0.unop }) = (_ : { unop := ((AddOpposite.op ∘ ↑f ∘ AddOpposite.unop) 0).unop } = { unop := 0.unop })
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
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
The 'unopposite' of an additive monoid homomorphism Mᵃᵒᵖ →+ Nᵃᵒᵖ
. Inverse to
AddMonoidHom.op
.
Equations
- AddMonoidHom.unop = Equiv.symm AddMonoidHom.op
The 'unopposite' of a monoid homomorphism Mᵐᵒᵖ →* Nᵐᵒᵖ
. Inverse to MonoidHom.op
.
Equations
- MonoidHom.unop = Equiv.symm MonoidHom.op
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
- One or more equations did not get rendered due to their size.
The 'unopposite' of an additive monoid hom αᵐᵒᵖ →+ βᵐᵒᵖ
. Inverse to
AddMonoidHom.mul_op
.
Equations
- AddMonoidHom.mulUnop = Equiv.symm AddMonoidHom.mulOp
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : (↑(AddEquiv.symm f) (↑f { unop := x })).unop = x) = (_ : (↑(AddEquiv.symm f) (↑f { unop := x })).unop = x)
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : (↑f (↑(AddEquiv.symm f) { unop := x })).unop = x) = (_ : (↑f (↑(AddEquiv.symm f) { unop := x })).unop = x)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
The 'unopposite' of an iso αᵃᵒᵖ ≃+ βᵃᵒᵖ
. Inverse to AddEquiv.op
.
Equations
- AddEquiv.unop = Equiv.symm AddEquiv.op
The 'unopposite' of an iso αᵐᵒᵖ ≃* βᵐᵒᵖ
. Inverse to MulEquiv.op
.
Equations
- MulEquiv.unop = Equiv.symm MulEquiv.op
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'
.