Ring structures on the multiplicative opposite

instance MulOpposite.distrib (α : Type u) [Distrib α] : Distrib αᵐᵒᵖ

Equations

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

instance MulOpposite.mulZeroClass (α : Type u) [MulZeroClass α] : MulZeroClass αᵐᵒᵖ

Equations

• MulOpposite.mulZeroClass α = MulZeroClass.mk (_ : ∀ (x : αᵐᵒᵖ), 0 * x = 0) (_ : ∀ (x : αᵐᵒᵖ), x * 0 = 0)

instance MulOpposite.mulZeroOneClass (α : Type u) [MulZeroOneClass α] : MulZeroOneClass αᵐᵒᵖ

Equations

• MulOpposite.mulZeroOneClass α = let src := MulOpposite.mulZeroClass α; let src_1 := MulOpposite.mulOneClass α; MulZeroOneClass.mk (_ : ∀ (a : αᵐᵒᵖ), 0 * a = 0) (_ : ∀ (a : αᵐᵒᵖ), a * 0 = 0)

instance MulOpposite.semigroupWithZero (α : Type u) [SemigroupWithZero α] : SemigroupWithZero αᵐᵒᵖ

Equations

• MulOpposite.semigroupWithZero α = let src := MulOpposite.semigroup α; let src_1 := MulOpposite.mulZeroClass α; SemigroupWithZero.mk (_ : ∀ (a : αᵐᵒᵖ), 0 * a = 0) (_ : ∀ (a : αᵐᵒᵖ), a * 0 = 0)

instance MulOpposite.monoidWithZero (α : Type u) [MonoidWithZero α] : MonoidWithZero αᵐᵒᵖ

Equations

• MulOpposite.monoidWithZero α = let src := MulOpposite.monoid α; let src_1 := MulOpposite.mulZeroOneClass α; MonoidWithZero.mk (_ : ∀ (a : αᵐᵒᵖ), 0 * a = 0) (_ : ∀ (a : αᵐᵒᵖ), a * 0 = 0)

instance MulOpposite.nonUnitalNonAssocSemiring (α : Type u) [NonUnitalNonAssocSemiring α] : NonUnitalNonAssocSemiring αᵐᵒᵖ

Equations

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

instance MulOpposite.nonUnitalSemiring (α : Type u) [NonUnitalSemiring α] : NonUnitalSemiring αᵐᵒᵖ

Equations

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

instance MulOpposite.nonAssocSemiring (α : Type u) [NonAssocSemiring α] : NonAssocSemiring αᵐᵒᵖ

Equations

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

instance MulOpposite.semiring (α : Type u) [Semiring α] : Semiring αᵐᵒᵖ

Equations

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

instance MulOpposite.nonUnitalCommSemiring (α : Type u) [NonUnitalCommSemiring α] : NonUnitalCommSemiring αᵐᵒᵖ

Equations

• MulOpposite.nonUnitalCommSemiring α = let src := MulOpposite.nonUnitalSemiring α; let src_1 := MulOpposite.commSemigroup α; NonUnitalCommSemiring.mk (_ : ∀ (a b : αᵐᵒᵖ), a * b = b * a)

instance MulOpposite.commSemiring (α : Type u) [CommSemiring α] : CommSemiring αᵐᵒᵖ

Equations

• MulOpposite.commSemiring α = let src := MulOpposite.semiring α; let src_1 := MulOpposite.commSemigroup α; CommSemiring.mk (_ : ∀ (a b : αᵐᵒᵖ), a * b = b * a)

instance MulOpposite.nonUnitalNonAssocRing (α : Type u) [NonUnitalNonAssocRing α] : NonUnitalNonAssocRing αᵐᵒᵖ

Equations

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

instance MulOpposite.nonUnitalRing (α : Type u) [NonUnitalRing α] : NonUnitalRing αᵐᵒᵖ

Equations

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

instance MulOpposite.nonAssocRing (α : Type u) [NonAssocRing α] : NonAssocRing αᵐᵒᵖ

Equations

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

