Mathlib.CategoryTheory.Localization.FiniteProducts

The localized category has finite products

In this file, it is shown that if L : C ⥤ D is a localization functor for W : MorphismProperty C and that W is stable under finite products, then D has finite products, and L preserves finite products.

source

theorem CategoryTheory.Localization.HasProductsOfShapeAux.inverts {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {W : CategoryTheory.MorphismProperty C} [CategoryTheory.Functor.IsLocalization L W] {J : Type} [CategoryTheory.Limits.HasProductsOfShape J C] (hW : CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape W J) :

CategoryTheory.MorphismProperty.IsInvertedBy (CategoryTheory.MorphismProperty.functorCategory W (CategoryTheory.Discrete J)) (CategoryTheory.Functor.comp CategoryTheory.Limits.lim L)

source

@[inline, reducible]

noncomputable abbrev CategoryTheory.Localization.HasProductsOfShapeAux.limitFunctor {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {W : CategoryTheory.MorphismProperty C} [CategoryTheory.Functor.IsLocalization L W] [CategoryTheory.MorphismProperty.ContainsIdentities W] {J : Type} [Finite J] [CategoryTheory.Limits.HasProductsOfShape J C] (hW : CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape W J) :

CategoryTheory.Functor (CategoryTheory.Functor (CategoryTheory.Discrete J) D) D

The (candidate) limit functor for the localized category. It is induced by lim ⋙ L : (Discrete J ⥤ C) ⥤ D.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def CategoryTheory.Localization.HasProductsOfShapeAux.compLimitFunctorIso {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {W : CategoryTheory.MorphismProperty C} [CategoryTheory.Functor.IsLocalization L W] [CategoryTheory.MorphismProperty.ContainsIdentities W] {J : Type} [Finite J] [CategoryTheory.Limits.HasProductsOfShape J C] (hW : CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape W J) :

CategoryTheory.Functor.comp ((CategoryTheory.whiskeringRight (CategoryTheory.Discrete J) C D).toPrefunctor.obj L) (CategoryTheory.Localization.HasProductsOfShapeAux.limitFunctor L hW) ≅ CategoryTheory.Functor.comp CategoryTheory.Limits.lim L

The functor limitFunctor L hW is induced by lim ⋙ L.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

instance CategoryTheory.Localization.HasProductsOfShapeAux.instCatCommSqFunctorDiscreteDiscreteCategoryFunctorCategoryCategoryConstObjFunctorToQuiverToCategoryStructCategoryFunctorToQuiverToCategoryStructCategoryToPrefunctorWhiskeringRightConst {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {J : Type} :

CategoryTheory.CatCommSq (CategoryTheory.Functor.const (CategoryTheory.Discrete J)) L ((CategoryTheory.whiskeringRight (CategoryTheory.Discrete J) C D).toPrefunctor.obj L) (CategoryTheory.Functor.const (CategoryTheory.Discrete J))

Equations

One or more equations did not get rendered due to their size.

source

noncomputable instance CategoryTheory.Localization.HasProductsOfShapeAux.instCatCommSqFunctorDiscreteDiscreteCategoryFunctorCategoryCategoryLimObjFunctorToQuiverToCategoryStructCategoryFunctorToQuiverToCategoryStructCategoryToPrefunctorWhiskeringRightLimitFunctor {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {W : CategoryTheory.MorphismProperty C} [CategoryTheory.Functor.IsLocalization L W] [CategoryTheory.MorphismProperty.ContainsIdentities W] {J : Type} [Finite J] [CategoryTheory.Limits.HasProductsOfShape J C] (hW : CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape W J) :

CategoryTheory.CatCommSq CategoryTheory.Limits.lim ((CategoryTheory.whiskeringRight (CategoryTheory.Discrete J) C D).toPrefunctor.obj L) L (CategoryTheory.Localization.HasProductsOfShapeAux.limitFunctor L hW)

Equations

One or more equations did not get rendered due to their size.

source

noncomputable def CategoryTheory.Localization.HasProductsOfShapeAux.adj {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {W : CategoryTheory.MorphismProperty C} [CategoryTheory.Functor.IsLocalization L W] [CategoryTheory.MorphismProperty.ContainsIdentities W] {J : Type} [Finite J] [CategoryTheory.Limits.HasProductsOfShape J C] (hW : CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape W J) :

CategoryTheory.Functor.const (CategoryTheory.Discrete J) ⊣ CategoryTheory.Localization.HasProductsOfShapeAux.limitFunctor L hW

The adjunction between the constant functor D ⥤ (Discrete J ⥤ D) and limitFunctor L hW.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem CategoryTheory.Localization.HasProductsOfShapeAux.adj_counit_app {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {W : CategoryTheory.MorphismProperty C} [CategoryTheory.Functor.IsLocalization L W] [CategoryTheory.MorphismProperty.ContainsIdentities W] {J : Type} [Finite J] [CategoryTheory.Limits.HasProductsOfShape J C] (hW : CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape W J) (F : CategoryTheory.Functor (CategoryTheory.Discrete J) C) :

(CategoryTheory.Localization.HasProductsOfShapeAux.adj L hW).counit.app (CategoryTheory.Functor.comp F L) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const (CategoryTheory.Discrete J)).toPrefunctor.map ((CategoryTheory.Localization.HasProductsOfShapeAux.compLimitFunctorIso L hW).hom.app F)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.compConstIso (CategoryTheory.Discrete J) L).hom.app (CategoryTheory.Limits.lim.toPrefunctor.obj F)) (CategoryTheory.whiskerRight (CategoryTheory.Limits.constLimAdj.counit.app F) L))

source

noncomputable def CategoryTheory.Localization.HasProductsOfShapeAux.isLimitMapCone {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {W : CategoryTheory.MorphismProperty C} [CategoryTheory.Functor.IsLocalization L W] [CategoryTheory.MorphismProperty.ContainsIdentities W] {J : Type} [Finite J] [CategoryTheory.Limits.HasProductsOfShape J C] (hW : CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape W J) (F : CategoryTheory.Functor (CategoryTheory.Discrete J) C) :

CategoryTheory.Limits.IsLimit (L.mapCone (CategoryTheory.Limits.limit.cone F))

Auxiliary definition for Localization.preservesProductsOfShape.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem CategoryTheory.Localization.hasProductsOfShape {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [CategoryTheory.Functor.IsLocalization L W] [CategoryTheory.MorphismProperty.ContainsIdentities W] (J : Type) [Finite J] [CategoryTheory.Limits.HasProductsOfShape J C] (hW : CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape W J) :

CategoryTheory.Limits.HasProductsOfShape J D

source

noncomputable def CategoryTheory.Localization.preservesProductsOfShape {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [CategoryTheory.Functor.IsLocalization L W] [CategoryTheory.MorphismProperty.ContainsIdentities W] (J : Type) [Finite J] [CategoryTheory.Limits.HasProductsOfShape J C] (hW : CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape W J) :

CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) L

When C has finite products indexed by J, W : MorphismProperty C contains identities and is stable by products indexed by J, then any localization functor for W preserves finite products indexed by J.

Equations

CategoryTheory.Localization.preservesProductsOfShape L W J hW = CategoryTheory.Limits.PreservesLimitsOfShape.mk

Instances For

source

theorem CategoryTheory.Localization.hasFiniteProducts {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [CategoryTheory.Functor.IsLocalization L W] [CategoryTheory.MorphismProperty.ContainsIdentities W] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.MorphismProperty.IsStableUnderFiniteProducts W] :

CategoryTheory.Limits.HasFiniteProducts D

source

noncomputable def CategoryTheory.Localization.preservesFiniteProducts {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [CategoryTheory.Functor.IsLocalization L W] [CategoryTheory.MorphismProperty.ContainsIdentities W] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.MorphismProperty.IsStableUnderFiniteProducts W] :

CategoryTheory.Limits.PreservesFiniteProducts L

When C has finite products and W : MorphismProperty C contains identities and is stable by finite products, then any localization functor for W preserves finite products.

Equations