Commit 2023-03-01 07:31 cbd89368

View on Github →

feat: port/CategoryTheory.Limits.Preserves.Basic (#2377)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Preserves/Basic.lean

added def CategoryTheory.Limits.fullyFaithfulReflectsColimits

added def CategoryTheory.Limits.fullyFaithfulReflectsLimits

added def CategoryTheory.Limits.isColimitOfPreserves

added def CategoryTheory.Limits.isColimitOfReflects

added def CategoryTheory.Limits.isLimitOfPreserves

added def CategoryTheory.Limits.isLimitOfReflects

added def CategoryTheory.Limits.preservesColimitOfIsoDiagram

added def CategoryTheory.Limits.preservesColimitOfNatIso

added def CategoryTheory.Limits.preservesColimitOfPreservesColimitCocone

added def CategoryTheory.Limits.preservesColimitOfReflectsOfPreserves

added def CategoryTheory.Limits.preservesColimitsOfNatIso

added def CategoryTheory.Limits.preservesColimitsOfReflectsOfPreserves

added def CategoryTheory.Limits.preservesColimitsOfShapeOfEquiv

added def CategoryTheory.Limits.preservesColimitsOfShapeOfNatIso

added def CategoryTheory.Limits.preservesColimitsOfShapeOfReflectsOfPreserves

added def CategoryTheory.Limits.preservesColimitsOfSizeShrink

added def CategoryTheory.Limits.preservesLimitOfIsoDiagram

added def CategoryTheory.Limits.preservesLimitOfNatIso

added def CategoryTheory.Limits.preservesLimitOfPreservesLimitCone

added def CategoryTheory.Limits.preservesLimitOfReflectsOfPreserves

added def CategoryTheory.Limits.preservesLimitsOfNatIso

added def CategoryTheory.Limits.preservesLimitsOfReflectsOfPreserves

added def CategoryTheory.Limits.preservesLimitsOfShapeOfEquiv

added def CategoryTheory.Limits.preservesLimitsOfShapeOfNatIso

added def CategoryTheory.Limits.preservesLimitsOfShapeOfReflectsOfPreserves

added def CategoryTheory.Limits.preservesLimitsOfSizeShrink

added def CategoryTheory.Limits.preservesSmallestColimitsOfPreservesColimits

added def CategoryTheory.Limits.preservesSmallestLimitsOfPreservesLimits

added def CategoryTheory.Limits.reflectsColimitOfIsoDiagram

added def CategoryTheory.Limits.reflectsColimitOfNatIso

added def CategoryTheory.Limits.reflectsColimitOfReflectsIsomorphisms

added def CategoryTheory.Limits.reflectsColimitsOfNatIso

added def CategoryTheory.Limits.reflectsColimitsOfReflectsIsomorphisms

added def CategoryTheory.Limits.reflectsColimitsOfShapeOfEquiv

added def CategoryTheory.Limits.reflectsColimitsOfShapeOfNatIso

added def CategoryTheory.Limits.reflectsColimitsOfShapeOfReflectsIsomorphisms

added def CategoryTheory.Limits.reflectsColimitsOfSizeShrink

added def CategoryTheory.Limits.reflectsLimitOfIsoDiagram

added def CategoryTheory.Limits.reflectsLimitOfNatIso

added def CategoryTheory.Limits.reflectsLimitOfReflectsIsomorphisms

added def CategoryTheory.Limits.reflectsLimitsOfNatIso

added def CategoryTheory.Limits.reflectsLimitsOfReflectsIsomorphisms

added def CategoryTheory.Limits.reflectsLimitsOfShapeOfEquiv

added def CategoryTheory.Limits.reflectsLimitsOfShapeOfNatIso

added def CategoryTheory.Limits.reflectsLimitsOfShapeOfReflectsIsomorphisms

added def CategoryTheory.Limits.reflectsLimitsOfSizeShrink

added def CategoryTheory.Limits.reflectsSmallestColimitsOfReflectsColimits

added def CategoryTheory.Limits.reflectsSmallestLimitsOfReflectsLimits