mathlib3 documentation

algebra.category.Ring.basic

Category instances for semiring, ring, comm_semiring, and comm_ring. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We introduce the bundled categories:

source
def SemiRing  :
Type (u+1)

The category of semirings.

Equations
Instances for SemiRing
source
@[reducible]
def SemiRing.assoc_ring_hom (M : Type u_1) (N : Type u_2) [semiring M] [semiring N] :
Type (max u_1 u_2)

ring_hom doesn't actually assume associativity. This alias is needed to make the category theory machinery work. We use the same trick in category_theory.Mon.assoc_monoid_hom.

source
@[protected, instance]
def SemiRing.bundled_hom  :
category_theory.bundled_hom SemiRing.assoc_ring_hom
Equations
source
@[protected, instance]
def SemiRing.large_category  :
category_theory.large_category SemiRing
source
@[protected, instance]
def SemiRing.concrete_category  :
category_theory.concrete_category SemiRing
source
@[protected, instance]
def SemiRing.has_coe_to_sort  :
has_coe_to_sort SemiRing (Type u_1)
Equations
source
def SemiRing.of (R : Type u) [semiring R] :
SemiRing

Construct a bundled SemiRing from the underlying type and typeclass.

Equations
source
def SemiRing.of_hom {R S : Type u} [semiring R] [semiring S] (f : R →+* S) :
SemiRing.of R ⟶ SemiRing.of S

Typecheck a ring_hom as a morphism in SemiRing.

Equations
source
@[simp]
theorem SemiRing.of_hom_apply {R S : Type u} [semiring R] [semiring S] (f : R →+* S) (x : R) :
⇑(SemiRing.of_hom f) x = ⇑f x
source
@[protected, instance]
def SemiRing.inhabited  :
inhabited SemiRing
Equations
source
@[protected, instance]
def SemiRing.semiring (R : SemiRing) :
semiring ↥R
Equations
source
@[simp]
theorem SemiRing.coe_of (R : Type u) [semiring R] :
↥(SemiRing.of R) = R
source
@[protected, instance]
def SemiRing.has_forget_to_Mon  :
category_theory.has_forget₂ SemiRing Mon
Equations
source
@[protected, instance]
def SemiRing.has_forget_to_AddCommMon  :
category_theory.has_forget₂ SemiRing AddCommMon
Equations
source
def Ring  :
Type (u+1)

The category of rings.

Equations
Instances for Ring
source
@[protected, instance]
def Ring.ring.to_semiring.category_theory.bundled_hom.parent_projection  :
category_theory.bundled_hom.parent_projection ring.to_semiring
Equations
source
@[protected, instance]
def Ring.concrete_category  :
category_theory.concrete_category Ring
source
@[protected, instance]
def Ring.large_category  :
category_theory.large_category Ring
source
@[protected, instance]
def Ring.has_coe_to_sort  :
has_coe_to_sort Ring (Type u_1)
source
def Ring.of (R : Type u) [ring R] :
Ring

Construct a bundled Ring from the underlying type and typeclass.

Equations
source
def Ring.of_hom {R S : Type u} [ring R] [ring S] (f : R →+* S) :
Ring.of R ⟶ Ring.of S

Typecheck a ring_hom as a morphism in Ring.

Equations
source
@[simp]
theorem Ring.of_hom_apply {R S : Type u} [ring R] [ring S] (f : R →+* S) (x : R) :
⇑(Ring.of_hom f) x = ⇑f x
source
@[protected, instance]
def Ring.inhabited  :
inhabited Ring
Equations
source
@[protected, instance]
def Ring.ring (R : Ring) :
ring ↥R
Equations
source
@[simp]
theorem Ring.coe_of (R : Type u) [ring R] :
↥(Ring.of R) = R
source
@[protected, instance]
def Ring.has_forget_to_SemiRing  :
category_theory.has_forget₂ Ring SemiRing
Equations
source
@[protected, instance]
def Ring.has_forget_to_AddCommGroup  :
category_theory.has_forget₂ Ring AddCommGroup
Equations
source
def CommSemiRing  :
Type (u+1)

