Ring structures on the multiplicative opposite

instance MulOpposite.instDistrib {α : Type u_1} [Distrib α] : Distrib αᵐᵒᵖ

Equations

• MulOpposite.instDistrib = Distrib.mk ⋯ ⋯

instance MulOpposite.instNonUnitalNonAssocSemiring {α : Type u_1} [NonUnitalNonAssocSemiring α] : NonUnitalNonAssocSemiring αᵐᵒᵖ

Equations

• MulOpposite.instNonUnitalNonAssocSemiring = NonUnitalNonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

instance MulOpposite.instNonUnitalSemiring {α : Type u_1} [NonUnitalSemiring α] : NonUnitalSemiring αᵐᵒᵖ

Equations

• MulOpposite.instNonUnitalSemiring = NonUnitalSemiring.mk ⋯

instance MulOpposite.instNonAssocSemiring {α : Type u_1} [NonAssocSemiring α] : NonAssocSemiring αᵐᵒᵖ

Equations

• MulOpposite.instNonAssocSemiring = NonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

instance MulOpposite.instSemiring {α : Type u_1} [Semiring α] : Semiring αᵐᵒᵖ

Equations

• MulOpposite.instSemiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯

instance MulOpposite.instNonUnitalCommSemiring {α : Type u_1} [NonUnitalCommSemiring α] : NonUnitalCommSemiring αᵐᵒᵖ

Equations

• MulOpposite.instNonUnitalCommSemiring = NonUnitalCommSemiring.mk ⋯

instance MulOpposite.instCommSemiring {α : Type u_1} [CommSemiring α] : CommSemiring αᵐᵒᵖ

Equations

• MulOpposite.instCommSemiring = CommSemiring.mk ⋯

instance MulOpposite.instNonUnitalNonAssocRing {α : Type u_1} [NonUnitalNonAssocRing α] : NonUnitalNonAssocRing αᵐᵒᵖ

Equations

• MulOpposite.instNonUnitalNonAssocRing = NonUnitalNonAssocRing.mk ⋯ ⋯ ⋯ ⋯

instance MulOpposite.instNonUnitalRing {α : Type u_1} [NonUnitalRing α] : NonUnitalRing αᵐᵒᵖ

Equations

• MulOpposite.instNonUnitalRing = NonUnitalRing.mk ⋯

instance MulOpposite.instNonAssocRing {α : Type u_1} [NonAssocRing α] : NonAssocRing αᵐᵒᵖ

Equations

• MulOpposite.instNonAssocRing = NonAssocRing.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance MulOpposite.instRing {α : Type u_1} [Ring α] : Ring αᵐᵒᵖ

Equations

• MulOpposite.instRing = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance MulOpposite.instNonUnitalCommRing {α : Type u_1} [NonUnitalCommRing α] : NonUnitalCommRing αᵐᵒᵖ

Equations

• MulOpposite.instNonUnitalCommRing = NonUnitalCommRing.mk ⋯

instance MulOpposite.instCommRing {α : Type u_1} [CommRing α] : CommRing αᵐᵒᵖ

Equations

• MulOpposite.instCommRing = CommRing.mk ⋯

instance MulOpposite.instIsDomain {α : Type u_1} [Ring α] [IsDomain α] : IsDomain αᵐᵒᵖ

instance AddOpposite.instDistrib {α : Type u_1} [Distrib α] : Distrib αᵃᵒᵖ

Equations

• AddOpposite.instDistrib = Distrib.mk ⋯ ⋯

instance AddOpposite.instNonUnitalNonAssocSemiring {α : Type u_1} [NonUnitalNonAssocSemiring α] : NonUnitalNonAssocSemiring αᵃᵒᵖ

Equations

• AddOpposite.instNonUnitalNonAssocSemiring = NonUnitalNonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

instance AddOpposite.instNonUnitalSemiring {α : Type u_1} [NonUnitalSemiring α] : NonUnitalSemiring αᵃᵒᵖ

Equations

• AddOpposite.instNonUnitalSemiring = NonUnitalSemiring.mk ⋯

instance AddOpposite.instNonAssocSemiring {α : Type u_1} [NonAssocSemiring α] : NonAssocSemiring αᵃᵒᵖ

Equations

• AddOpposite.instNonAssocSemiring = NonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

instance AddOpposite.instSemiring {α : Type u_1} [Semiring α] : Semiring αᵃᵒᵖ

Equations

• AddOpposite.instSemiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯

instance AddOpposite.instNonUnitalCommSemiring {α : Type u_1} [NonUnitalCommSemiring α] : NonUnitalCommSemiring αᵃᵒᵖ

Equations

• AddOpposite.instNonUnitalCommSemiring = NonUnitalCommSemiring.mk ⋯

instance AddOpposite.instCommSemiring {α : Type u_1} [CommSemiring α] : CommSemiring αᵃᵒᵖ

Equations

• AddOpposite.instCommSemiring = CommSemiring.mk ⋯

instance AddOpposite.instNonUnitalNonAssocRing {α : Type u_1} [NonUnitalNonAssocRing α] : NonUnitalNonAssocRing αᵃᵒᵖ

Equations

• AddOpposite.instNonUnitalNonAssocRing = NonUnitalNonAssocRing.mk ⋯ ⋯ ⋯ ⋯

instance AddOpposite.instNonUnitalRing {α : Type u_1} [NonUnitalRing α] : NonUnitalRing αᵃᵒᵖ

Equations

• AddOpposite.instNonUnitalRing = NonUnitalRing.mk ⋯

instance AddOpposite.instNonAssocRing {α : Type u_1} [NonAssocRing α] : NonAssocRing αᵃᵒᵖ

Equations

• AddOpposite.instNonAssocRing = NonAssocRing.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance AddOpposite.instRing {α : Type u_1} [Ring α] : Ring αᵃᵒᵖ

Equations

• AddOpposite.instRing = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance AddOpposite.instNonUnitalCommRing {α : Type u_1} [NonUnitalCommRing α] : NonUnitalCommRing αᵃᵒᵖ

Equations

• AddOpposite.instNonUnitalCommRing = NonUnitalCommRing.mk ⋯

instance AddOpposite.instCommRing {α : Type u_1} [CommRing α] : CommRing αᵃᵒᵖ

Equations

• AddOpposite.instCommRing = CommRing.mk ⋯

instance AddOpposite.instIsDomain {α : Type u_1} [Ring α] [IsDomain α] : IsDomain αᵃᵒᵖ

def NonUnitalRingHom.toOpposite {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) : R →ₙ+* Sᵐᵒᵖ

A non-unital ring homomorphism f : R →ₙ+* S such that f x commutes with f y for all x, y defines a non-unital ring homomorphism to Sᵐᵒᵖ.

Equations

• f.toOpposite hf = { toFun := MulOpposite.op ∘ ⇑f, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem NonUnitalRingHom.toOpposite_apply {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) : ⇑(f.toOpposite hf) = MulOpposite.op ∘ ⇑f

def NonUnitalRingHom.fromOpposite {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) : Rᵐᵒᵖ →ₙ+* S

A non-unital ring homomorphism f : R →ₙ* S such that f x commutes with f y for all x, y defines a non-unital ring homomorphism from Rᵐᵒᵖ.

Equations

• f.fromOpposite hf = { toFun := ⇑f ∘ MulOpposite.unop, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem NonUnitalRingHom.fromOpposite_apply {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) : ⇑(f.fromOpposite hf) = ⇑f ∘ MulOpposite.unop

def NonUnitalRingHom.op {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] : (α →ₙ+* β) ≃ (αᵐᵒᵖ →ₙ+* βᵐᵒᵖ)

A non-unital ring hom α →ₙ+* β can equivalently be viewed as a non-unital ring hom αᵐᵒᵖ →+* βᵐᵒᵖ. This is the action of the (fully faithful) ᵐᵒᵖ-functor on morphisms.

Equations

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

@[simp]

theorem NonUnitalRingHom.op_symm_apply_apply {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : αᵐᵒᵖ →ₙ+* βᵐᵒᵖ) (a✝ : α) : (op.symm f) a✝ = (↑(AddMonoidHom.mulUnop f.toAddMonoidHom)).toFun a✝

@[simp]

theorem NonUnitalRingHom.op_apply_apply {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) (a✝ : αᵐᵒᵖ) : (op f) a✝ = (↑(AddMonoidHom.mulOp f.toAddMonoidHom)).toFun a✝

def NonUnitalRingHom.unop {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] : (αᵐᵒᵖ →ₙ+* βᵐᵒᵖ) ≃ (α →ₙ+* β)

The 'unopposite' of a non-unital ring hom αᵐᵒᵖ →ₙ+* βᵐᵒᵖ. Inverse to NonUnitalRingHom.op.

Equations

• NonUnitalRingHom.unop = NonUnitalRingHom.op.symm

def RingHom.toOpposite {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) : R →+* Sᵐᵒᵖ

A ring homomorphism f : R →+* S such that f x commutes with f y for all x, y defines a ring homomorphism to Sᵐᵒᵖ.

Equations

• f.toOpposite hf = { toFun := MulOpposite.op ∘ ⇑f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem RingHom.toOpposite_apply {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) : ⇑(f.toOpposite hf) = MulOpposite.op ∘ ⇑f

def RingHom.fromOpposite {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) : Rᵐᵒᵖ →+* S

A ring homomorphism f : R →+* S such that f x commutes with f y for all x, y defines a ring homomorphism from Rᵐᵒᵖ.

Equations

• f.fromOpposite hf = { toFun := ⇑f ∘ MulOpposite.unop, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem RingHom.fromOpposite_apply {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) : ⇑(f.fromOpposite hf) = ⇑f ∘ MulOpposite.unop

def RingHom.op {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [NonAssocSemiring β] : (α →+* β) ≃ (αᵐᵒᵖ →+* βᵐᵒᵖ)

A ring hom α →+* β can equivalently be viewed as a ring hom αᵐᵒᵖ →+* βᵐᵒᵖ. This is the action of the (fully faithful) ᵐᵒᵖ-functor on morphisms.

Equations

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

@[simp]

theorem RingHom.op_symm_apply_apply {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [NonAssocSemiring β] (f : αᵐᵒᵖ →+* βᵐᵒᵖ) (a✝ : α) : (op.symm f) a✝ = MulOpposite.unop (f (MulOpposite.op a✝))

@[simp]

theorem RingHom.op_apply_apply {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [NonAssocSemiring β] (f : α →+* β) (a✝ : αᵐᵒᵖ) : (op f) a✝ = MulOpposite.op (f (MulOpposite.unop a✝))

def RingHom.unop {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [NonAssocSemiring β] : (αᵐᵒᵖ →+* βᵐᵒᵖ) ≃ (α →+* β)

The 'unopposite' of a ring hom αᵐᵒᵖ →+* βᵐᵒᵖ. Inverse to RingHom.op.

Equations

• RingHom.unop = RingHom.op.symm