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.

source
def CategoryTheory.Join.costructuredArrowEquiv (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (d : D) :
CostructuredArrow (inclLeft C D) (right d) ≌ C

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
    source
    def CategoryTheory.Join.structuredArrowEquiv (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (c : C) :
    StructuredArrow (left c) (inclRight C D) ≌ D

    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
      source
      instance CategoryTheory.Join.instInitialInclLeftOfIsConnected (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [IsConnected C] :
      (inclLeft C D).Initial
      source
      instance CategoryTheory.Join.instFinalInclRightOfIsConnected (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [IsConnected D] :
      (inclRight C D).Final