Ring structures on the multiplicative opposite

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

Equations

• MulOpposite.instDistrib = { toMul := MulOpposite.instMul, toAdd := MulOpposite.instAdd, left_distrib := ⋯, right_distrib := ⋯ }

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

Equations

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

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

Equations

• MulOpposite.instNonUnitalSemiring = { toNonUnitalNonAssocSemiring := MulOpposite.instNonUnitalNonAssocSemiring, mul_assoc := ⋯ }

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

Equations

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

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

Equations

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

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

Equations

• MulOpposite.instNonUnitalCommSemiring = { toNonUnitalSemiring := MulOpposite.instNonUnitalSemiring, mul_comm := ⋯ }

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

Equations

• MulOpposite.instCommSemiring = { toSemiring := MulOpposite.instSemiring, mul_comm := ⋯ }

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

Equations

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

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

Equations

• MulOpposite.instNonUnitalRing = { toNonUnitalNonAssocRing := MulOpposite.instNonUnitalNonAssocRing, mul_assoc := ⋯ }

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

Equations

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

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

Equations

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

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

Equations

• MulOpposite.instNonUnitalCommRing = { toNonUnitalRing := MulOpposite.instNonUnitalRing, mul_comm := ⋯ }

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

Equations

• MulOpposite.instCommRing = { toRing := MulOpposite.instRing, mul_comm := ⋯ }

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

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

Equations

• AddOpposite.instDistrib = { toMul := AddOpposite.instMul, toAdd := AddOpposite.instAdd, left_distrib := ⋯, right_distrib := ⋯ }

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

Equations

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

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

Equations

• AddOpposite.instNonUnitalSemiring = { toNonUnitalNonAssocSemiring := AddOpposite.instNonUnitalNonAssocSemiring, mul_assoc := ⋯ }

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

Equations

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

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

Equations

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

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

Equations

• AddOpposite.instNonUnitalCommSemiring = { toNonUnitalSemiring := AddOpposite.instNonUnitalSemiring, mul_comm := ⋯ }

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

Equations

• AddOpposite.instCommSemiring = { toSemiring := AddOpposite.instSemiring, mul_comm := ⋯ }

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

Equations

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

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

Equations

• AddOpposite.instNonUnitalRing = { toNonUnitalNonAssocRing := AddOpposite.instNonUnitalNonAssocRing, mul_assoc := ⋯ }

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

Equations

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

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

Equations

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

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

Equations

• AddOpposite.instNonUnitalCommRing = { toNonUnitalRing := AddOpposite.instNonUnitalRing, mul_comm := ⋯ }

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

Equations

• AddOpposite.instCommRing = { toRing := AddOpposite.instRing, mul_comm := ⋯ }

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

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 {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] : (R →ₙ+* S) ≃ (Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ)

A non-unital ring hom R →ₙ+* S can equivalently be viewed as a non-unital ring hom Rᵐᵒᵖ →+* Sᵐᵒᵖ. 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 {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ) (a✝ : R) : (op.symm f) a✝ = (↑(AddMonoidHom.mulUnop f.toAddMonoidHom)).toFun a✝

@[simp]

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

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

The 'unopposite' of a non-unital ring hom Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ. 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 {R : Type u_2} {S : Type u_3} [NonAssocSemiring R] [NonAssocSemiring S] : (R →+* S) ≃ (Rᵐᵒᵖ →+* Sᵐᵒᵖ)

A ring hom R →+* S can equivalently be viewed as a ring hom Rᵐᵒᵖ →+* Sᵐᵒᵖ. 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 {R : Type u_2} {S : Type u_3} [NonAssocSemiring R] [NonAssocSemiring S] (f : Rᵐᵒᵖ →+* Sᵐᵒᵖ) (a✝ : R) : (op.symm f) a✝ = MulOpposite.unop (f (MulOpposite.op a✝))

@[simp]

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

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

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

Equations

• RingHom.unop = RingHom.op.symm