(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.
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)
:
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
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)
:
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
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]
:
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]
: