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₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {W : CategoryTheory.MorphismProperty C} [L.IsLocalization W] {J : Type} [CategoryTheory.Limits.HasProductsOfShape J C] (hW : W.IsStableUnderProductsOfShape J) : (W.functorCategory (CategoryTheory.Discrete J)).IsInvertedBy (CategoryTheory.Limits.lim.comp L)

@[reducible, inline]

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} [L.IsLocalization W] {J : Type} [CategoryTheory.Limits.HasProductsOfShape J C] (hW : W.IsStableUnderProductsOfShape J) [W.ContainsIdentities] [Finite 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.

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} [L.IsLocalization W] {J : Type} [CategoryTheory.Limits.HasProductsOfShape J C] (hW : W.IsStableUnderProductsOfShape J) [W.ContainsIdentities] [Finite J] : ((CategoryTheory.whiskeringRight (CategoryTheory.Discrete J) C D).obj L).comp (CategoryTheory.Localization.HasProductsOfShapeAux.limitFunctor L hW) ≅ CategoryTheory.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₂} [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).obj L) (CategoryTheory.Functor.const (CategoryTheory.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₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {W : CategoryTheory.MorphismProperty C} [L.IsLocalization W] {J : Type} [CategoryTheory.Limits.HasProductsOfShape J C] (hW : W.IsStableUnderProductsOfShape J) [W.ContainsIdentities] [Finite J] : CategoryTheory.CatCommSq CategoryTheory.Limits.lim ((CategoryTheory.whiskeringRight (CategoryTheory.Discrete J) C D).obj L) L (CategoryTheory.Localization.HasProductsOfShapeAux.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₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {W : CategoryTheory.MorphismProperty C} [L.IsLocalization W] {J : Type} [CategoryTheory.Limits.HasProductsOfShape J C] (hW : W.IsStableUnderProductsOfShape J) [W.ContainsIdentities] [Finite 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.

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} [L.IsLocalization W] {J : Type} [CategoryTheory.Limits.HasProductsOfShape J C] (hW : W.IsStableUnderProductsOfShape J) [W.ContainsIdentities] [Finite J] (F : CategoryTheory.Functor (CategoryTheory.Discrete J) C) : (CategoryTheory.Localization.HasProductsOfShapeAux.adj L hW).counit.app (F.comp L) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const (CategoryTheory.Discrete J)).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.obj F)) (CategoryTheory.whiskerRight (CategoryTheory.Limits.constLimAdj.counit.app F) L))

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} [L.IsLocalization W] {J : Type} [CategoryTheory.Limits.HasProductsOfShape J C] (hW : W.IsStableUnderProductsOfShape J) [W.ContainsIdentities] [Finite 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.

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) [L.IsLocalization W] [W.ContainsIdentities] (J : Type) [Finite J] [CategoryTheory.Limits.HasProductsOfShape J C] (hW : W.IsStableUnderProductsOfShape J) : CategoryTheory.Limits.HasProductsOfShape J D

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) [L.IsLocalization W] [W.ContainsIdentities] (J : Type) [Finite J] [CategoryTheory.Limits.HasProductsOfShape J C] (hW : W.IsStableUnderProductsOfShape 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

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

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) [L.IsLocalization W] [W.ContainsIdentities] [CategoryTheory.Limits.HasFiniteProducts C] [W.IsStableUnderFiniteProducts] : CategoryTheory.Limits.HasFiniteProducts D

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) [L.IsLocalization W] [W.ContainsIdentities] [CategoryTheory.Limits.HasFiniteProducts C] [W.IsStableUnderFiniteProducts] : 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

• CategoryTheory.Localization.preservesFiniteProducts L W = { preserves := fun (J : Type) (x : Fintype J) => CategoryTheory.Localization.preservesProductsOfShape L W J ⋯ }

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

Equations

• ⋯ = ⋯

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

Equations

• CategoryTheory.Localization.instPreservesFiniteProductsLocalizationQ W = CategoryTheory.Localization.preservesFiniteProducts W.Q W

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

Equations

• ⋯ = ⋯

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

Equations

• CategoryTheory.Localization.instPreservesFiniteProductsLocalization'Q' W = CategoryTheory.Localization.preservesFiniteProducts W.Q' W