Constructions of (co)limits in CommRingCat
#
In this file we provide the explicit (co)cones for various (co)limits in CommRingCat
, including
- tensor product is the pushout
- tensor product over
Z
is the binary coproduct Z
is the initial object0
is the strict terminal object- cartesian product is the product
- arbitrary direct product of a family of rings is the product object (Pi object)
RingHom.eqLocus
is the equalizer
The explicit cocone with tensor products as the fibered product in CommRingCat
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The tensor product A ⊗[ℤ] B
forms a cocone for A
and B
.
Equations
Instances For
The tensor product A ⊗[ℤ] B
is a coproduct for A
and B
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The limit cone of the tensor product A ⊗[ℤ] B
in CommRingCat
.
Equations
Instances For
Equations
- X.instUniqueHomOfPUnit = { default := CommRingCat.ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ }, uniq := ⋯ }
ℤ
is the initial object of CommRingCat
.
Instances For
The product in CommRingCat
is the cartesian product.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The categorical product of rings is the cartesian product of rings. This is its Fan
.
Equations
- CommRingCat.piFan R = CategoryTheory.Limits.Fan.mk (CommRingCat.of ((i : ι) → ↑(R i))) fun (i : ι) => CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) => ↑(R i)) i)
Instances For
The categorical product of rings is the cartesian product of rings.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The categorical product and the usual product agrees
Equations
Instances For
The categorical product and the usual product agrees
Equations
Instances For
The equalizer in CommRingCat
is the equalizer as sets. This is the equalizer fork.
Equations
Instances For
The equalizer in CommRingCat
is the equalizer as sets.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alias of CommRingCat.equalizer_ι_isLocalHom
.
In the category of CommRingCat
, the pullback of f : A ⟶ C
and g : B ⟶ C
is the eqLocus
of the two maps A × B ⟶ C
. This is the constructed pullback cone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The constructed pullback cone is indeed the limit.
Equations
- One or more equations did not get rendered due to their size.