Commit 2024-02-08 16:52 00c3cd40

View on Github →

feat(CategoryTheory): prerequisites for the existence of finite products in localized categories (#9702) This PR contains various prerequisites in order to show that under suitable assumptions, a localized category of a category that has finite products also has finite products:

the equivalence of categories (J → C) ≌ (Discrete J ⥤ C)
more API for the existence of limits as a consequence of a right adjoint to the constant functor C ⥤ (J ⥤ C).
the typeclass MorphismProperty.IsStableUnderFiniteProducts

Estimated changes

Modified Mathlib/CategoryTheory/Adjunction/Basic.lean

modified theorem CategoryTheory.Adjunction.right_triangle_components

Modified Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean

Modified Mathlib/CategoryTheory/Closed/Monoidal.lean

Modified Mathlib/CategoryTheory/DiscreteCategory.lean

added def CategoryTheory.piEquivalenceFunctorDiscrete

Modified Mathlib/CategoryTheory/Functor/Const.lean

added def CategoryTheory.Functor.compConstIso

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

added def CategoryTheory.Limits.isLimitConeOfAdj

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

added def CategoryTheory.Limits.Pi.cone

added def CategoryTheory.Limits.Pi.isoLimit

added theorem CategoryTheory.Limits.Pi.isoLimit_hom_π

added theorem CategoryTheory.Limits.Pi.isoLimit_inv_π

added def CategoryTheory.Limits.productIsProduct'

Modified Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean

Modified Mathlib/CategoryTheory/Limits/VanKampen.lean

Modified Mathlib/CategoryTheory/MorphismProperty.lean

added theorem CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape.lim_map

added def CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape

added theorem CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape.mk

added def CategoryTheory.MorphismProperty.functorCategory

added theorem CategoryTheory.MorphismProperty.isStableUnderProductsOfShape_of_isStableUnderFiniteProducts