The category of commutative semirings.

Equations
Instances for CommSemiRing
source
@[protected, instance]
def CommSemiRing.comm_semiring.to_semiring.category_theory.bundled_hom.parent_projection  :
category_theory.bundled_hom.parent_projection comm_semiring.to_semiring
Equations
source
@[protected, instance]
def CommSemiRing.concrete_category  :
category_theory.concrete_category CommSemiRing
source
@[protected, instance]
def CommSemiRing.large_category  :
category_theory.large_category CommSemiRing
source
@[protected, instance]
def CommSemiRing.has_coe_to_sort  :
has_coe_to_sort CommSemiRing (Type u_1)
Equations
source
def CommSemiRing.of (R : Type u) [comm_semiring R] :
CommSemiRing

Construct a bundled CommSemiRing from the underlying type and typeclass.

Equations
source
def CommSemiRing.of_hom {R S : Type u} [comm_semiring R] [comm_semiring S] (f : R →+* S) :
CommSemiRing.of R ⟶ CommSemiRing.of S

Typecheck a ring_hom as a morphism in CommSemiRing.

Equations
source
@[simp]
theorem CommSemiRing.of_hom_apply {R S : Type u} [comm_semiring R] [comm_semiring S] (f : R →+* S) (x : R) :
⇑(CommSemiRing.of_hom f) x = ⇑f x
source
@[protected, instance]
def CommSemiRing.inhabited  :
inhabited CommSemiRing
Equations
source
@[protected, instance]
def CommSemiRing.comm_semiring (R : CommSemiRing) :
comm_semiring ↥R
Equations
source
@[simp]
theorem CommSemiRing.coe_of (R : Type u) [comm_semiring R] :
↥(CommSemiRing.of R) = R
source
@[protected, instance]
def CommSemiRing.has_forget_to_SemiRing  :
category_theory.has_forget₂ CommSemiRing SemiRing
Equations
source
@[protected, instance]
def CommSemiRing.has_forget_to_CommMon  :
category_theory.has_forget₂ CommSemiRing CommMon

The forgetful functor from commutative rings to (multiplicative) commutative monoids.

Equations
source
def CommRing  :
Type (u+1)

The category of commutative rings.

Equations
Instances for CommRing
source
@[protected, instance]
def CommRing.comm_ring.to_ring.category_theory.bundled_hom.parent_projection  :
category_theory.bundled_hom.parent_projection comm_ring.to_ring
Equations
source
@[protected, instance]
def CommRing.large_category  :
category_theory.large_category CommRing
source
@[protected, instance]
def CommRing.concrete_category  :
category_theory.concrete_category CommRing
source
@[protected, instance]
def CommRing.has_coe_to_sort  :
has_coe_to_sort CommRing (Type u_1)
Equations
source
def CommRing.of (R : Type u) [comm_ring R] :
CommRing

Construct a bundled CommRing from the underlying type and typeclass.

Equations
source
def CommRing.of_hom {R S : Type u} [comm_ring R] [comm_ring S] (f : R →+* S) :
CommRing.of R ⟶ CommRing.of S

Typecheck a ring_hom as a morphism in CommRing.

Equations
source
@[simp]
theorem CommRing.of_hom_apply {R S : Type u} [comm_ring R] [comm_ring S] (f : R →+* S) (x : R) :
⇑(CommRing.of_hom f) x = ⇑f x
source
@[protected, instance]
def CommRing.inhabited  :
inhabited CommRing
Equations
source
@[protected, instance]
def CommRing.comm_ring (R : CommRing) :
comm_ring ↥R
Equations
source
@[simp]
theorem CommRing.coe_of (R : Type u) [comm_ring R] :
↥(CommRing.of R) = R
source
@[protected, instance]
def CommRing.has_forget_to_Ring  :
category_theory.has_forget₂ CommRing Ring
Equations
source
@[protected, instance]
def CommRing.has_forget_to_CommSemiRing  :
category_theory.has_forget₂ CommRing CommSemiRing

