mathlib documentation

algebra.category.CommRing.basic

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

We introduce the bundled categories:

SemiRing
Ring
CommSemiRing
CommRing along with the relevant forgetful functors between them.

def SemiRing :

Type (u+1)

The category of semirings.

Equations

SemiRing = category_theory.bundled semiring

@[protected, instance]

def SemiRing.bundled_hom :

category_theory.bundled_hom ring_hom

Equations

SemiRing.bundled_hom = {to_fun := ring_hom.to_fun, id := ring_hom.id, comp := ring_hom.comp, hom_ext := ring_hom.coe_inj, id_to_fun := SemiRing.bundled_hom._proof_1, comp_to_fun := SemiRing.bundled_hom._proof_2}

@[protected, instance]

def SemiRing.large_category :

category_theory.large_category SemiRing

@[protected, instance]

def SemiRing.concrete_category :

category_theory.concrete_category SemiRing

@[protected, instance]

def SemiRing.has_coe_to_sort :

has_coe_to_sort SemiRing

def SemiRing.of (R : Type u) [semiring R] :

Construct a bundled SemiRing from the underlying type and typeclass.

Equations

SemiRing.of R = category_theory.bundled.of R

@[protected, instance]

def SemiRing.inhabited :

inhabited SemiRing

Equations

SemiRing.inhabited = {default := SemiRing.of punit ring.to_semiring}

@[protected, instance]

def SemiRing.semiring (R : SemiRing) :

Equations

R.semiring = R.str

@[simp]

theorem SemiRing.coe_of (R : Type u) [semiring R] :

↥(SemiRing.of R) = R

@[protected, instance]

def SemiRing.has_forget_to_Mon :

category_theory.has_forget₂ SemiRing Mon

Equations

SemiRing.has_forget_to_Mon = category_theory.bundled_hom.mk_has_forget₂ (λ (R : Type u_1) (hR : semiring R), monoid_with_zero.to_monoid R) (λ (R₁ R₂ : category_theory.bundled semiring), ring_hom.to_monoid_hom) SemiRing.has_forget_to_Mon._proof_1

@[protected, instance]

def SemiRing.has_forget_to_AddCommMon :

category_theory.has_forget₂ SemiRing AddCommMon

Equations

SemiRing.has_forget_to_AddCommMon = {forget₂ := {obj := λ (R : SemiRing), AddCommMon.of ↥R, map := λ (R₁ R₂ : SemiRing) (f : R₁ ⟶ R₂), ring_hom.to_add_monoid_hom f, map_id' := SemiRing.has_forget_to_AddCommMon._proof_1, map_comp' := SemiRing.has_forget_to_AddCommMon._proof_2}, forget_comp := SemiRing.has_forget_to_AddCommMon._proof_3}

def Ring :

Type (u+1)

The category of rings.

Equations

Ring = category_theory.bundled ring

@[protected, instance]

def Ring.ring.to_semiring.category_theory.bundled_hom.parent_projection :

category_theory.bundled_hom.parent_projection ring.to_semiring

Equations

Ring.ring.to_semiring.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk

@[protected, instance]

def Ring.concrete_category :

category_theory.concrete_category Ring

@[protected, instance]

def Ring.large_category :

category_theory.large_category Ring

@[protected, instance]

def Ring.has_coe_to_sort :

has_coe_to_sort Ring

def Ring.of (R : Type u) [ring R] :

Construct a bundled Ring from the underlying type and typeclass.

Equations

Ring.of R = category_theory.bundled.of R

@[protected, instance]

def Ring.inhabited :

Equations

Ring.inhabited = {default := Ring.of punit (comm_ring.to_ring punit)}

@[protected, instance]

def Ring.ring (R : Ring) :

Equations

R.ring = R.str

@[simp]

theorem Ring.coe_of (R : Type u) [ring R] :

↥(Ring.of R) = R

@[protected, instance]

def Ring.has_forget_to_SemiRing :

category_theory.has_forget₂ Ring SemiRing

Equations

Ring.has_forget_to_SemiRing = category_theory.bundled_hom.forget₂ ring_hom ring.to_semiring

@[protected, instance]

def Ring.has_forget_to_AddCommGroup :

category_theory.has_forget₂ Ring AddCommGroup

Equations

Ring.has_forget_to_AddCommGroup = {forget₂ := {obj := λ (R : Ring), AddCommGroup.of ↥R, map := λ (R₁ R₂ : Ring) (f : R₁ ⟶ R₂), ring_hom.to_add_monoid_hom f, map_id' := Ring.has_forget_to_AddCommGroup._proof_1, map_comp' := Ring.has_forget_to_AddCommGroup._proof_2}, forget_comp := Ring.has_forget_to_AddCommGroup._proof_3}

def CommSemiRing :

Type (u+1)

The category of commutative semirings.

Equations

CommSemiRing = category_theory.bundled comm_semiring

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

CommSemiRing.comm_semiring.to_semiring.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk

@[protected, instance]

def CommSemiRing.concrete_category :

category_theory.concrete_category CommSemiRing

@[protected, instance]

def CommSemiRing.has_coe_to_sort :

has_coe_to_sort CommSemiRing

@[protected, instance]

def CommSemiRing.large_category :

