Commit 2023-03-06 07:28 de999b27

View on Github →

feat: port CategoryTheory.Limits.Creates (#2646)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Creates.lean

added structure CategoryTheory.LiftableCocone

added structure CategoryTheory.LiftableCone

added structure CategoryTheory.LiftsToColimit

added structure CategoryTheory.LiftsToLimit

added def CategoryTheory.createsColimitOfFullyFaithfulOfIso'

added def CategoryTheory.createsColimitOfFullyFaithfulOfIso

added def CategoryTheory.createsColimitOfFullyFaithfulOfLift'

added def CategoryTheory.createsColimitOfFullyFaithfulOfLift

added def CategoryTheory.createsColimitOfIsoDiagram

added def CategoryTheory.createsColimitOfNatIso

added def CategoryTheory.createsColimitOfReflectsIso

added def CategoryTheory.createsColimitsOfNatIso

added def CategoryTheory.createsColimitsOfShapeOfNatIso

added def CategoryTheory.createsLimitOfFullyFaithfulOfIso'

added def CategoryTheory.createsLimitOfFullyFaithfulOfIso

added def CategoryTheory.createsLimitOfFullyFaithfulOfLift'

added def CategoryTheory.createsLimitOfFullyFaithfulOfLift

added def CategoryTheory.createsLimitOfIsoDiagram

added def CategoryTheory.createsLimitOfNatIso

added def CategoryTheory.createsLimitOfReflectsIso

added def CategoryTheory.createsLimitsOfNatIso

added def CategoryTheory.createsLimitsOfShapeOfNatIso

added theorem CategoryTheory.hasColimit_of_created

added theorem CategoryTheory.hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape

added theorem CategoryTheory.hasLimit_of_created

added theorem CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape

added theorem CategoryTheory.has_colimits_of_has_colimits_creates_colimits

added theorem CategoryTheory.has_limits_of_has_limits_creates_limits

added def CategoryTheory.idLiftsCocone

added def CategoryTheory.idLiftsCone

added def CategoryTheory.liftColimit

added def CategoryTheory.liftLimit

added def CategoryTheory.liftedColimitIsColimit

added def CategoryTheory.liftedColimitMapsToOriginal

added def CategoryTheory.liftedLimitIsLimit

added def CategoryTheory.liftedLimitMapsToOriginal

added def CategoryTheory.liftsToColimitOfCreates

added def CategoryTheory.liftsToLimitOfCreates