The forgetful functor from commutative rings to (multiplicative) commutative monoids.

Equations
source
@[protected, instance]
def CommRing.category_theory.forget₂.category_theory.full  :
category_theory.full (category_theory.forget₂ CommRing CommSemiRing)
Equations
source
def ring_equiv.to_Ring_iso {X Y : Type u} [ring X] [ring Y] (e : X ≃+* Y) :
Ring.of X ≅ Ring.of Y

Build an isomorphism in the category Ring from a ring_equiv between rings.

Equations
source
@[simp]
theorem ring_equiv.to_Ring_iso_inv {X Y : Type u} [ring X] [ring Y] (e : X ≃+* Y) :
e.to_Ring_iso.inv = e.symm.to_ring_hom
source
@[simp]
theorem ring_equiv.to_Ring_iso_hom {X Y : Type u} [ring X] [ring Y] (e : X ≃+* Y) :
e.to_Ring_iso.hom = e.to_ring_hom
source
@[simp]
theorem ring_equiv.to_CommRing_iso_hom {X Y : Type u} [comm_ring X] [comm_ring Y] (e : X ≃+* Y) :
e.to_CommRing_iso.hom = e.to_ring_hom
source
def ring_equiv.to_CommRing_iso {X Y : Type u} [comm_ring X] [comm_ring Y] (e : X ≃+* Y) :
CommRing.of X ≅ CommRing.of Y

Build an isomorphism in the category CommRing from a ring_equiv between comm_rings.

Equations
source
@[simp]
theorem ring_equiv.to_CommRing_iso_inv {X Y : Type u} [comm_ring X] [comm_ring Y] (e : X ≃+* Y) :
e.to_CommRing_iso.inv = e.symm.to_ring_hom
source
def category_theory.iso.Ring_iso_to_ring_equiv {X Y : Ring} (i : X ≅ Y) :
↥X ≃+* ↥Y

Build a ring_equiv from an isomorphism in the category Ring.

Equations
source
def category_theory.iso.CommRing_iso_to_ring_equiv {X Y : CommRing} (i : X ≅ Y) :
↥X ≃+* ↥Y

Build a ring_equiv from an isomorphism in the category CommRing.

Equations
source
@[simp]
theorem category_theory.iso.CommRing_iso_to_ring_equiv_to_ring_hom {X Y : CommRing} (i : X ≅ Y) :
i.CommRing_iso_to_ring_equiv.to_ring_hom = i.hom
source
@[simp]
theorem category_theory.iso.CommRing_iso_to_ring_equiv_symm_to_ring_hom {X Y : CommRing} (i : X ≅ Y) :
i.CommRing_iso_to_ring_equiv.symm.to_ring_hom = i.inv
source
def ring_equiv_iso_Ring_iso {X Y : Type u} [ring X] [ring Y] :
X ≃+* Y ≅ Ring.of X ≅ Ring.of Y

Ring equivalences between rings are the same as (isomorphic to) isomorphisms in Ring.

Equations
source
def ring_equiv_iso_CommRing_iso {X Y : Type u} [comm_ring X] [comm_ring Y] :
X ≃+* Y ≅ CommRing.of X ≅ CommRing.of Y

Ring equivalences between comm_rings are the same as (isomorphic to) isomorphisms in CommRing.

Equations
source
@[protected, instance]
def Ring.forget_reflects_isos  :
category_theory.reflects_isomorphisms (category_theory.forget Ring)
source
@[protected, instance]
def CommRing.forget_reflects_isos  :
category_theory.reflects_isomorphisms (category_theory.forget CommRing)
source
theorem CommRing.comp_eq_ring_hom_comp {R S T : CommRing} (f : R ⟶ S) (g : S ⟶ T) :
f ≫ g = ring_hom.comp g f
source
theorem CommRing.ring_hom_comp_eq_comp {R S T : Type u_1} [comm_ring R] [comm_ring S] [comm_ring T] (f : R →+* S) (g : S →+* T) :
g.comp f = CommRing.of_hom f ≫ CommRing.of_hom g