mathlib3 documentation

category_theory.limits.cone_category

Limits and the category of (co)cones #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This files contains results that stem from the limit API. For the definition and the category instance of cone, please refer to category_theory/limits/cones.lean.

Main results #

Construct an object of the category (Δ ↓ F) from a cone on F. This is part of an equivalence, see cone.equiv_costructured_arrow.

Equations

Construct a cone on F from an object of the category (Δ ↓ F). This is part of an equivalence, see cone.equiv_costructured_arrow.

Equations

Construct an object of the category (F ↓ Δ) from a cocone on F. This is part of an equivalence, see cocone.equiv_structured_arrow.

Equations

Construct a cocone on F from an object of the category (F ↓ Δ). This is part of an equivalence, see cocone.equiv_structured_arrow.

Equations