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

source
def CommRingCat.pushoutCocone {R : CommRingCat} {A : CommRingCat} {B : CommRingCat} (f : R ⟶ A) (g : R ⟶ B) :
CategoryTheory.Limits.PushoutCocone f g

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

Instances For
    source
    @[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
    source
    @[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
    source
    @[simp]
    theorem CommRingCat.pushoutCocone_pt {R : CommRingCat} {A : CommRingCat} {B : CommRingCat} (f : R ⟶ A) (g : R ⟶ B) :
    (CommRingCat.pushoutCocone f g).pt = CommRingCat.of (TensorProduct ↑R ↑A ↑B)
    source
    def CommRingCat.pushoutCoconeIsColimit {R : CommRingCat} {A : CommRingCat} {B : CommRingCat} (f : R ⟶ A) (g : R ⟶ B) :
    CategoryTheory.Limits.IsColimit (CommRingCat.pushoutCocone f g)

    Verify that the pushout_cocone is indeed the colimit.

    Instances For
      source
      def CommRingCat.punitIsTerminal :
      CategoryTheory.Limits.IsTerminal (CommRingCat.of PUnit.{u + 1} )

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

      Instances For
        source
        instance CommRingCat.commRingCat_hasStrictTerminalObjects :
        CategoryTheory.Limits.HasStrictTerminalObjects CommRingCat
        source
        theorem CommRingCat.subsingleton_of_isTerminal {X : CommRingCat} (hX : CategoryTheory.Limits.IsTerminal X) :
        Subsingleton ↑X
        source
        def CommRingCat.zIsInitial :
        CategoryTheory.Limits.IsInitial (CommRingCat.of ℤ)

        ℤ is the initial object of CommRingCat.

        Instances For
          source
          @[simp]
          theorem CommRingCat.prodFan_pt (A : CommRingCat) (B : CommRingCat) :
          (CommRingCat.prodFan A B).pt = CommRingCat.of (↑A × ↑B)
          source
          def CommRingCat.prodFan (A : CommRingCat) (B : CommRingCat) :
          CategoryTheory.Limits.BinaryFan A B

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

          Instances For
            source
            def CommRingCat.prodFanIsLimit (A : CommRingCat) (B : CommRingCat) :
            CategoryTheory.Limits.IsLimit (CommRingCat.prodFan A B)

            The product in CommRingCat is the cartesian product.

            Instances For
              source
              def CommRingCat.equalizerFork {A : CommRingCat} {B : CommRingCat} (f : A ⟶ B) (g : A ⟶ B) :
              CategoryTheory.Limits.Fork f g

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

              Instances For
                source
                def CommRingCat.equalizerForkIsLimit {A : CommRingCat} {B : CommRingCat} (f : A ⟶ B) (g : A ⟶ B) :
                CategoryTheory.Limits.IsLimit (CommRingCat.equalizerFork f g)

                The equalizer in CommRingCat is the equalizer as sets.

                Instances For
                  source
                  instance CommRingCat.instIsLocalRingHomαCommRingObjWalkingParallelPairToQuiverToCategoryStructWalkingParallelPairHomCategoryCommRingCatToQuiverToCategoryStructInstCommRingCatLargeCategoryToPrefunctorObjFunctorCategoryToPrefunctorConstPtParallelPairEqualizerForkZeroToSemiringToRingStrι {A : CommRingCat} {B : CommRingCat} (f : A ⟶ B) (g : A ⟶ B) :
                  IsLocalRingHom (CategoryTheory.Limits.Fork.ι (CommRingCat.equalizerFork f g))
                  source
                  instance CommRingCat.equalizer_ι_isLocalRingHom (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair CommRingCat) :
                  IsLocalRingHom (CategoryTheory.Limits.limit.π F CategoryTheory.Limits.WalkingParallelPair.zero)
                  source
                  instance CommRingCat.equalizer_ι_is_local_ring_hom' (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPairᵒᵖ CommRingCat) :
                  IsLocalRingHom (CategoryTheory.Limits.limit.π F (Opposite.op CategoryTheory.Limits.WalkingParallelPair.one))
                  source
                  def CommRingCat.pullbackCone {A : CommRingCat} {B : CommRingCat} {C : CommRingCat} (f : A ⟶ C) (g : B ⟶ C) :
                  CategoryTheory.Limits.PullbackCone f g

                  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
                    source
                    def CommRingCat.pullbackConeIsLimit {A : CommRingCat} {B : CommRingCat} {C : CommRingCat} (f : A ⟶ C) (g : B ⟶ C) :
                    CategoryTheory.Limits.IsLimit (CommRingCat.pullbackCone f g)

                    The constructed pullback cone is indeed the limit.

                    Instances For