category_theory.large_category CommSemiRing

def CommSemiRing.of (R : Type u) [comm_semiring R] :

Construct a bundled CommSemiRing from the underlying type and typeclass.

Equations

CommSemiRing.of R = category_theory.bundled.of R

@[protected, instance]

def CommSemiRing.inhabited :

inhabited CommSemiRing

Equations

CommSemiRing.inhabited = {default := CommSemiRing.of punit comm_ring.to_comm_semiring}

@[protected, instance]

def CommSemiRing.comm_semiring (R : CommSemiRing) :

comm_semiring ↥R

Equations

R.comm_semiring = R.str

@[simp]

theorem CommSemiRing.coe_of (R : Type u) [comm_semiring R] :

↥(CommSemiRing.of R) = R

@[protected, instance]

def CommSemiRing.has_forget_to_SemiRing :

category_theory.has_forget₂ CommSemiRing SemiRing

Equations

CommSemiRing.has_forget_to_SemiRing = category_theory.bundled_hom.forget₂ ring_hom comm_semiring.to_semiring

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

CommSemiRing.has_forget_to_CommMon = category_theory.has_forget₂.mk' (λ (R : CommSemiRing), CommMon.of ↥R) CommSemiRing.has_forget_to_CommMon._proof_1 (λ (R₁ R₂ : CommSemiRing) (f : R₁ ⟶ R₂), ring_hom.to_monoid_hom f) CommSemiRing.has_forget_to_CommMon._proof_2

def CommRing :

Type (u+1)

The category of commutative rings.

Equations

CommRing = category_theory.bundled comm_ring

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

CommRing.comm_ring.to_ring.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk

@[protected, instance]

def CommRing.large_category :

category_theory.large_category CommRing

@[protected, instance]

def CommRing.has_coe_to_sort :

has_coe_to_sort CommRing

@[protected, instance]

def CommRing.concrete_category :

category_theory.concrete_category CommRing

def CommRing.of (R : Type u) [comm_ring R] :

Construct a bundled CommRing from the underlying type and typeclass.

Equations

CommRing.of R = category_theory.bundled.of R

@[protected, instance]

def CommRing.inhabited :

inhabited CommRing

Equations

CommRing.inhabited = {default := CommRing.of punit punit.comm_ring}

@[protected, instance]

def CommRing.comm_ring (R : CommRing) :

Equations

R.comm_ring = R.str

@[simp]

theorem CommRing.coe_of (R : Type u) [comm_ring R] :

↥(CommRing.of R) = R

@[protected, instance]

def CommRing.has_forget_to_Ring :

category_theory.has_forget₂ CommRing Ring

Equations

CommRing.has_forget_to_Ring = category_theory.bundled_hom.forget₂ (category_theory.bundled_hom.map_hom ring_hom ring.to_semiring) comm_ring.to_ring

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

CommRing.has_forget_to_CommSemiRing = category_theory.has_forget₂.mk' (λ (R : CommRing), CommSemiRing.of ↥R) CommRing.has_forget_to_CommSemiRing._proof_1 (λ (R₁ R₂ : CommRing) (f : R₁ ⟶ R₂), f) CommRing.has_forget_to_CommSemiRing._proof_2

@[protected, instance]

def CommRing.category_theory.forget₂.category_theory.full :

category_theory.full (category_theory.forget₂ CommRing CommSemiRing)

Equations

CommRing.category_theory.forget₂.category_theory.full = {preimage := λ (X Y : CommRing) (f : (category_theory.forget₂ CommRing CommSemiRing).obj X ⟶ (category_theory.forget₂ CommRing CommSemiRing).obj Y), f, witness' := CommRing.category_theory.forget₂.category_theory.full._proof_1}

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

e.to_Ring_iso = {hom := e.to_ring_hom, inv := e.symm.to_ring_hom, hom_inv_id' := _, inv_hom_id' := _}

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

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

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

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

e.to_CommRing_iso = {hom := e.to_ring_hom, inv := e.symm.to_ring_hom, hom_inv_id' := _, inv_hom_id' := _}

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

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

i.Ring_iso_to_ring_equiv = {to_fun := ⇑(i.hom), inv_fun := ⇑(i.inv), left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

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

i.CommRing_iso_to_ring_equiv = {to_fun := ⇑(i.hom), inv_fun := ⇑(i.inv), left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

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

ring_equiv_iso_Ring_iso = {hom := λ (e : X ≃+* Y), e.to_Ring_iso, inv := λ (i : Ring.of X ≅ Ring.of Y), i.Ring_iso_to_ring_equiv, hom_inv_id' := _, inv_hom_id' := _}

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

ring_equiv_iso_CommRing_iso = {hom := λ (e : X ≃+* Y), e.to_CommRing_iso, inv := λ (i : CommRing.of X ≅ CommRing.of Y), i.CommRing_iso_to_ring_equiv, hom_inv_id' := _, inv_hom_id' := _}

@[protected, instance]

def Ring.forget_reflects_isos :

category_theory.reflects_isomorphisms (category_theory.forget Ring)

@[protected, instance]

def CommRing.forget_reflects_isos :

category_theory.reflects_isomorphisms (category_theory.forget CommRing)