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.

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Localization.HasProductsOfShapeAux.limitFunctor {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] (J : Type) [Limits.HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J] [W.ContainsIdentities] [Finite J] : Functor (Functor (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.

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

The functor limitFunctor L W J is induced by lim ⋙ L.

Equations

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

instance CategoryTheory.Localization.HasProductsOfShapeAux.instCatCommSqFunctorDiscreteConstObjWhiskeringRight {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (L : Functor C D) (J : Type) : CatCommSq (Functor.const (Discrete J)) L ((Functor.whiskeringRight (Discrete J) C D).obj L) (Functor.const (Discrete J))

Equations

• CategoryTheory.Localization.HasProductsOfShapeAux.instCatCommSqFunctorDiscreteConstObjWhiskeringRight L J = { iso := (CategoryTheory.Functor.compConstIso (CategoryTheory.Discrete J) L).symm }

noncomputable instance CategoryTheory.Localization.HasProductsOfShapeAux.instCatCommSqFunctorDiscreteLimObjWhiskeringRightLimitFunctor {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] (J : Type) [Limits.HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J] [W.ContainsIdentities] [Finite J] : CatCommSq Limits.lim ((Functor.whiskeringRight (Discrete J) C D).obj L) L (limitFunctor L W J)

Equations

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

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

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

Equations

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

theorem CategoryTheory.Localization.HasProductsOfShapeAux.adj_counit_app {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] (J : Type) [Limits.HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J] [W.ContainsIdentities] [Finite J] (F : Functor (Discrete J) C) : (adj L W J).counit.app (F.comp L) = CategoryStruct.comp ((Functor.const (Discrete J)).map ((compLimitFunctorIso L W J).hom.app F)) (CategoryStruct.comp ((Functor.compConstIso (Discrete J) L).hom.app (Limits.lim.obj F)) (Functor.whiskerRight (Limits.constLimAdj.counit.app F) L))

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

Auxiliary definition for Localization.preservesProductsOfShape.

Equations

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

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

theorem CategoryTheory.Localization.preservesProductsOfShape {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.ContainsIdentities] (J : Type) [Finite J] [Limits.HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J] : Limits.PreservesLimitsOfShape (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.

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

theorem CategoryTheory.Localization.preservesFiniteProducts {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.ContainsIdentities] [Limits.HasFiniteProducts C] [W.IsStableUnderFiniteProducts] : 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.

instance CategoryTheory.Localization.instHasFiniteProductsLocalization {C : Type u₁} [Category.{v₁, u₁} C] (W : MorphismProperty C) [W.ContainsIdentities] [Limits.HasFiniteProducts C] [W.IsStableUnderFiniteProducts] : Limits.HasFiniteProducts W.Localization

instance CategoryTheory.Localization.instPreservesFiniteProductsLocalizationQ {C : Type u₁} [Category.{v₁, u₁} C] (W : MorphismProperty C) [W.ContainsIdentities] [Limits.HasFiniteProducts C] [W.IsStableUnderFiniteProducts] : Limits.PreservesFiniteProducts W.Q

instance CategoryTheory.Localization.instHasFiniteProductsLocalization' {C : Type u₁} [Category.{v₁, u₁} C] (W : MorphismProperty C) [W.ContainsIdentities] [Limits.HasFiniteProducts C] [W.IsStableUnderFiniteProducts] [W.HasLocalization] : Limits.HasFiniteProducts W.Localization'

instance CategoryTheory.Localization.instPreservesFiniteProductsLocalization'Q' {C : Type u₁} [Category.{v₁, u₁} C] (W : MorphismProperty C) [W.ContainsIdentities] [Limits.HasFiniteProducts C] [W.IsStableUnderFiniteProducts] [W.HasLocalization] : Limits.PreservesFiniteProducts W.Q'