Documentation

Mathlib.Algebra.Ring.Opposite

Ring structures on the multiplicative opposite #

instance MulOpposite.distrib (α : Type u) [inst : Distrib α] :
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
Equations
Equations
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.
instance MulOpposite.semiring (α : Type u) [inst : Semiring α] :
Equations
  • One or more equations did not get rendered due to their size.
Equations
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.
instance MulOpposite.ring (α : Type u) [inst : Ring α] :
Equations
instance MulOpposite.commRing (α : Type u) [inst : CommRing α] :
Equations
Equations
  • One or more equations did not get rendered due to their size.
instance AddOpposite.distrib (α : Type u) [inst : Distrib α] :
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
Equations
Equations
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.
instance AddOpposite.semiring (α : Type u) [inst : Semiring α] :
Equations
  • One or more equations did not get rendered due to their size.
Equations
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.
instance AddOpposite.ring (α : Type u) [inst : Ring α] :
Equations
instance AddOpposite.commRing (α : Type u) [inst : CommRing α] :
Equations
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem NonUnitalRingHom.toOpposite_apply {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :
↑(NonUnitalRingHom.toOpposite f hf) = MulOpposite.op f
def NonUnitalRingHom.toOpposite {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :

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
  • One or more equations did not get rendered due to their size.
@[simp]
theorem NonUnitalRingHom.fromOpposite_apply {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :
↑(NonUnitalRingHom.fromOpposite f hf) = f MulOpposite.unop
def NonUnitalRingHom.fromOpposite {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :

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
  • One or more equations did not get rendered due to their size.
@[simp]
theorem NonUnitalRingHom.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst : NonUnitalNonAssocSemiring β] (f : αᵐᵒᵖ →ₙ+* βᵐᵒᵖ) :
∀ (a : α), ↑(↑(Equiv.symm NonUnitalRingHom.op) f) a = ZeroHom.toFun (↑(AddMonoidHom.mulUnop (NonUnitalRingHom.toAddMonoidHom f))) a
@[simp]
theorem NonUnitalRingHom.op_apply_apply {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst : NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) :
∀ (a : αᵐᵒᵖ), ↑(NonUnitalRingHom.op f) a = ZeroHom.toFun (↑(AddMonoidHom.mulOp (NonUnitalRingHom.toAddMonoidHom f))) a

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.

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

Equations
@[simp]
theorem RingHom.toOpposite_apply {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] (f : R →+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :
↑(RingHom.toOpposite f hf) = MulOpposite.op f
def RingHom.toOpposite {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] (f : R →+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :

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
  • One or more equations did not get rendered due to their size.
@[simp]
theorem RingHom.fromOpposite_apply {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] (f : R →+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :
↑(RingHom.fromOpposite f hf) = f MulOpposite.unop
def RingHom.fromOpposite {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] (f : R →+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :

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
  • One or more equations did not get rendered due to their size.
@[simp]
theorem RingHom.op_apply_apply_unop {α : Type u_1} {β : Type u_2} [inst : NonAssocSemiring α] [inst : NonAssocSemiring β] (f : α →+* β) :
∀ (a : αᵐᵒᵖ), (↑(RingHom.op f) a).unop = f a.unop
@[simp]
theorem RingHom.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [inst : NonAssocSemiring α] [inst : NonAssocSemiring β] (f : αᵐᵒᵖ →+* βᵐᵒᵖ) :
∀ (a : α), ↑(↑(Equiv.symm RingHom.op) f) a = (f { unop := a }).unop
def RingHom.op {α : Type u_1} {β : Type u_2} [inst : NonAssocSemiring α] [inst : 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.
def RingHom.unop {α : Type u_1} {β : Type u_2} [inst : NonAssocSemiring α] [inst : NonAssocSemiring β] :

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

Equations