Commit 2024-11-19 08:25 809872da

View on Github →

refactor(CategoryTheory): make PreservesLimit and ReflectsLimit props (#19206) All changes are straightforward. Some universe parameters had to be made explicit, but without changing the level of generality of the definitions/statements.

Estimated changes

Modified Mathlib/Algebra/Category/AlgebraCat/Limits.lean

Modified Mathlib/Algebra/Category/Grp/AB5.lean

Modified Mathlib/Algebra/Category/Grp/FilteredColimits.lean

Modified Mathlib/Algebra/Category/Grp/Limits.lean

Modified Mathlib/Algebra/Category/ModuleCat/Abelian.lean

Modified Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

Modified Mathlib/Algebra/Category/ModuleCat/Colimits.lean

Modified Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean

Modified Mathlib/Algebra/Category/ModuleCat/Limits.lean

deleted def ModuleCat.forget₂AddCommGroupPreservesLimitsAux

added def ModuleCat.forget₂AddCommGroup_preservesLimitsAux

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf/Colimits.lean

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafification.lean

Modified Mathlib/Algebra/Category/ModuleCat/Sheaf/Limits.lean

Modified Mathlib/Algebra/Category/MonCat/FilteredColimits.lean

Modified Mathlib/Algebra/Category/MonCat/Limits.lean

Modified Mathlib/Algebra/Category/Ring/FilteredColimits.lean

Modified Mathlib/Algebra/Category/Ring/Limits.lean

Modified Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean

Modified Mathlib/Algebra/Homology/HomologicalComplexBiprod.lean

Modified Mathlib/Algebra/Homology/HomologicalComplexLimits.lean

deleted def HomologicalComplex.preservesColimitsOfShapeOfEval

added theorem HomologicalComplex.preservesColimitsOfShape_of_eval

deleted def HomologicalComplex.preservesLimitsOfShapeOfEval

added theorem HomologicalComplex.preservesLimitsOfShape_of_eval

Modified Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean

Modified Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean

added theorem CategoryTheory.Functor.preservesFiniteColimits_of_preservesHomology

added theorem CategoryTheory.Functor.preservesFiniteLimits_of_preservesHomology

Modified Mathlib/Algebra/Homology/ShortComplex/Limits.lean

Modified Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean

added theorem CategoryTheory.Functor.PreservesHomology.preservesCokernel

deleted def CategoryTheory.Functor.PreservesHomology.preservesCokernel

added theorem CategoryTheory.Functor.PreservesHomology.preservesKernel

deleted def CategoryTheory.Functor.PreservesHomology.preservesKernel

added theorem CategoryTheory.Functor.PreservesLeftHomologyOf.mk'

deleted def CategoryTheory.Functor.PreservesLeftHomologyOf.mk'

added theorem CategoryTheory.Functor.PreservesRightHomologyOf.mk'

deleted def CategoryTheory.Functor.PreservesRightHomologyOf.mk'

added theorem CategoryTheory.Functor.preservesLeftHomology_of_zero_f

added theorem CategoryTheory.Functor.preservesLeftHomology_of_zero_g

added theorem CategoryTheory.Functor.preservesRightHomology_of_zero_f

added theorem CategoryTheory.Functor.preservesRightHomology_of_zero_g

added theorem CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hf'

deleted def CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hf'

added theorem CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hg

deleted def CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hg

added theorem CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hf

deleted def CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hf

added theorem CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hg'

deleted def CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hg'

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

Modified Mathlib/AlgebraicGeometry/Limits.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/Product.lean

added theorem FundamentalGroupoidFunctor.preservesProduct

deleted def FundamentalGroupoidFunctor.preservesProduct

Modified Mathlib/CategoryTheory/Abelian/Exact.lean

deleted def CategoryTheory.Functor.preservesHomologyOfMapExact

deleted def CategoryTheory.Functor.preservesHomologyOfPreservesEpisAndKernels

deleted def CategoryTheory.Functor.preservesHomologyOfPreservesMonosAndCokernels

added theorem CategoryTheory.Functor.preservesHomology_of_map_exact

added theorem CategoryTheory.Functor.preservesHomology_of_preservesEpis_and_kernels

added theorem CategoryTheory.Functor.preservesHomology_of_preservesMonos_and_cokernels

Modified Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean

deleted def CategoryTheory.AB4.ofAB5

added theorem CategoryTheory.AB4.of_AB5

Modified Mathlib/CategoryTheory/Abelian/Injective.lean

Modified Mathlib/CategoryTheory/Abelian/Projective.lean

Modified Mathlib/CategoryTheory/Abelian/Transfer.lean

Modified Mathlib/CategoryTheory/Adhesive.lean

Modified Mathlib/CategoryTheory/Adjunction/Limits.lean

added theorem CategoryTheory.Adjunction.isEquivalenceReflectsColimits

added theorem CategoryTheory.Adjunction.isEquivalenceReflectsLimits

added theorem CategoryTheory.Adjunction.leftAdjointPreservesColimits

deleted def CategoryTheory.Adjunction.leftAdjointPreservesColimits

added theorem CategoryTheory.Adjunction.leftAdjoint_preservesColimits

added theorem CategoryTheory.Adjunction.rightAdjointPreservesLimits

deleted def CategoryTheory.Adjunction.rightAdjointPreservesLimits

added theorem CategoryTheory.Adjunction.rightAdjoint_preservesLimits

Modified Mathlib/CategoryTheory/Category/Cat/Limit.lean

Modified Mathlib/CategoryTheory/ChosenFiniteProducts.lean

deleted def CategoryTheory.ChosenFiniteProducts.isLimitChosenFiniteProductsOfPreservesLimits

added theorem CategoryTheory.ChosenFiniteProducts.preservesLimit_empty_of_isIso_terminalComparison

added theorem CategoryTheory.ChosenFiniteProducts.preservesLimit_pair_of_isIso_prodComparison

added theorem CategoryTheory.ChosenFiniteProducts.preservesLimitsOfShape_discrete_walkingPair_of_isIso_prodComparison

deleted def CategoryTheory.ChosenFiniteProducts.preservesTerminalIso

deleted def CategoryTheory.ChosenFiniteProducts.prodComparisonIso

Modified Mathlib/CategoryTheory/ChosenFiniteProducts/FunctorCategory.lean

Modified Mathlib/CategoryTheory/Closed/Cartesian.lean

Modified Mathlib/CategoryTheory/Closed/Ideal.lean

added theorem CategoryTheory.preservesBinaryProducts_of_exponentialIdeal

added theorem CategoryTheory.preservesFiniteProducts_of_exponentialIdeal

Modified Mathlib/CategoryTheory/Closed/Monoidal.lean

Modified Mathlib/CategoryTheory/Extensive.lean

Modified Mathlib/CategoryTheory/Functor/Flat.lean

added theorem CategoryTheory.preservesFiniteColimits_iff_coflat

added theorem CategoryTheory.preservesFiniteColimits_of_coflat

added theorem CategoryTheory.preservesFiniteLimits_iff_flat

added theorem CategoryTheory.preservesFiniteLimits_iff_lan_preservesFiniteLimits

added theorem CategoryTheory.preservesFiniteLimits_of_flat

Modified Mathlib/CategoryTheory/Galois/Action.lean

Modified Mathlib/CategoryTheory/Galois/Basic.lean

added theorem CategoryTheory.PreGaloisCategory.FiberFunctor.comp_right

Modified Mathlib/CategoryTheory/Galois/Examples.lean

Modified Mathlib/CategoryTheory/Galois/GaloisObjects.lean

Modified Mathlib/CategoryTheory/Galois/Prorepresentability.lean

Modified Mathlib/CategoryTheory/GlueData.lean

Modified Mathlib/CategoryTheory/GradedObject/Monoidal.lean

Modified Mathlib/CategoryTheory/Limits/Comma.lean

deleted def CategoryTheory.Comma.coconeOfPreserves

deleted def CategoryTheory.Comma.coconeOfPreservesIsColimit

deleted def CategoryTheory.Comma.coneOfPreserves

deleted def CategoryTheory.Comma.coneOfPreservesIsLimit

Modified Mathlib/CategoryTheory/Limits/ConeCategory.lean

deleted def CategoryTheory.Limits.IsColimit.ofPreservesCoconeInitial

deleted def CategoryTheory.Limits.IsColimit.ofReflectsCoconeInitial

deleted def CategoryTheory.Limits.IsLimit.ofPreservesConeTerminal

deleted def CategoryTheory.Limits.IsLimit.ofReflectsConeTerminal

Modified Mathlib/CategoryTheory/Limits/Connected.lean

added theorem CategoryTheory.prod_preservesConnectedLimits

Modified Mathlib/CategoryTheory/Limits/Constructions/BinaryProducts.lean

added theorem preservesBinaryCoproducts_of_preservesInitial_and_pushouts

added theorem preservesBinaryProducts_of_preservesTerminal_and_pullbacks

Modified Mathlib/CategoryTheory/Limits/Constructions/Equalizers.lean

deleted def CategoryTheory.Limits.preservesCoequalizersOfPreservesPushoutsAndBinaryCoproducts

added theorem CategoryTheory.Limits.preservesCoequalizers_of_preservesPushouts_and_binaryCoproducts

deleted def CategoryTheory.Limits.preservesEqualizersOfPreservesPullbacksAndBinaryProducts

added theorem CategoryTheory.Limits.preservesEqualizers_of_preservesPullbacks_and_binaryProducts

Modified Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean

added theorem CategoryTheory.preservesFinOfPreservesBinaryAndTerminal

added theorem CategoryTheory.preservesFiniteCoproductsOfPreservesBinaryAndInitial

deleted def CategoryTheory.preservesFiniteCoproductsOfPreservesBinaryAndInitial

deleted def CategoryTheory.preservesFiniteProductsOfPreservesBinaryAndTerminal

added theorem CategoryTheory.preservesFiniteProducts_of_preserves_binary_and_terminal

deleted def CategoryTheory.preservesShapeFinOfPreservesBinaryAndInitial

deleted def CategoryTheory.preservesShapeFinOfPreservesBinaryAndTerminal

added theorem CategoryTheory.preservesShape_fin_of_preserves_binary_and_initial

added theorem CategoryTheory.preservesShape_fin_of_preserves_binary_and_terminal

added theorem CategoryTheory.preserves_fin_of_preserves_binary_and_initial

Modified Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean

added theorem CategoryTheory.Limits.preservesColimit_of_preservesCoequalizers_and_coproduct

added theorem CategoryTheory.Limits.preservesColimits_of_preservesCoequalizers_and_coproducts

added theorem CategoryTheory.Limits.preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts

added theorem CategoryTheory.Limits.preservesFiniteColimits_of_preservesInitial_and_pushouts

added theorem CategoryTheory.Limits.preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts

added theorem CategoryTheory.Limits.preservesFiniteLimits_of_preservesTerminal_and_pullbacks

added theorem CategoryTheory.Limits.preservesLimit_of_preservesEqualizers_and_product

added theorem CategoryTheory.Limits.preservesLimits_of_preservesEqualizers_and_products

Modified Mathlib/CategoryTheory/Limits/Creates.lean

added theorem CategoryTheory.preservesColimitOfCreatesColimitAndHasColimit

added theorem CategoryTheory.preservesColimitOfShapeOfCreatesColimitsOfShapeAndHasColimitsOfShape

added theorem CategoryTheory.preservesColimitsOfCreatesColimitsAndHasColimits

added theorem CategoryTheory.preservesLimitOfCreatesLimitAndHasLimit

added theorem CategoryTheory.preservesLimitOfShapeOfCreatesLimitsOfShapeAndHasLimitsOfShape

added theorem CategoryTheory.preservesLimitsOfCreatesLimitsAndHasLimits

Modified Mathlib/CategoryTheory/Limits/ExactFunctor.lean

Modified Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean

Modified Mathlib/CategoryTheory/Limits/FintypeCat.lean

Modified Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean

added theorem CategoryTheory.Limits.preservesColimitOfEvaluation

deleted def CategoryTheory.Limits.preservesColimitOfEvaluation

added theorem CategoryTheory.Limits.preservesColimit_of_evaluation

deleted def CategoryTheory.Limits.preservesColimitsOfEvaluation

deleted def CategoryTheory.Limits.preservesColimitsOfShapeOfEvaluation

added theorem CategoryTheory.Limits.preservesColimitsOfShape_of_evaluation

added theorem CategoryTheory.Limits.preservesColimits_of_evaluation

added theorem CategoryTheory.Limits.preservesLimitOfEvaluation

deleted def CategoryTheory.Limits.preservesLimitOfEvaluation

added theorem CategoryTheory.Limits.preservesLimit_of_evaluation

added theorem CategoryTheory.Limits.preservesLimitsOfEvaluation

deleted def CategoryTheory.Limits.preservesLimitsOfEvaluation

added theorem CategoryTheory.Limits.preservesLimitsOfShapeOfEvaluation

deleted def CategoryTheory.Limits.preservesLimitsOfShapeOfEvaluation

added theorem CategoryTheory.Limits.preservesLimitsOfShape_of_evaluation

added theorem CategoryTheory.Limits.preservesLimits_of_evaluation

Modified Mathlib/CategoryTheory/Limits/Over.lean

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

added theorem CategoryTheory.Limits.PreservesColimitsOfSizeShrink

added theorem CategoryTheory.Limits.PreservesLimitsOfSizeShrink

added theorem CategoryTheory.Limits.compPreservesColimit

added theorem CategoryTheory.Limits.compPreservesColimits

added theorem CategoryTheory.Limits.compPreservesColimitsOfShape

added theorem CategoryTheory.Limits.compPreservesLimit

added theorem CategoryTheory.Limits.compPreservesLimits

added theorem CategoryTheory.Limits.compPreservesLimitsOfShape

added theorem CategoryTheory.Limits.compReflectsColimit

added theorem CategoryTheory.Limits.compReflectsColimits

added theorem CategoryTheory.Limits.compReflectsColimitsOfShape

added theorem CategoryTheory.Limits.compReflectsLimit

added theorem CategoryTheory.Limits.compReflectsLimits

added theorem CategoryTheory.Limits.compReflectsLimitsOfShape

added theorem CategoryTheory.Limits.fullyFaithfulReflectsColimits

added theorem CategoryTheory.Limits.fullyFaithfulReflectsLimits

added theorem CategoryTheory.Limits.idPreservesColimits

added theorem CategoryTheory.Limits.idPreservesLimits

added theorem CategoryTheory.Limits.idReflectsColimits

added theorem CategoryTheory.Limits.idReflectsLimits

added theorem CategoryTheory.Limits.preservesColimitOfIsoDiagram

deleted def CategoryTheory.Limits.preservesColimitOfIsoDiagram

added theorem CategoryTheory.Limits.preservesColimitOfNatIso

deleted def CategoryTheory.Limits.preservesColimitOfNatIso

added theorem CategoryTheory.Limits.preservesColimitOfPreservesColimitCocone

deleted def CategoryTheory.Limits.preservesColimitOfPreservesColimitCocone

added theorem CategoryTheory.Limits.preservesColimitOfReflectsOfPreserves

deleted def CategoryTheory.Limits.preservesColimitOfReflectsOfPreserves

added theorem CategoryTheory.Limits.preservesColimit_of_iso_diagram

added theorem CategoryTheory.Limits.preservesColimit_of_natIso

added theorem CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone

added theorem CategoryTheory.Limits.preservesColimit_of_reflects_of_preserves

added theorem CategoryTheory.Limits.preservesColimitsOfNatIso

deleted def CategoryTheory.Limits.preservesColimitsOfNatIso

added theorem CategoryTheory.Limits.preservesColimitsOfReflectsOfPreserves

deleted def CategoryTheory.Limits.preservesColimitsOfReflectsOfPreserves

added theorem CategoryTheory.Limits.preservesColimitsOfShapeOfEquiv

deleted def CategoryTheory.Limits.preservesColimitsOfShapeOfEquiv

added theorem CategoryTheory.Limits.preservesColimitsOfShapeOfNatIso

deleted def CategoryTheory.Limits.preservesColimitsOfShapeOfNatIso

added theorem CategoryTheory.Limits.preservesColimitsOfShapeOfReflectsOfPreserves

deleted def CategoryTheory.Limits.preservesColimitsOfShapeOfReflectsOfPreserves

added theorem CategoryTheory.Limits.preservesColimitsOfShape_of_equiv

added theorem CategoryTheory.Limits.preservesColimitsOfShape_of_natIso

added theorem CategoryTheory.Limits.preservesColimitsOfShape_of_reflects_of_preserves

added theorem CategoryTheory.Limits.preservesColimitsOfSizeOfUnivLE

deleted def CategoryTheory.Limits.preservesColimitsOfSizeOfUnivLE

deleted def CategoryTheory.Limits.preservesColimitsOfSizeShrink

added theorem CategoryTheory.Limits.preservesColimitsOfSize_of_univLE

added theorem CategoryTheory.Limits.preservesColimitsOfSize_shrink

added theorem CategoryTheory.Limits.preservesColimits_of_natIso

added theorem CategoryTheory.Limits.preservesColimits_of_reflects_of_preserves

added theorem CategoryTheory.Limits.preservesLimitOfIsoDiagram

deleted def CategoryTheory.Limits.preservesLimitOfIsoDiagram

added theorem CategoryTheory.Limits.preservesLimitOfNatIso

deleted def CategoryTheory.Limits.preservesLimitOfNatIso

added theorem CategoryTheory.Limits.preservesLimitOfPreservesLimitCone

deleted def CategoryTheory.Limits.preservesLimitOfPreservesLimitCone

added theorem CategoryTheory.Limits.preservesLimitOfReflectsOfPreserves

deleted def CategoryTheory.Limits.preservesLimitOfReflectsOfPreserves

added theorem CategoryTheory.Limits.preservesLimit_of_iso_diagram

added theorem CategoryTheory.Limits.preservesLimit_of_natIso

added theorem CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone

added theorem CategoryTheory.Limits.preservesLimit_of_reflects_of_preserves

added theorem CategoryTheory.Limits.preservesLimitsOfNatIso

deleted def CategoryTheory.Limits.preservesLimitsOfNatIso

added theorem CategoryTheory.Limits.preservesLimitsOfReflectsOfPreserves

deleted def CategoryTheory.Limits.preservesLimitsOfReflectsOfPreserves

added theorem CategoryTheory.Limits.preservesLimitsOfShapeOfEquiv

deleted def CategoryTheory.Limits.preservesLimitsOfShapeOfEquiv

added theorem CategoryTheory.Limits.preservesLimitsOfShapeOfNatIso

deleted def CategoryTheory.Limits.preservesLimitsOfShapeOfNatIso

added theorem CategoryTheory.Limits.preservesLimitsOfShapeOfReflectsOfPreserves

deleted def CategoryTheory.Limits.preservesLimitsOfShapeOfReflectsOfPreserves

added theorem CategoryTheory.Limits.preservesLimitsOfShape_of_equiv

added theorem CategoryTheory.Limits.preservesLimitsOfShape_of_natIso

added theorem CategoryTheory.Limits.preservesLimitsOfShape_of_reflects_of_preserves

added theorem CategoryTheory.Limits.preservesLimitsOfSizeOfUnivLE

deleted def CategoryTheory.Limits.preservesLimitsOfSizeOfUnivLE

deleted def CategoryTheory.Limits.preservesLimitsOfSizeShrink

added theorem CategoryTheory.Limits.preservesLimitsOfSize_of_univLE

added theorem CategoryTheory.Limits.preservesLimitsOfSize_shrink

added theorem CategoryTheory.Limits.preservesLimits_of_natIso

added theorem CategoryTheory.Limits.preservesLimits_of_reflects_of_preserves

added theorem CategoryTheory.Limits.preservesSmallestColimitsOfPreservesColimits

deleted def CategoryTheory.Limits.preservesSmallestColimitsOfPreservesColimits

added theorem CategoryTheory.Limits.preservesSmallestColimits_of_preservesColimits

added theorem CategoryTheory.Limits.preservesSmallestLimitsOfPreservesLimits

deleted def CategoryTheory.Limits.preservesSmallestLimitsOfPreservesLimits

added theorem CategoryTheory.Limits.preservesSmallestLimits_of_preservesLimits

added theorem CategoryTheory.Limits.reflectsColimitOfIsoDiagram

deleted def CategoryTheory.Limits.reflectsColimitOfIsoDiagram

added theorem CategoryTheory.Limits.reflectsColimitOfNatIso

deleted def CategoryTheory.Limits.reflectsColimitOfNatIso

added theorem CategoryTheory.Limits.reflectsColimitOfReflectsIsomorphisms

deleted def CategoryTheory.Limits.reflectsColimitOfReflectsIsomorphisms

added theorem CategoryTheory.Limits.reflectsColimit_of_iso_diagram

added theorem CategoryTheory.Limits.reflectsColimit_of_natIso

added theorem CategoryTheory.Limits.reflectsColimit_of_reflectsIsomorphisms

added theorem CategoryTheory.Limits.reflectsColimitsOfNatIso

deleted def CategoryTheory.Limits.reflectsColimitsOfNatIso

added theorem CategoryTheory.Limits.reflectsColimitsOfReflectsIsomorphisms

deleted def CategoryTheory.Limits.reflectsColimitsOfReflectsIsomorphisms

added theorem CategoryTheory.Limits.reflectsColimitsOfShapeOfEquiv

deleted def CategoryTheory.Limits.reflectsColimitsOfShapeOfEquiv

added theorem CategoryTheory.Limits.reflectsColimitsOfShapeOfNatIso

deleted def CategoryTheory.Limits.reflectsColimitsOfShapeOfNatIso

added theorem CategoryTheory.Limits.reflectsColimitsOfShapeOfReflectsIsomorphisms

deleted def CategoryTheory.Limits.reflectsColimitsOfShapeOfReflectsIsomorphisms

added theorem CategoryTheory.Limits.reflectsColimitsOfShape_of_equiv

added theorem CategoryTheory.Limits.reflectsColimitsOfShape_of_natIso

added theorem CategoryTheory.Limits.reflectsColimitsOfShape_of_reflectsIsomorphisms

added theorem CategoryTheory.Limits.reflectsColimitsOfSizeOfUnivLE

deleted def CategoryTheory.Limits.reflectsColimitsOfSizeOfUnivLE

added theorem CategoryTheory.Limits.reflectsColimitsOfSizeShrink

deleted def CategoryTheory.Limits.reflectsColimitsOfSizeShrink

added theorem CategoryTheory.Limits.reflectsColimitsOfSize_of_univLE

added theorem CategoryTheory.Limits.reflectsColimitsOfSize_shrink

added theorem CategoryTheory.Limits.reflectsColimits_of_natIso

added theorem CategoryTheory.Limits.reflectsColimits_of_reflectsIsomorphisms

added theorem CategoryTheory.Limits.reflectsLimitOfIsoDiagram

deleted def CategoryTheory.Limits.reflectsLimitOfIsoDiagram

added theorem CategoryTheory.Limits.reflectsLimitOfNatIso

deleted def CategoryTheory.Limits.reflectsLimitOfNatIso

added theorem CategoryTheory.Limits.reflectsLimitOfReflectsIsomorphisms

deleted def CategoryTheory.Limits.reflectsLimitOfReflectsIsomorphisms

added theorem CategoryTheory.Limits.reflectsLimit_of_iso_diagram

added theorem CategoryTheory.Limits.reflectsLimit_of_natIso

added theorem CategoryTheory.Limits.reflectsLimit_of_reflectsIsomorphisms

added theorem CategoryTheory.Limits.reflectsLimitsOfNatIso

deleted def CategoryTheory.Limits.reflectsLimitsOfNatIso

added theorem CategoryTheory.Limits.reflectsLimitsOfReflectsIsomorphisms

deleted def CategoryTheory.Limits.reflectsLimitsOfReflectsIsomorphisms

added theorem CategoryTheory.Limits.reflectsLimitsOfShapeOfEquiv

deleted def CategoryTheory.Limits.reflectsLimitsOfShapeOfEquiv

added theorem CategoryTheory.Limits.reflectsLimitsOfShapeOfNatIso

deleted def CategoryTheory.Limits.reflectsLimitsOfShapeOfNatIso

added theorem CategoryTheory.Limits.reflectsLimitsOfShapeOfReflectsIsomorphisms

deleted def CategoryTheory.Limits.reflectsLimitsOfShapeOfReflectsIsomorphisms

added theorem CategoryTheory.Limits.reflectsLimitsOfShape_of_equiv

added theorem CategoryTheory.Limits.reflectsLimitsOfShape_of_natIso

added theorem CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsIsomorphisms

added theorem CategoryTheory.Limits.reflectsLimitsOfSizeOfUnivLE

deleted def CategoryTheory.Limits.reflectsLimitsOfSizeOfUnivLE

added theorem CategoryTheory.Limits.reflectsLimitsOfSizeShrink

deleted def CategoryTheory.Limits.reflectsLimitsOfSizeShrink

added theorem CategoryTheory.Limits.reflectsLimitsOfSize_of_univLE

added theorem CategoryTheory.Limits.reflectsLimitsOfSize_shrink

added theorem CategoryTheory.Limits.reflectsLimits_of_natIso

added theorem CategoryTheory.Limits.reflectsLimits_of_reflectsIsomorphisms

added theorem CategoryTheory.Limits.reflectsSmallestColimitsOfReflectsColimits

deleted def CategoryTheory.Limits.reflectsSmallestColimitsOfReflectsColimits

added theorem CategoryTheory.Limits.reflectsSmallestColimits_of_reflectsColimits

added theorem CategoryTheory.Limits.reflectsSmallestLimitsOfReflectsLimits

deleted def CategoryTheory.Limits.reflectsSmallestLimitsOfReflectsLimits

added theorem CategoryTheory.Limits.reflectsSmallestLimits_of_reflectsLimits

Modified Mathlib/CategoryTheory/Limits/Preserves/Filtered.lean

added theorem CategoryTheory.Limits.preservesCofilteredLimitsOfSize_of_univLE

added theorem CategoryTheory.Limits.preservesCofilteredLimitsOfSize_shrink

added theorem CategoryTheory.Limits.preservesFilteredColimitsOfSize_of_univLE

added theorem CategoryTheory.Limits.preservesFilteredColimitsOfSize_shrink

added theorem CategoryTheory.Limits.preservesSmallestCofilteredLimits_of_preservesCofilteredLimits

added theorem CategoryTheory.Limits.preservesSmallestFilteredColimits_of_preservesFilteredColimits

added theorem CategoryTheory.Limits.reflectsCofilteredLimitsOfSize_of_univLE

added theorem CategoryTheory.Limits.reflectsCofilteredLimitsOfSize_shrink

added theorem CategoryTheory.Limits.reflectsFilteredColimitsOfSize_of_univLE

added theorem CategoryTheory.Limits.reflectsFilteredColimitsOfSize_shrink

added theorem CategoryTheory.Limits.reflectsSmallestCofilteredLimits_of_reflectsCofilteredLimits

added theorem CategoryTheory.Limits.reflectsSmallestFilteredColimits_of_reflectsFilteredColimits

Modified Mathlib/CategoryTheory/Limits/Preserves/Finite.lean

added theorem CategoryTheory.Limits.PreservesColimitsOfSize.preservesFiniteColimits

added theorem CategoryTheory.Limits.PreservesLimitsOfSize.preservesFiniteLimits

added theorem CategoryTheory.Limits.ReflectsColimitsOfSize.reflectsFiniteColimits

added theorem CategoryTheory.Limits.ReflectsLimitsOfSize.reflectsFiniteLimits

deleted def CategoryTheory.Limits.compPreservesFiniteColimits

deleted def CategoryTheory.Limits.compPreservesFiniteLimits

added theorem CategoryTheory.Limits.comp_preservesFiniteColimits

added theorem CategoryTheory.Limits.comp_preservesFiniteLimits

deleted def CategoryTheory.Limits.preservesFiniteColimitsOfNatIso

deleted def CategoryTheory.Limits.preservesFiniteColimitsOfPreservesFiniteColimitsOfSize

deleted def CategoryTheory.Limits.preservesFiniteColimitsOfReflectsOfPreserves

added theorem CategoryTheory.Limits.preservesFiniteColimits_of_natIso

added theorem CategoryTheory.Limits.preservesFiniteColimits_of_preservesFiniteColimitsOfSize

added theorem CategoryTheory.Limits.preservesFiniteColimits_of_reflects_of_preserves

added theorem CategoryTheory.Limits.preservesFiniteCoproducts_of_reflects_of_preserves

deleted def CategoryTheory.Limits.preservesFiniteLimitsOfNatIso

deleted def CategoryTheory.Limits.preservesFiniteLimitsOfPreservesFiniteLimitsOfSize

deleted def CategoryTheory.Limits.preservesFiniteLimitsOfReflectsOfPreserves

added theorem CategoryTheory.Limits.preservesFiniteLimits_of_natIso

added theorem CategoryTheory.Limits.preservesFiniteLimits_of_preservesFiniteLimitsOfSize

added theorem CategoryTheory.Limits.preservesFiniteLimits_of_reflects_of_preserves

deleted def CategoryTheory.Limits.preservesFiniteProductsOfReflectsOfPreserves

added theorem CategoryTheory.Limits.preservesFiniteProducts_of_reflects_of_preserves

Modified Mathlib/CategoryTheory/Limits/Preserves/FunctorCategory.lean

deleted def CategoryTheory.FunctorCategory.prodPreservesColimits

added theorem CategoryTheory.FunctorCategory.prod_preservesColimits

deleted def CategoryTheory.preservesFiniteColimitsOfEvaluation

added theorem CategoryTheory.preservesFiniteColimits_of_evaluation

deleted def CategoryTheory.preservesFiniteLimitsOfEvaluation

added theorem CategoryTheory.preservesFiniteLimits_of_evaluation

added theorem CategoryTheory.preservesLimit_of_lan_preservesLimit

Modified Mathlib/CategoryTheory/Limits/Preserves/Limits.lean

deleted def CategoryTheory.preservesColimitOfIsIsoPost

added theorem CategoryTheory.preservesColimit_of_isIso_post

deleted def CategoryTheory.preservesLimitOfIsIsoPost

added theorem CategoryTheory.preservesLimit_of_isIso_post

Modified Mathlib/CategoryTheory/Limits/Preserves/Opposites.lean

deleted def CategoryTheory.Limits.perservesColimitsOp

added theorem CategoryTheory.Limits.perservesColimits_op

deleted def CategoryTheory.Limits.preservesColimitLeftOp

deleted def CategoryTheory.Limits.preservesColimitOfLeftOp

deleted def CategoryTheory.Limits.preservesColimitOfOp

deleted def CategoryTheory.Limits.preservesColimitOfRightOp

deleted def CategoryTheory.Limits.preservesColimitOfUnop

deleted def CategoryTheory.Limits.preservesColimitOp

deleted def CategoryTheory.Limits.preservesColimitRightOp

deleted def CategoryTheory.Limits.preservesColimitUnop

added theorem CategoryTheory.Limits.preservesColimit_leftOp

added theorem CategoryTheory.Limits.preservesColimit_of_leftOp

added theorem CategoryTheory.Limits.preservesColimit_of_op

added theorem CategoryTheory.Limits.preservesColimit_of_rightOp

added theorem CategoryTheory.Limits.preservesColimit_of_unop

added theorem CategoryTheory.Limits.preservesColimit_op

added theorem CategoryTheory.Limits.preservesColimit_rightOp

added theorem CategoryTheory.Limits.preservesColimit_unop

deleted def CategoryTheory.Limits.preservesColimitsLeftOp

deleted def CategoryTheory.Limits.preservesColimitsOfLeftOp

deleted def CategoryTheory.Limits.preservesColimitsOfOp

deleted def CategoryTheory.Limits.preservesColimitsOfRightOp

deleted def CategoryTheory.Limits.preservesColimitsOfShapeLeftOp

deleted def CategoryTheory.Limits.preservesColimitsOfShapeOfLeftOp

deleted def CategoryTheory.Limits.preservesColimitsOfShapeOfOp

deleted def CategoryTheory.Limits.preservesColimitsOfShapeOfRightOp

deleted def CategoryTheory.Limits.preservesColimitsOfShapeOfUnop

deleted def CategoryTheory.Limits.preservesColimitsOfShapeOp

deleted def CategoryTheory.Limits.preservesColimitsOfShapeRightOp

deleted def CategoryTheory.Limits.preservesColimitsOfShapeUnop

added theorem CategoryTheory.Limits.preservesColimitsOfShape_leftOp

added theorem CategoryTheory.Limits.preservesColimitsOfShape_of_leftOp

added theorem CategoryTheory.Limits.preservesColimitsOfShape_of_op

added theorem CategoryTheory.Limits.preservesColimitsOfShape_of_rightOp

added theorem CategoryTheory.Limits.preservesColimitsOfShape_of_unop

added theorem CategoryTheory.Limits.preservesColimitsOfShape_op

added theorem CategoryTheory.Limits.preservesColimitsOfShape_rightOp

added theorem CategoryTheory.Limits.preservesColimitsOfShape_unop

deleted def CategoryTheory.Limits.preservesColimitsOfSizeLeftOp

deleted def CategoryTheory.Limits.preservesColimitsOfSizeOfLeftOp

deleted def CategoryTheory.Limits.preservesColimitsOfSizeOfOp

deleted def CategoryTheory.Limits.preservesColimitsOfSizeOfRightOp

deleted def CategoryTheory.Limits.preservesColimitsOfSizeOfUnop

deleted def CategoryTheory.Limits.preservesColimitsOfSizeOp

deleted def CategoryTheory.Limits.preservesColimitsOfSizeRightOp

deleted def CategoryTheory.Limits.preservesColimitsOfSizeUnop

added theorem CategoryTheory.Limits.preservesColimitsOfSize_leftOp

added theorem CategoryTheory.Limits.preservesColimitsOfSize_of_leftOp

added theorem CategoryTheory.Limits.preservesColimitsOfSize_of_op

added theorem CategoryTheory.Limits.preservesColimitsOfSize_of_rightOp

added theorem CategoryTheory.Limits.preservesColimitsOfSize_of_unop

added theorem CategoryTheory.Limits.preservesColimitsOfSize_op

added theorem CategoryTheory.Limits.preservesColimitsOfSize_rightOp

added theorem CategoryTheory.Limits.preservesColimitsOfSize_unop

deleted def CategoryTheory.Limits.preservesColimitsOfUnop

deleted def CategoryTheory.Limits.preservesColimitsRightOp

deleted def CategoryTheory.Limits.preservesColimitsUnop

added theorem CategoryTheory.Limits.preservesColimits_leftOp

added theorem CategoryTheory.Limits.preservesColimits_of_leftOp

added theorem CategoryTheory.Limits.preservesColimits_of_op

added theorem CategoryTheory.Limits.preservesColimits_of_rightOp

added theorem CategoryTheory.Limits.preservesColimits_of_unop

added theorem CategoryTheory.Limits.preservesColimits_rightOp

added theorem CategoryTheory.Limits.preservesColimits_unop

deleted def CategoryTheory.Limits.preservesFiniteColimitsLeftOp

deleted def CategoryTheory.Limits.preservesFiniteColimitsOfLeftOp

deleted def CategoryTheory.Limits.preservesFiniteColimitsOfOp

deleted def CategoryTheory.Limits.preservesFiniteColimitsOfRightOp

deleted def CategoryTheory.Limits.preservesFiniteColimitsOfUnop

deleted def CategoryTheory.Limits.preservesFiniteColimitsOp

deleted def CategoryTheory.Limits.preservesFiniteColimitsRightOp

deleted def CategoryTheory.Limits.preservesFiniteColimitsUnop

added theorem CategoryTheory.Limits.preservesFiniteColimits_leftOp

added theorem CategoryTheory.Limits.preservesFiniteColimits_of_leftOp

added theorem CategoryTheory.Limits.preservesFiniteColimits_of_op

added theorem CategoryTheory.Limits.preservesFiniteColimits_of_rightOp

added theorem CategoryTheory.Limits.preservesFiniteColimits_of_unop

added theorem CategoryTheory.Limits.preservesFiniteColimits_op

added theorem CategoryTheory.Limits.preservesFiniteColimits_rightOp

added theorem CategoryTheory.Limits.preservesFiniteColimits_unop

deleted def CategoryTheory.Limits.preservesFiniteCoproductsLeftOp

deleted def CategoryTheory.Limits.preservesFiniteCoproductsOp

deleted def CategoryTheory.Limits.preservesFiniteCoproductsRightOp

deleted def CategoryTheory.Limits.preservesFiniteCoproductsUnop

added theorem CategoryTheory.Limits.preservesFiniteCoproducts_leftOp

added theorem CategoryTheory.Limits.preservesFiniteCoproducts_op

added theorem CategoryTheory.Limits.preservesFiniteCoproducts_rightOp

added theorem CategoryTheory.Limits.preservesFiniteCoproducts_unop

deleted def CategoryTheory.Limits.preservesFiniteLimitsLeftOp

deleted def CategoryTheory.Limits.preservesFiniteLimitsOfLeftOp

deleted def CategoryTheory.Limits.preservesFiniteLimitsOfOp

deleted def CategoryTheory.Limits.preservesFiniteLimitsOfRightOp

deleted def CategoryTheory.Limits.preservesFiniteLimitsOfUnop

deleted def CategoryTheory.Limits.preservesFiniteLimitsOp

deleted def CategoryTheory.Limits.preservesFiniteLimitsRightOp

deleted def CategoryTheory.Limits.preservesFiniteLimitsUnop

added theorem CategoryTheory.Limits.preservesFiniteLimits_leftOp

added theorem CategoryTheory.Limits.preservesFiniteLimits_of_leftOp

added theorem CategoryTheory.Limits.preservesFiniteLimits_of_op

added theorem CategoryTheory.Limits.preservesFiniteLimits_of_rightOp

added theorem CategoryTheory.Limits.preservesFiniteLimits_of_unop

added theorem CategoryTheory.Limits.preservesFiniteLimits_op

added theorem CategoryTheory.Limits.preservesFiniteLimits_rightOp

added theorem CategoryTheory.Limits.preservesFiniteLimits_unop

deleted def CategoryTheory.Limits.preservesFiniteProductsLeftOp

deleted def CategoryTheory.Limits.preservesFiniteProductsOp

deleted def CategoryTheory.Limits.preservesFiniteProductsRightOp

deleted def CategoryTheory.Limits.preservesFiniteProductsUnop

added theorem CategoryTheory.Limits.preservesFiniteProducts_leftOp

added theorem CategoryTheory.Limits.preservesFiniteProducts_op

added theorem CategoryTheory.Limits.preservesFiniteProducts_rightOp

added theorem CategoryTheory.Limits.preservesFiniteProducts_unop

deleted def CategoryTheory.Limits.preservesLimitLeftOp

deleted def CategoryTheory.Limits.preservesLimitOfLeftOp

deleted def CategoryTheory.Limits.preservesLimitOfOp

deleted def CategoryTheory.Limits.preservesLimitOfRightOp

deleted def CategoryTheory.Limits.preservesLimitOfUnop

deleted def CategoryTheory.Limits.preservesLimitOp

deleted def CategoryTheory.Limits.preservesLimitRightOp

deleted def CategoryTheory.Limits.preservesLimitUnop

added theorem CategoryTheory.Limits.preservesLimit_leftOp

added theorem CategoryTheory.Limits.preservesLimit_of_leftOp

added theorem CategoryTheory.Limits.preservesLimit_of_op

added theorem CategoryTheory.Limits.preservesLimit_of_rightOp

added theorem CategoryTheory.Limits.preservesLimit_of_unop

added theorem CategoryTheory.Limits.preservesLimit_op

added theorem CategoryTheory.Limits.preservesLimit_rightOp

added theorem CategoryTheory.Limits.preservesLimit_unop

deleted def CategoryTheory.Limits.preservesLimitsLeftOp

deleted def CategoryTheory.Limits.preservesLimitsOfLeftOp

deleted def CategoryTheory.Limits.preservesLimitsOfOp

deleted def CategoryTheory.Limits.preservesLimitsOfRightOp

deleted def CategoryTheory.Limits.preservesLimitsOfShapeLeftOp

deleted def CategoryTheory.Limits.preservesLimitsOfShapeOfLeftOp

deleted def CategoryTheory.Limits.preservesLimitsOfShapeOfOp

deleted def CategoryTheory.Limits.preservesLimitsOfShapeOfRightOp

deleted def CategoryTheory.Limits.preservesLimitsOfShapeOfUnop

deleted def CategoryTheory.Limits.preservesLimitsOfShapeOp

deleted def CategoryTheory.Limits.preservesLimitsOfShapeRightOp

deleted def CategoryTheory.Limits.preservesLimitsOfShapeUnop

added theorem CategoryTheory.Limits.preservesLimitsOfShape_leftOp

added theorem CategoryTheory.Limits.preservesLimitsOfShape_of_leftOp

added theorem CategoryTheory.Limits.preservesLimitsOfShape_of_op

added theorem CategoryTheory.Limits.preservesLimitsOfShape_of_rightOp

added theorem CategoryTheory.Limits.preservesLimitsOfShape_of_unop

added theorem CategoryTheory.Limits.preservesLimitsOfShape_op

added theorem CategoryTheory.Limits.preservesLimitsOfShape_rightOp

added theorem CategoryTheory.Limits.preservesLimitsOfShape_unop

deleted def CategoryTheory.Limits.preservesLimitsOfSizeLeftOp

deleted def CategoryTheory.Limits.preservesLimitsOfSizeOfLeftOp

deleted def CategoryTheory.Limits.preservesLimitsOfSizeOfOp

deleted def CategoryTheory.Limits.preservesLimitsOfSizeOfRightOp

deleted def CategoryTheory.Limits.preservesLimitsOfSizeOfUnop

deleted def CategoryTheory.Limits.preservesLimitsOfSizeOp

deleted def CategoryTheory.Limits.preservesLimitsOfSizeRightOp

deleted def CategoryTheory.Limits.preservesLimitsOfSizeUnop

added theorem CategoryTheory.Limits.preservesLimitsOfSize_leftOp

added theorem CategoryTheory.Limits.preservesLimitsOfSize_of_leftOp

added theorem CategoryTheory.Limits.preservesLimitsOfSize_of_op

added theorem CategoryTheory.Limits.preservesLimitsOfSize_of_rightOp

added theorem CategoryTheory.Limits.preservesLimitsOfSize_of_unop

added theorem CategoryTheory.Limits.preservesLimitsOfSize_op

added theorem CategoryTheory.Limits.preservesLimitsOfSize_rightOp

added theorem CategoryTheory.Limits.preservesLimitsOfSize_unop

deleted def CategoryTheory.Limits.preservesLimitsOfUnop

deleted def CategoryTheory.Limits.preservesLimitsOp

deleted def CategoryTheory.Limits.preservesLimitsRightOp

deleted def CategoryTheory.Limits.preservesLimitsUnop

added theorem CategoryTheory.Limits.preservesLimits_leftOp

added theorem CategoryTheory.Limits.preservesLimits_of_leftOp

added theorem CategoryTheory.Limits.preservesLimits_of_op

added theorem CategoryTheory.Limits.preservesLimits_of_rightOp

added theorem CategoryTheory.Limits.preservesLimits_of_unop

added theorem CategoryTheory.Limits.preservesLimits_op

added theorem CategoryTheory.Limits.preservesLimits_rightOp

added theorem CategoryTheory.Limits.preservesLimits_unop

Modified Mathlib/CategoryTheory/Limits/Preserves/Presheaf.lean

added theorem CategoryTheory.Limits.preservesFiniteLimits_of_isFiltered_costructuredArrow_yoneda

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/BinaryProducts.lean

deleted def CategoryTheory.Limits.PreservesColimitPair.ofIsoCoprodComparison

added theorem CategoryTheory.Limits.PreservesColimitPair.of_iso_coprod_comparison

deleted def CategoryTheory.Limits.PreservesLimitPair.ofIsoProdComparison

added theorem CategoryTheory.Limits.PreservesLimitPair.of_iso_prod_comparison

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/Biproducts.lean

deleted def CategoryTheory.Limits.preservesBinaryBiproductOfPreservesBiproduct

added theorem CategoryTheory.Limits.preservesBinaryBiproduct_of_preservesBiproduct

deleted def CategoryTheory.Limits.preservesBinaryBiproductsOfPreservesBiproducts

added theorem CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBiproducts

deleted def CategoryTheory.Limits.preservesBiproductsShrink

added theorem CategoryTheory.Limits.preservesBiproducts_shrink

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean

deleted def CategoryTheory.Limits.PreservesEqualizer.ofIsoComparison

added theorem CategoryTheory.Limits.PreservesEqualizer.of_iso_comparison

deleted def CategoryTheory.Limits.ofIsoComparison

added theorem CategoryTheory.Limits.of_iso_comparison

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/Kernels.lean

deleted def CategoryTheory.Limits.PreservesCokernel.ofIsoComparison

added theorem CategoryTheory.Limits.PreservesCokernel.of_iso_comparison

deleted def CategoryTheory.Limits.PreservesKernel.ofIsoComparison

added theorem CategoryTheory.Limits.PreservesKernel.of_iso_comparison

added theorem CategoryTheory.Limits.preservesCokernel_zero'

added theorem CategoryTheory.Limits.preservesKernel_zero'

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/Products.lean

deleted def CategoryTheory.Limits.PreservesCoproduct.ofIsoComparison

added theorem CategoryTheory.Limits.PreservesCoproduct.of_iso_comparison

deleted def CategoryTheory.Limits.PreservesProduct.ofIsoComparison

added theorem CategoryTheory.Limits.PreservesProduct.of_iso_comparison

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean

deleted def CategoryTheory.Limits.PreservesPullback.ofIsoComparison

added theorem CategoryTheory.Limits.PreservesPullback.of_iso_comparison

deleted def CategoryTheory.Limits.PreservesPushout.ofIsoComparison

added theorem CategoryTheory.Limits.PreservesPushout.of_iso_comparison

deleted def CategoryTheory.Limits.preservesPullbackSymmetry

added theorem CategoryTheory.Limits.preservesPullback_symmetry

deleted def CategoryTheory.Limits.preservesPushoutSymmetry

added theorem CategoryTheory.Limits.preservesPushout_symmetry

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.lean

deleted def CategoryTheory.Limits.PreservesInitial.ofIsoComparison

added theorem CategoryTheory.Limits.PreservesInitial.of_iso_comparison

deleted def CategoryTheory.Limits.PreservesTerminal.ofIsoComparison

added theorem CategoryTheory.Limits.PreservesTerminal.of_iso_comparison

deleted def CategoryTheory.Limits.preservesColimitsOfShapePemptyOfPreservesInitial

added theorem CategoryTheory.Limits.preservesColimitsOfShape_pempty_of_preservesInitial

deleted def CategoryTheory.Limits.preservesInitialOfIsIso

deleted def CategoryTheory.Limits.preservesInitialOfIso

added theorem CategoryTheory.Limits.preservesInitial_of_isIso

added theorem CategoryTheory.Limits.preservesInitial_of_iso

deleted def CategoryTheory.Limits.preservesLimitsOfShapePemptyOfPreservesTerminal

added theorem CategoryTheory.Limits.preservesLimitsOfShape_pempty_of_preservesTerminal

deleted def CategoryTheory.Limits.preservesTerminalOfIsIso

deleted def CategoryTheory.Limits.preservesTerminalOfIso

added theorem CategoryTheory.Limits.preservesTerminal_of_isIso

added theorem CategoryTheory.Limits.preservesTerminal_of_iso

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean

deleted def CategoryTheory.Functor.preservesColimitsOfShapeOfIsZero

added theorem CategoryTheory.Functor.preservesColimitsOfShape_of_isZero

deleted def CategoryTheory.Functor.preservesColimitsOfSizeOfIsZero

added theorem CategoryTheory.Functor.preservesColimitsOfSize_of_isZero

deleted def CategoryTheory.Functor.preservesInitialObjectOfPreservesZeroMorphisms

added theorem CategoryTheory.Functor.preservesInitialObject_of_preservesZeroMorphisms

deleted def CategoryTheory.Functor.preservesLimitsOfShapeOfIsZero

added theorem CategoryTheory.Functor.preservesLimitsOfShape_of_isZero

deleted def CategoryTheory.Functor.preservesLimitsOfSizeOfIsZero

added theorem CategoryTheory.Functor.preservesLimitsOfSize_of_isZero

deleted def CategoryTheory.Functor.preservesTerminalObjectOfPreservesZeroMorphisms

added theorem CategoryTheory.Functor.preservesTerminalObject_of_preservesZeroMorphisms

Modified Mathlib/CategoryTheory/Limits/Preserves/Ulift.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/Yoneda.lean

Modified Mathlib/CategoryTheory/Limits/Presheaf.lean

added theorem CategoryTheory.Presheaf.preservesColimitsOfSize_of_isLeftKanExtension

Modified Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Basic.lean

Modified Mathlib/CategoryTheory/Limits/VanKampen.lean

Modified Mathlib/CategoryTheory/Limits/Yoneda.lean

Modified Mathlib/CategoryTheory/Localization/FiniteProducts.lean

added theorem CategoryTheory.Localization.preservesFiniteProducts

added theorem CategoryTheory.Localization.preservesProductsOfShape

Modified Mathlib/CategoryTheory/Monad/Comonadicity.lean

Modified Mathlib/CategoryTheory/Monad/Limits.lean

deleted def CategoryTheory.Comonad.ForgetCreatesLimits'.conePoint

deleted def CategoryTheory.Comonad.ForgetCreatesLimits'.liftedCone

deleted def CategoryTheory.Comonad.ForgetCreatesLimits'.liftedConeIsLimit

deleted def CategoryTheory.Monad.ForgetCreatesColimits.coconePoint

deleted def CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone

deleted def CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconeIsColimit

added theorem CategoryTheory.leftAdjoint_preservesTerminal_of_reflective

added theorem CategoryTheory.rightAdjoint_preservesInitial_of_coreflective

Modified Mathlib/CategoryTheory/Monad/Monadicity.lean

Modified Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean

Modified Mathlib/CategoryTheory/Monoidal/Preadditive.lean

Modified Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean

Modified Mathlib/CategoryTheory/Preadditive/Biproducts.lean

deleted def CategoryTheory.Limits.preservesBinaryBiproductOfEpiBiprodComparison'

deleted def CategoryTheory.Limits.preservesBinaryBiproductOfMonoBiprodComparison

deleted def CategoryTheory.Limits.preservesBinaryBiproductOfPreservesBinaryCoproduct

deleted def CategoryTheory.Limits.preservesBinaryBiproductOfPreservesBinaryProduct

added theorem CategoryTheory.Limits.preservesBinaryBiproduct_of_epi_biprodComparison'

added theorem CategoryTheory.Limits.preservesBinaryBiproduct_of_mono_biprodComparison

added theorem CategoryTheory.Limits.preservesBinaryBiproduct_of_preservesBinaryCoproduct

added theorem CategoryTheory.Limits.preservesBinaryBiproduct_of_preservesBinaryProduct

deleted def CategoryTheory.Limits.preservesBinaryBiproductsOfPreservesBinaryCoproducts

deleted def CategoryTheory.Limits.preservesBinaryBiproductsOfPreservesBinaryProducts

added theorem CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBinaryCoproducts

added theorem CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBinaryProducts

deleted def CategoryTheory.Limits.preservesBinaryCoproductOfPreservesBinaryBiproduct

added theorem CategoryTheory.Limits.preservesBinaryCoproduct_of_preservesBinaryBiproduct

deleted def CategoryTheory.Limits.preservesBinaryCoproductsOfPreservesBinaryBiproducts

added theorem CategoryTheory.Limits.preservesBinaryCoproducts_of_preservesBinaryBiproducts

deleted def CategoryTheory.Limits.preservesBinaryProductOfPreservesBinaryBiproduct

added theorem CategoryTheory.Limits.preservesBinaryProduct_of_preservesBinaryBiproduct

deleted def CategoryTheory.Limits.preservesBinaryProductsOfPreservesBinaryBiproducts

added theorem CategoryTheory.Limits.preservesBinaryProducts_of_preservesBinaryBiproducts

deleted def CategoryTheory.Limits.preservesBiproductOfEpiBiproductComparison'

deleted def CategoryTheory.Limits.preservesBiproductOfMonoBiproductComparison

deleted def CategoryTheory.Limits.preservesBiproductOfPreservesCoproduct

deleted def CategoryTheory.Limits.preservesBiproductOfPreservesProduct

added theorem CategoryTheory.Limits.preservesBiproduct_of_epi_biproductComparison'

added theorem CategoryTheory.Limits.preservesBiproduct_of_mono_biproductComparison

added theorem CategoryTheory.Limits.preservesBiproduct_of_preservesCoproduct

added theorem CategoryTheory.Limits.preservesBiproduct_of_preservesProduct

deleted def CategoryTheory.Limits.preservesBiproductsOfShapeOfPreservesCoproductsOfShape

deleted def CategoryTheory.Limits.preservesBiproductsOfShapeOfPreservesProductsOfShape

added theorem CategoryTheory.Limits.preservesBiproductsOfShape_of_preservesCoproductsOfShape

added theorem CategoryTheory.Limits.preservesBiproductsOfShape_of_preservesProductsOfShape

deleted def CategoryTheory.Limits.preservesCoproductOfPreservesBiproduct

added theorem CategoryTheory.Limits.preservesCoproduct_of_preservesBiproduct

deleted def CategoryTheory.Limits.preservesCoproductsOfShapeOfPreservesBiproductsOfShape

added theorem CategoryTheory.Limits.preservesCoproductsOfShape_of_preservesBiproductsOfShape

deleted def CategoryTheory.Limits.preservesProductOfPreservesBiproduct

added theorem CategoryTheory.Limits.preservesProduct_of_preservesBiproduct

deleted def CategoryTheory.Limits.preservesProductsOfShapeOfPreservesBiproductsOfShape

added theorem CategoryTheory.Limits.preservesProductsOfShape_of_preservesBiproductsOfShape

Modified Mathlib/CategoryTheory/Preadditive/Injective.lean

Modified Mathlib/CategoryTheory/Preadditive/LeftExact.lean

deleted def CategoryTheory.Functor.preservesBinaryCoproductsOfPreservesCokernels

added theorem CategoryTheory.Functor.preservesBinaryCoproducts_of_preservesCokernels

deleted def CategoryTheory.Functor.preservesBinaryProductOfPreservesKernels

added theorem CategoryTheory.Functor.preservesBinaryProduct_of_preservesKernels

deleted def CategoryTheory.Functor.preservesBinaryProductsOfPreservesKernels

added theorem CategoryTheory.Functor.preservesBinaryProducts_of_preservesKernels

deleted def CategoryTheory.Functor.preservesCoequalizerOfPreservesCokernels

added theorem CategoryTheory.Functor.preservesCoequalizer_of_preservesCokernels

deleted def CategoryTheory.Functor.preservesCoequalizersOfPreservesCokernels

added theorem CategoryTheory.Functor.preservesCoequalizers_of_preservesCokernels

deleted def CategoryTheory.Functor.preservesCoproductOfPreservesCokernels

added theorem CategoryTheory.Functor.preservesCoproduct_of_preservesCokernels

deleted def CategoryTheory.Functor.preservesEqualizerOfPreservesKernels

added theorem CategoryTheory.Functor.preservesEqualizer_of_preservesKernels

deleted def CategoryTheory.Functor.preservesEqualizersOfPreservesKernels

added theorem CategoryTheory.Functor.preservesEqualizers_of_preservesKernels

deleted def CategoryTheory.Functor.preservesFiniteColimitsOfPreservesCokernels

added theorem CategoryTheory.Functor.preservesFiniteColimits_of_preservesCokernels

deleted def CategoryTheory.Functor.preservesFiniteLimitsOfPreservesKernels

added theorem CategoryTheory.Functor.preservesFiniteLimits_of_preservesKernels

Modified Mathlib/CategoryTheory/Preadditive/Projective.lean

Modified Mathlib/CategoryTheory/Preadditive/Yoneda/Limits.lean

Modified Mathlib/CategoryTheory/Sites/Abelian.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/ExtensiveSheaves.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/LocallySurjective.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean

Modified Mathlib/CategoryTheory/Sites/Equivalence.lean

Modified Mathlib/CategoryTheory/Sites/LeftExact.lean

added def CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux

added theorem CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux_fac

Modified Mathlib/CategoryTheory/Sites/Preserves.lean

deleted def CategoryTheory.Presieve.preservesProductOfIsSheafFor

added theorem CategoryTheory.Presieve.preservesProduct_of_isSheafFor

deleted def CategoryTheory.Presieve.preservesTerminalOfIsSheafForEmpty

added theorem CategoryTheory.Presieve.preservesTerminal_of_isSheaf_for_empty

Modified Mathlib/CategoryTheory/Sites/Pullback.lean

Modified Mathlib/CategoryTheory/Sites/Sheaf.lean

Modified Mathlib/CategoryTheory/Sites/Sheafification.lean

Modified Mathlib/CategoryTheory/Triangulated/Functor.lean

Modified Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean

Modified Mathlib/Condensed/Discrete/Characterization.lean

Modified Mathlib/Condensed/Discrete/Colimit.lean

Modified Mathlib/Condensed/Explicit.lean

Modified Mathlib/Condensed/Light/Explicit.lean

Modified Mathlib/Condensed/TopComparison.lean

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

Modified Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean

Modified Mathlib/Geometry/RingedSpace/SheafedSpace.lean

Modified Mathlib/RepresentationTheory/Action/Basic.lean

Modified Mathlib/RepresentationTheory/Action/Limits.lean

added theorem Action.preservesColimit_of_preserves

added theorem Action.preservesColimitsOfShape_of_preserves

added theorem Action.preservesColimitsOfSize_of_preserves

added theorem Action.preservesLimit_of_preserves

added theorem Action.preservesLimitsOfShape_of_preserves

added theorem Action.preservesLimitsOfSize_of_preserves

Modified Mathlib/RepresentationTheory/Rep.lean

Modified Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean

Modified Mathlib/Topology/Category/CompHausLike/Limits.lean

Modified Mathlib/Topology/Category/LightProfinite/Basic.lean

Modified Mathlib/Topology/Category/Profinite/Basic.lean

Modified Mathlib/Topology/Category/Stonean/Adjunctions.lean

Modified Mathlib/Topology/Category/TopCat/Limits/Basic.lean

Modified Mathlib/Topology/Category/TopCat/Yoneda.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean