Category instances for semiring, ring, comm_semiring, and comm_ring.
We introduce the bundled categories:
SemiRingRingCommSemiRingCommRingalong with the relevant forgetful functors between them.
@[instance]
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}
Construct a bundled SemiRing from the underlying type and typeclass.
Equations
@[instance]
Equations
@[instance]
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
@[instance]
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}
@[instance]
Equations
@[instance]
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}
The category of commutative semirings.
Equations
Construct a bundled CommSemiRing from the underlying type and typeclass.
Equations
@[instance]
@[instance]
Equations
- R.comm_semiring = R.str
@[instance]
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
Construct a bundled CommRing from the underlying type and typeclass.
Equations
@[instance]
Equations
@[instance]
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
@[instance]
Equations
- CommRing.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.full._proof_1}
@[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
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]
def
ring_equiv.to_CommRing_iso
{X Y : Type u}
[comm_ring X]
[comm_ring Y] :
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]
Build a ring_equiv from an isomorphism in the category CommRing.
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' := _}
@[instance]
Equations
- Ring.forget_reflects_isos = {reflects := λ (X Y : Ring) (f : X ⟶ Y) (_x : category_theory.is_iso ((category_theory.forget Ring).map f)), let i : (category_theory.forget Ring).obj X ≅ (category_theory.forget Ring).obj Y := category_theory.as_iso ((category_theory.forget Ring).map f), e : ↥X ≃+* ↥Y := {to_fun := f.to_fun, inv_fun := i.to_equiv.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _} in {inv := e.to_Ring_iso.inv, hom_inv_id' := _, inv_hom_id' := _}}
@[instance]
Equations
- CommRing.forget_reflects_isos = {reflects := λ (X Y : CommRing) (f : X ⟶ Y) (_x : category_theory.is_iso ((category_theory.forget CommRing).map f)), let i : (category_theory.forget CommRing).obj X ≅ (category_theory.forget CommRing).obj Y := category_theory.as_iso ((category_theory.forget CommRing).map f), e : ↥X ≃+* ↥Y := {to_fun := f.to_fun, inv_fun := i.to_equiv.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _} in {inv := e.to_CommRing_iso.inv, hom_inv_id' := _, inv_hom_id' := _}}