Commit 2023-11-28 14:52 2bfea869

View on Github →

feat(CategoryTheory): the localized category of a product category (#8516) This PR develops the API for cartesian products of categories (natural isomorphisms, equivalences, morphism properties) in order to show that under simple assumptions, the localized category of a product of two categories identifies to a product of the localized categories.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Functor/Currying.lean

added theorem CategoryTheory.Functor.curry_obj_injective

added theorem CategoryTheory.Functor.curry_obj_uncurry_obj

added theorem CategoryTheory.Functor.flip_flip

added theorem CategoryTheory.Functor.flip_injective

added theorem CategoryTheory.Functor.uncurry_obj_curry_obj

added theorem CategoryTheory.Functor.uncurry_obj_curry_obj_flip_flip'

added theorem CategoryTheory.Functor.uncurry_obj_curry_obj_flip_flip

added theorem CategoryTheory.Functor.uncurry_obj_injective

Created Mathlib/CategoryTheory/Localization/Prod.lean

added theorem CategoryTheory.Localization.Construction.prodIsLocalization

added theorem CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac

added theorem CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac₁

added theorem CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac₂

added theorem CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_uniq

Modified Mathlib/CategoryTheory/MorphismProperty.lean

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.prod

added def CategoryTheory.MorphismProperty.prod

Modified Mathlib/CategoryTheory/Products/Basic.lean

added def CategoryTheory.Equivalence.prod

added def CategoryTheory.NatIso.prod