Commit 2023-03-07 06:55 099cf190

View on Github →

feat: port CategoryTheory.Adjunction.Limits (#2683)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Adjunction/Limits.lean

added def CategoryTheory.Adjunction.coconesIso

added def CategoryTheory.Adjunction.coconesIsoComponentHom

added def CategoryTheory.Adjunction.coconesIsoComponentInv

added def CategoryTheory.Adjunction.conesIso

added def CategoryTheory.Adjunction.conesIsoComponentHom

added def CategoryTheory.Adjunction.conesIsoComponentInv

added def CategoryTheory.Adjunction.functorialityCounit'

added def CategoryTheory.Adjunction.functorialityCounit

added def CategoryTheory.Adjunction.functorialityIsLeftAdjoint

added def CategoryTheory.Adjunction.functorialityIsRightAdjoint

added def CategoryTheory.Adjunction.functorialityLeftAdjoint

added def CategoryTheory.Adjunction.functorialityRightAdjoint

added def CategoryTheory.Adjunction.functorialityUnit'

added def CategoryTheory.Adjunction.functorialityUnit

added theorem CategoryTheory.Adjunction.hasColimit_comp_equivalence

added theorem CategoryTheory.Adjunction.hasColimit_of_comp_equivalence

added theorem CategoryTheory.Adjunction.hasColimitsOfShape_of_equivalence

added theorem CategoryTheory.Adjunction.hasLimit_comp_equivalence

added theorem CategoryTheory.Adjunction.hasLimit_of_comp_equivalence

added theorem CategoryTheory.Adjunction.hasLimitsOfShape_of_equivalence

added theorem CategoryTheory.Adjunction.has_colimits_of_equivalence

added theorem CategoryTheory.Adjunction.has_limits_of_equivalence

added def CategoryTheory.Adjunction.leftAdjointPreservesColimits

added def CategoryTheory.Adjunction.rightAdjointPreservesLimits