Documentation

Mathlib.CategoryTheory.Limits.ConeCategory

Limits and the category of (co)cones #

This files contains results that stem from the limit API. For the definition and the category instance of Cone, please refer to CategoryTheory/Limits/Cones.lean.

Main results #

Given a cone c over F, we can interpret the legs of c as structured arrows c.pt ⟶ F.obj -.

Instances For

    Interpreting the legs of a cone as a structured arrow, interpreting this arrow as an arrow over the cone point, and finally forgetting the arrow is the same as just applying the functor the cone was over.

    Instances For

      Given a cone c : Cone K and a map f : X ⟶ F.obj c.X, we can construct a cone of structured arrows over X with f as the cone point.

      Instances For

        The category of cones on F is just the comma category (Δ ↓ F), where Δ is the constant functor.

        Instances For

          Given a cocone c over F, we can interpret the legs of c as costructured arrows F.obj - ⟶ c.pt.

          Instances For

            Interpreting the legs of a cocone as a costructured arrow, interpreting this arrow as an arrow over the cocone point, and finally forgetting the arrow is the same as just applying the functor the cocone was over.

            Instances For

              Given a cocone c : Cocone K and a map f : F.obj c.X ⟶ X, we can construct a cocone of costructured arrows over X with f as the cone point.

              Instances For

                The category of cocones on F is just the comma category (F ↓ Δ), where Δ is the constant functor.

                Instances For