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] (hW : 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] (hW : 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] (hW : W.IsStableUnderProductsOfShape J) [W.ContainsIdentities] [Finite J] : ((whiskeringRight (Discrete J) C D).obj L).comp (limitFunctor L hW) ≅ Limits.lim.comp L

The functor limitFunctor L hW 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 ((whiskeringRight (Discrete J) C D).obj L) (Functor.const (Discrete J))

Equations

• CategoryTheory.Localization.HasProductsOfShapeAux.instCatCommSqFunctorDiscreteConstObjWhiskeringRight L = { 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] (hW : W.IsStableUnderProductsOfShape J) [W.ContainsIdentities] [Finite J] : CatCommSq Limits.lim ((whiskeringRight (Discrete J) C D).obj L) L (limitFunctor L hW)

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] (hW : W.IsStableUnderProductsOfShape J) [W.ContainsIdentities] [Finite J] : Functor.const (Discrete J) ⊣ 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.

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] (hW : W.IsStableUnderProductsOfShape J) [W.ContainsIdentities] [Finite J] (F : Functor (Discrete J) C) : (adj L hW).counit.app (F.comp L) = CategoryStruct.comp ((Functor.const (Discrete J)).map ((compLimitFunctorIso L hW).hom.app F)) (CategoryStruct.comp ((Functor.compConstIso (Discrete J) L).hom.app (Limits.lim.obj F)) (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] (hW : 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] (hW : 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] (hW : 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'