Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-03-10 07:31
7a06df46
View on Github →
feat: port CategoryTheory.Adjunction.Comma (
#2591
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/CategoryTheory/Adjunction/Comma.lean
added
def
CategoryTheory.adjunctionOfCostructuredArrowTerminals
added
def
CategoryTheory.adjunctionOfStructuredArrowInitials
added
def
CategoryTheory.isLeftAdjointOfCostructuredArrowTerminals
added
def
CategoryTheory.isRightAdjointOfStructuredArrowInitials
added
def
CategoryTheory.leftAdjointOfStructuredArrowInitials
added
def
CategoryTheory.leftAdjointOfStructuredArrowInitialsAux
added
def
CategoryTheory.mkInitialOfLeftAdjoint
added
def
CategoryTheory.mkTerminalOfRightAdjoint
added
theorem
CategoryTheory.nonempty_isLeftAdjoint_iff_hasTerminal_costructuredArrow
added
theorem
CategoryTheory.nonempty_isRightAdjoint_iff_hasInitial_structuredArrow
added
def
CategoryTheory.rightAdjointOfCostructuredArrowTerminals
added
def
CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux