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

noncomputable def CommRingCat.pushoutCocone {R : CommRingCat} {A : CommRingCat} {B : CommRingCat} (f : R A) (g : R B) :

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
    @[simp]
    theorem CommRingCat.pushoutCocone_inl {R : CommRingCat} {A : CommRingCat} {B : CommRingCat} (f : R A) (g : R B) :
    (CommRingCat.pushoutCocone f g).inl = Algebra.TensorProduct.includeLeftRingHom
    @[simp]
    theorem CommRingCat.pushoutCocone_inr {R : CommRingCat} {A : CommRingCat} {B : CommRingCat} (f : R A) (g : R B) :
    (CommRingCat.pushoutCocone f g).inr = Algebra.TensorProduct.includeRight.toRingHom
    @[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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

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

      Equations
      Instances For
        @[simp]
        theorem CommRingCat.prodFan_pt (A : CommRingCat) (B : CommRingCat) :
        (A.prodFan B).pt = CommRingCat.of (A × B)

        The product in CommRingCat is the cartesian product.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          noncomputable def CommRingCat.piFan {ι : Type u} (R : ιCommRingCat) :

          The categorical product of rings is the cartesian product of rings. This is its Fan.

          Equations
          Instances For
            @[simp]
            theorem CommRingCat.piFan_pt {ι : Type u} (R : ιCommRingCat) :
            (CommRingCat.piFan R).pt = CommRingCat.of ((i : ι) → (R i))

            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
              noncomputable def CommRingCat.piIsoPi {ι : Type u} (R : ιCommRingCat) :
              R CommRingCat.of ((i : ι) → (R i))

              The categorical product and the usual product agrees

              Equations
              Instances For
                noncomputable def RingEquiv.piEquivPi {ι : Type u} (R : ιType u) [(i : ι) → CommRing (R i)] :
                ( fun (i : ι) => CommRingCat.of (R i)) ≃+* ((i : ι) → R i)

                The categorical product and the usual product agrees

                Equations
                Instances For
                  noncomputable def CommRingCat.equalizerFork {A : CommRingCat} {B : CommRingCat} (f : A B) (g : A B) :

                  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
                      noncomputable def CommRingCat.pullbackCone {A : CommRingCat} {B : CommRingCat} {C : CommRingCat} (f : A C) (g : B C) :

                      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.
                        Instances For