Documentation

Mathlib.CategoryTheory.Join.Final

(Co)Finality of the inclusions in joins of category #

This file records the fact that inclLeft C D : C ⥤ C ⋆ D is initial if C is connected. Dually, inclRight : C ⥤ C ⋆ D is final if D is connected.

The category of Join.inclLeft C D-costructured arrows with target right d is equivalent to C.

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

    The category of Join.inclRight C D-structured arrows with source left c is equivalent to D.

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