Documentation

Mathlib.Algebra.Category.Ring.Constructions

Constructions of (co)limits in CommRingCat #

In this file we provide the explicit (co)cones for various (co)limits in CommRingCat, including

The explicit cocone with tensor products as the fibered product in CommRingCat.

Instances For
    @[simp]
    theorem CommRingCat.pushoutCocone_inl {R : CommRingCat} {A : CommRingCat} {B : CommRingCat} (f : R A) (g : R B) :
    CategoryTheory.Limits.PushoutCocone.inl (CommRingCat.pushoutCocone f g) = Algebra.TensorProduct.includeLeftRingHom
    @[simp]
    theorem CommRingCat.pushoutCocone_inr {R : CommRingCat} {A : CommRingCat} {B : CommRingCat} (f : R A) (g : R B) :
    CategoryTheory.Limits.PushoutCocone.inr (CommRingCat.pushoutCocone f g) = Algebra.TensorProduct.includeRight
    @[simp]
    theorem CommRingCat.pushoutCocone_pt {R : CommRingCat} {A : CommRingCat} {B : CommRingCat} (f : R A) (g : R B) :

    Verify that the pushout_cocone is indeed the colimit.

    Instances For

      The trivial ring is the (strict) terminal object of CommRingCat.

      Instances For

        The product in CommRingCat is the cartesian product. This is the binary fan.

        Instances For

          The product in CommRingCat is the cartesian product.

          Instances For

            The equalizer in CommRingCat is the equalizer as sets. This is the equalizer fork.

            Instances For

              The equalizer in CommRingCat is the equalizer as sets.

              Instances For

                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.

                Instances For

                  The constructed pullback cone is indeed the limit.

                  Instances For