Commit 2023-03-08 07:00 6df2c84c

View on Github →

feat: port CategoryTheory.Limits.KanExtension (#2601)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/KanExtension.lean

added def CategoryTheory.Lan.adjunction

added def CategoryTheory.Lan.cocone

added theorem CategoryTheory.Lan.coreflective

added def CategoryTheory.Lan.equiv

added def CategoryTheory.Lan.loc

added def CategoryTheory.Ran.adjunction

added def CategoryTheory.Ran.cone

added def CategoryTheory.Ran.equiv

added def CategoryTheory.Ran.loc

added theorem CategoryTheory.Ran.reflective

added def CategoryTheory.lan

added def CategoryTheory.ran