Documentation

Mathlib.CategoryTheory.Discrete.StructuredArrow

Structured arrows when the target category is discrete #

When T is a type with a unique element t, we show that if F : C ⥤ Discrete T, then the categories StructuredArrow (Discrete.mk t) F and CostructuredArrow (Discrete.mk t) F are equivalent to C.

source
def CategoryTheory.Discrete.structuredArrowEquivalenceOfUnique {C : Type u} [Category.{v, u} C] {T : Type w} (F : Functor C (Discrete T)) (t : T) [Subsingleton T] :
StructuredArrow { as := t } F ≌ C

If F : C ⥤ Discrete T is a functor with T containing a unique element t, then this is the equivalence StructuredArrow (Discrete.mk t) F ≌ C.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def CategoryTheory.Discrete.costructuredArrowEquivalenceOfUnique {C : Type u} [Category.{v, u} C] {T : Type w} (F : Functor C (Discrete T)) (t : T) [Subsingleton T] :
    CostructuredArrow F { as := t } ≌ C

    If F : C ⥤ Discrete T is a functor with T containing a unique element t, then this is the equivalence CostructuredArrow F (Discrete.mk t) ≌ C.

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