Category instances for Semiring
, Ring
, CommSemiring
, and CommRing
. #
We introduce the bundled categories:
SemiRingCat
RingCat
CommSemiRingCat
CommRingCat
along with the relevant forgetful functors between them.
The category of semirings.
Equations
Instances For
An alias for Semiring.{max u v}
, to deal around unification issues.
Equations
Instances For
RingHom
doesn't actually assume associativity. This alias is needed to make the category
theory machinery work. We use the same trick in MonCat.AssocMonoidHom
.
Equations
- SemiRingCat.AssocRingHom M N = (M →+* N)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- R.forget_obj_eq_coe = ((CategoryTheory.forget SemiRingCat).obj R = ↑R)
Instances For
Equations
- X.instSemiring = X.str
Equations
- SemiRingCat.instFunLike = CategoryTheory.ConcreteCategory.instFunLike
Equations
- ⋯ = ⋯
Construct a bundled SemiRing from the underlying type and typeclass.
Equations
Instances For
Equations
- SemiRingCat.instInhabited = { default := SemiRingCat.of PUnit.{?u.3 + 1} }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Typecheck a RingHom
as a morphism in SemiRingCat
.
Equations
- SemiRingCat.ofHom f = f
Instances For
Equations
Equations
- R.forget_obj_eq_coe = ((CategoryTheory.forget RingCat).obj R = ↑R)
Instances For
Equations
- ⋯ = ⋯
Typecheck a RingHom
as a morphism in RingCat
.
Equations
- RingCat.ofHom f = f
Instances For
Equations
- RingCat.instInhabited = { default := RingCat.of PUnit.{?u.3 + 1} }
Equations
- One or more equations did not get rendered due to their size.
The category of commutative semirings.
Instances For
Equations
- CommSemiRingCat.instConcreteCategory = id inferInstance
Equations
- CommSemiRingCat.instCoeSortType = { coe := fun (X : CommSemiRingCat) => ↑X }
Equations
- X.instCommSemiringα = X.str
Equations
- R.forget_obj_eq_coe = ((CategoryTheory.forget CommSemiRingCat).obj R = ↑R)
Instances For
Equations
- X.instCommSemiring = X.str
Equations
- X.instCommSemiring' = X.str
Equations
- CommSemiRingCat.instFunLike = CategoryTheory.ConcreteCategory.instFunLike
Equations
- ⋯ = ⋯
Typecheck a RingHom
as a morphism in CommSemiRingCat
.
Equations
Instances For
Equations
- CommSemiRingCat.instInhabited = { default := CommSemiRingCat.of PUnit.{?u.3 + 1} }
Equations
- R.instCommSemiringα_1 = R.str
The forgetful functor from commutative rings to (multiplicative) commutative monoids.
Equations
- One or more equations did not get rendered due to their size.
Ring equivalence are isomorphisms in category of commutative semirings
Equations
- e.toCommSemiRingCatIso = { hom := e.toRingHom, inv := e.symm.toRingHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Equations
The category of commutative rings.
Equations
Instances For
Equations
- CommRingCat.instConcreteCategory = id inferInstance
Equations
- CommRingCat.instCoeSortType = { coe := fun (X : CommRingCat) => ↑X }
Equations
- R.forget_obj_eq_coe = ((CategoryTheory.forget CommRingCat).obj R = ↑R)
Instances For
Equations
- X.instCommRing = X.str
Equations
- X.instCommRing' = X.str
Equations
- CommRingCat.instFunLike = CategoryTheory.ConcreteCategory.instFunLike
Equations
- ⋯ = ⋯
Specialization of ConcreteCategory.id_apply
because simp
can't see through the defeq.
Equations
- CommRingCat.instFunLike' = CategoryTheory.ConcreteCategory.instFunLike
Equations
- CommRingCat.instFunLike'' = CategoryTheory.ConcreteCategory.instFunLike
Equations
- CommRingCat.instFunLike''' = CategoryTheory.ConcreteCategory.instFunLike
Typecheck a RingHom
as a morphism in CommRingCat
.
Equations
- CommRingCat.ofHom f = f
Instances For
Equations
- CommRingCat.instInhabited = { default := CommRingCat.of PUnit.{?u.3 + 1} }
Equations
- R.instCommRingα = R.str
The forgetful functor from commutative rings to (multiplicative) commutative monoids.
Equations
- One or more equations did not get rendered due to their size.
Build an isomorphism in the category RingCat
from a RingEquiv
between RingCat
s.
Equations
- e.toRingCatIso = { hom := e.toRingHom, inv := e.symm.toRingHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Build an isomorphism in the category CommRingCat
from a RingEquiv
between CommRingCat
s.
Equations
- e.toCommRingCatIso = { hom := e.toRingHom, inv := e.symm.toRingHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Build a RingEquiv
from an isomorphism in the category RingCat
.
Equations
- i.ringCatIsoToRingEquiv = RingEquiv.ofHomInv i.hom i.inv ⋯ ⋯
Instances For
Build a RingEquiv
from an isomorphism in the category CommRingCat
.
Equations
- i.commRingCatIsoToRingEquiv = RingEquiv.ofHomInv i.hom i.inv ⋯ ⋯
Instances For
Ring equivalences between RingCat
s are the same as (isomorphic to) isomorphisms in
RingCat
.
Equations
- ringEquivIsoRingIso = { hom := fun (e : X ≃+* Y) => e.toRingCatIso, inv := fun (i : RingCat.of X ≅ RingCat.of Y) => i.ringCatIsoToRingEquiv, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Ring equivalences between CommRingCat
s are the same as (isomorphic to) isomorphisms
in CommRingCat
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
@[simp]
lemmas for RingHom.comp
and categorical identities.