Documentation

Mathlib.Algebra.Ring.Opposite

Ring structures on the multiplicative opposite #

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

Distrib Rᵐᵒᵖ

Equations

instance MulOpposite.instNatCast {R : Type u_1} [NatCast R] :

NatCast Rᵐᵒᵖ

Equations

instance AddOpposite.instNatCast {R : Type u_1} [NatCast R] :

NatCast Rᵃᵒᵖ

Equations

instance MulOpposite.instIntCast {R : Type u_1} [IntCast R] :

IntCast Rᵐᵒᵖ

Equations

instance AddOpposite.instIntCast {R : Type u_1} [IntCast R] :

IntCast Rᵃᵒᵖ

Equations

@[simp]

theorem MulOpposite.op_natCast {R : Type u_1} [NatCast R] (n : ℕ) :

op ↑n = ↑n

@[simp]

theorem AddOpposite.op_natCast {R : Type u_1} [NatCast R] (n : ℕ) :

op ↑n = ↑n

@[simp]

theorem MulOpposite.op_ofNat {R : Type u_1} [NatCast R] (n : ℕ) [n.AtLeastTwo] :

op (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem AddOpposite.op_ofNat {R : Type u_1} [NatCast R] (n : ℕ) [n.AtLeastTwo] :

op (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem MulOpposite.op_intCast {R : Type u_1} [IntCast R] (n : ℤ) :

op ↑n = ↑n

@[simp]

theorem AddOpposite.op_intCast {R : Type u_1} [IntCast R] (n : ℤ) :

op ↑n = ↑n

@[simp]

theorem MulOpposite.unop_natCast {R : Type u_1} [NatCast R] (n : ℕ) :

unop ↑n = ↑n

@[simp]

theorem AddOpposite.unop_natCast {R : Type u_1} [NatCast R] (n : ℕ) :

unop ↑n = ↑n

@[simp]

theorem MulOpposite.unop_ofNat {R : Type u_1} [NatCast R] (n : ℕ) [n.AtLeastTwo] :

unop (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem AddOpposite.unop_ofNat {R : Type u_1} [NatCast R] (n : ℕ) [n.AtLeastTwo] :

unop (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem MulOpposite.unop_intCast {R : Type u_1} [IntCast R] (n : ℤ) :

unop ↑n = ↑n

@[simp]

theorem AddOpposite.unop_intCast {R : Type u_1} [IntCast R] (n : ℤ) :

unop ↑n = ↑n

instance MulOpposite.instAddMonoidWithOne {R : Type u_1} [AddMonoidWithOne R] :

AddMonoidWithOne Rᵐᵒᵖ

Equations

instance MulOpposite.instAddCommMonoidWithOne {R : Type u_1} [AddCommMonoidWithOne R] :

AddCommMonoidWithOne Rᵐᵒᵖ

Equations

instance MulOpposite.instAddGroupWithOne {R : Type u_1} [AddGroupWithOne R] :

AddGroupWithOne Rᵐᵒᵖ

Equations

instance MulOpposite.instAddCommGroupWithOne {R : Type u_1} [AddCommGroupWithOne R] :

AddCommGroupWithOne Rᵐᵒᵖ

Equations

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

NonUnitalNonAssocSemiring Rᵐᵒᵖ

Equations

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

NonUnitalSemiring Rᵐᵒᵖ

Equations

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

NonAssocSemiring Rᵐᵒᵖ

Equations

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

Semiring Rᵐᵒᵖ

Equations

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

NonUnitalCommSemiring Rᵐᵒᵖ

Equations

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

CommSemiring Rᵐᵒᵖ

Equations

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

NonUnitalNonAssocRing Rᵐᵒᵖ

Equations

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

NonUnitalRing Rᵐᵒᵖ

Equations

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

NonAssocRing Rᵐᵒᵖ

Equations

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

Ring Rᵐᵒᵖ

Equations

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

NonUnitalCommRing Rᵐᵒᵖ

Equations

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

CommRing Rᵐᵒᵖ

Equations

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

instance AddOpposite.instAddCommMonoidWithOne {R : Type u_1} [AddCommMonoidWithOne R] :

AddCommMonoidWithOne Rᵃᵒᵖ

Equations

instance AddOpposite.instAddCommGroupWithOne {R : Type u_1} [AddCommGroupWithOne R] :

AddCommGroupWithOne Rᵃᵒᵖ

Equations

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

NonUnitalNonAssocSemiring Rᵃᵒᵖ

Equations

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

NonUnitalSemiring Rᵃᵒᵖ

Equations

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

NonAssocSemiring Rᵃᵒᵖ

Equations

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

Semiring Rᵃᵒᵖ

Equations

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

NonUnitalCommSemiring Rᵃᵒᵖ

Equations

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

CommSemiring Rᵃᵒᵖ

Equations

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

NonUnitalNonAssocRing Rᵃᵒᵖ

Equations

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

NonUnitalRing Rᵃᵒᵖ

Equations

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

NonAssocRing Rᵃᵒᵖ

Equations

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

Ring Rᵃᵒᵖ

Equations

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

NonUnitalCommRing Rᵃᵒᵖ

Equations

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

CommRing Rᵃᵒᵖ

Equations

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

Instances For

@[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

Instances For

@[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

Instances For

@[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✝

@[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✝

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

Instances For

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

Instances For

@[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

Instances For

@[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

Instances For

@[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✝))

@[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✝))

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

Instances For