instance MulOpposite.ring (α : Type u) [Ring α] : Ring αᵐᵒᵖ

Equations

• MulOpposite.ring α = let src := MulOpposite.monoid α; let src_1 := MulOpposite.nonAssocRing α; Ring.mk SubNegMonoid.zsmul (_ : ∀ (a : αᵐᵒᵖ), -a + a = 0)

instance MulOpposite.nonUnitalCommRing (α : Type u) [NonUnitalCommRing α] : NonUnitalCommRing αᵐᵒᵖ

Equations

• MulOpposite.nonUnitalCommRing α = let src := MulOpposite.nonUnitalRing α; let src_1 := MulOpposite.nonUnitalCommSemiring α; NonUnitalCommRing.mk (_ : ∀ (a b : αᵐᵒᵖ), a * b = b * a)

instance MulOpposite.commRing (α : Type u) [CommRing α] : CommRing αᵐᵒᵖ

Equations

• MulOpposite.commRing α = let src := MulOpposite.ring α; let src_1 := MulOpposite.commSemiring α; CommRing.mk (_ : ∀ (a b : αᵐᵒᵖ), a * b = b * a)

instance MulOpposite.noZeroDivisors (α : Type u) [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors αᵐᵒᵖ

Equations

• MulOpposite.noZeroDivisors = MulOpposite.noZeroDivisors.proof_1

instance MulOpposite.isDomain (α : Type u) [Ring α] [IsDomain α] : IsDomain αᵐᵒᵖ

Equations

• MulOpposite.isDomain = MulOpposite.isDomain.proof_1

instance MulOpposite.groupWithZero (α : Type u) [GroupWithZero α] : GroupWithZero αᵐᵒᵖ

Equations

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

instance AddOpposite.distrib (α : Type u) [Distrib α] : Distrib αᵃᵒᵖ

Equations

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

instance AddOpposite.mulZeroClass (α : Type u) [MulZeroClass α] : MulZeroClass αᵃᵒᵖ

Equations

• AddOpposite.mulZeroClass α = MulZeroClass.mk (_ : ∀ (x : αᵃᵒᵖ), 0 * x = 0) (_ : ∀ (x : αᵃᵒᵖ), x * 0 = 0)

instance AddOpposite.mulZeroOneClass (α : Type u) [MulZeroOneClass α] : MulZeroOneClass αᵃᵒᵖ

Equations

• AddOpposite.mulZeroOneClass α = let src := AddOpposite.mulZeroClass α; let src_1 := AddOpposite.mulOneClass α; MulZeroOneClass.mk (_ : ∀ (a : αᵃᵒᵖ), 0 * a = 0) (_ : ∀ (a : αᵃᵒᵖ), a * 0 = 0)

instance AddOpposite.semigroupWithZero (α : Type u) [SemigroupWithZero α] : SemigroupWithZero αᵃᵒᵖ

Equations

• AddOpposite.semigroupWithZero α = let src := AddOpposite.semigroup α; let src_1 := AddOpposite.mulZeroClass α; SemigroupWithZero.mk (_ : ∀ (a : αᵃᵒᵖ), 0 * a = 0) (_ : ∀ (a : αᵃᵒᵖ), a * 0 = 0)

instance AddOpposite.monoidWithZero (α : Type u) [MonoidWithZero α] : MonoidWithZero αᵃᵒᵖ

Equations

• AddOpposite.monoidWithZero α = let src := AddOpposite.monoid α; let src_1 := AddOpposite.mulZeroOneClass α; MonoidWithZero.mk (_ : ∀ (a : αᵃᵒᵖ), 0 * a = 0) (_ : ∀ (a : αᵃᵒᵖ), a * 0 = 0)

instance AddOpposite.nonUnitalNonAssocSemiring (α : Type u) [NonUnitalNonAssocSemiring α] : NonUnitalNonAssocSemiring αᵃᵒᵖ

Equations

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

instance AddOpposite.nonUnitalSemiring (α : Type u) [NonUnitalSemiring α] : NonUnitalSemiring αᵃᵒᵖ

Equations

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

instance AddOpposite.nonAssocSemiring (α : Type u) [NonAssocSemiring α] : NonAssocSemiring αᵃᵒᵖ

Equations

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

instance AddOpposite.semiring (α : Type u) [Semiring α] : Semiring αᵃᵒᵖ

Equations

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

instance AddOpposite.nonUnitalCommSemiring (α : Type u) [NonUnitalCommSemiring α] : NonUnitalCommSemiring αᵃᵒᵖ

Equations

• AddOpposite.nonUnitalCommSemiring α = let src := AddOpposite.nonUnitalSemiring α; let src_1 := AddOpposite.commSemigroup α; NonUnitalCommSemiring.mk (_ : ∀ (a b : αᵃᵒᵖ), a * b = b * a)

instance AddOpposite.commSemiring (α : Type u) [CommSemiring α] : CommSemiring αᵃᵒᵖ

Equations

• AddOpposite.commSemiring α = let src := AddOpposite.semiring α; let src_1 := AddOpposite.commSemigroup α; CommSemiring.mk (_ : ∀ (a b : αᵃᵒᵖ), a * b = b * a)

instance AddOpposite.nonUnitalNonAssocRing (α : Type u) [NonUnitalNonAssocRing α] : NonUnitalNonAssocRing αᵃᵒᵖ

Equations

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

instance AddOpposite.nonUnitalRing (α : Type u) [NonUnitalRing α] : NonUnitalRing αᵃᵒᵖ

Equations

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

instance AddOpposite.nonAssocRing (α : Type u) [NonAssocRing α] : NonAssocRing αᵃᵒᵖ

Equations

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

instance AddOpposite.ring (α : Type u) [Ring α] : Ring αᵃᵒᵖ

Equations

• AddOpposite.ring α = let src := AddOpposite.nonAssocRing α; let src_1 := AddOpposite.semiring α; Ring.mk SubNegMonoid.zsmul (_ : ∀ (a : αᵃᵒᵖ), -a + a = 0)

instance AddOpposite.nonUnitalCommRing (α : Type u) [NonUnitalCommRing α] : NonUnitalCommRing αᵃᵒᵖ

Equations

• AddOpposite.nonUnitalCommRing α = let src := AddOpposite.nonUnitalRing α; let src_1 := AddOpposite.nonUnitalCommSemiring α; NonUnitalCommRing.mk (_ : ∀ (a b : αᵃᵒᵖ), a * b = b * a)

instance AddOpposite.commRing (α : Type u) [CommRing α] : CommRing αᵃᵒᵖ

Equations

• AddOpposite.commRing α = let src := AddOpposite.ring α; let src_1 := AddOpposite.commSemiring α; CommRing.mk (_ : ∀ (a b : αᵃᵒᵖ), a * b = b * a)

instance AddOpposite.noZeroDivisors (α : Type u) [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors αᵃᵒᵖ

Equations

• AddOpposite.noZeroDivisors = AddOpposite.noZeroDivisors.proof_1

instance AddOpposite.isDomain (α : Type u) [Ring α] [IsDomain α] : IsDomain αᵃᵒᵖ

Equations

• AddOpposite.isDomain = AddOpposite.isDomain.proof_1

instance AddOpposite.groupWithZero (α : Type u) [GroupWithZero α] : GroupWithZero αᵃᵒᵖ

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} [NonUnitalNonAssocSemiring R] [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} [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

• 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} [NonUnitalNonAssocSemiring R] [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} [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

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

@[simp]

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

@[simp]

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

def NonUnitalRingHom.op {α : Type u_1} {β : Type u_2} [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.

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

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

Equations

• NonUnitalRingHom.unop = NonUnitalRingHom.op.symm

@[simp]

theorem RingHom.toOpposite_apply {R : Type u_1} {S : Type u_2} [Semiring R] [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} [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

• 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} [Semiring R] [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} [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

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

@[simp]

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

@[simp]

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

def RingHom.op {α : Type u_1} {β : Type u_2} [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.

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

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

Equations

• RingHom.unop = RingHom.op.symm