Coproducts in a localization

Let L : C ⥤ D be a localization functor for a class W of morphisms with a right calculus of fractions. If C has coproducts of shape ι and W is stable under them, then D has coproducts of shape ι, they are computed in C, and L preserves them. This is the argument that the derived category of an abelian category with exact coproducts has coproducts, run at the level of the localization: a morphism out of L (∐ X) is a right fraction, its restrictions to the summands are right fractions with a common denominator Sigma.map of denominators, and two fractions agreeing on every summand are identified by the Ore condition summand by summand and one more Sigma.map.

Main definitions

• Localization.isColimitCofan: L (∐ X) is a coproduct of the L (X i).

Main results

• Localization.sigma_hom_ext: two morphisms out of L (∐ X) agreeing on every summand are equal.
• Localization.preservesCoproductsOfShape: L preserves coproducts of shape ι.
• Localization.hasCoproductsOfShape: D has coproducts of shape ι.

Implementation notes

The hypotheses are exactly those of the derived category Qh : K(A) ⥤ D(A): the homotopy category has coproducts computed degreewise, quasi-isomorphisms have a right calculus of fractions there, and they are stable under coproducts when A has exact coproducts. Nothing here is about complexes; the instances for D(A) are a later consumer.

Mathlib's Localization.preservesProductsOfShape and hasProductsOfShape (Mathlib/CategoryTheory/Localization/FiniteProducts.lean) need no calculus of fractions but only apply to Finite J: they descend lim along the localization of Discrete J ⥤ C, and Functor.IsLocalization.pi is proved by induction on a finite index type. This file trades a right calculus of fractions for an arbitrary ι. Right fractions, not left: a morphism out of L (∐ X) written as a right fraction has its denominator on the coproduct side, so the ι-many denominators of the legs are absorbed by a single Sigma.map; with left fractions the denominators sit at the target, and a common one for infinitely many legs would need an infinitary Ore condition that a calculus of fractions does not provide.

The two main results are theorems producing instances rather than instances, since W is not determined by L nor L by D; for the universal localization W.Q they are instances, as in Mathlib's finite-products file. The construction internals live in Localization.HasCoproductsOfShapeAux, following Localization.HasProductsOfShapeAux.

References

• Neeman, Triangulated categories, Lemma 3.2.10, the Verdier-quotient form: for a β-localizing subcategory N of T, T/N has the coproducts of fewer than β objects that T has, and the quotient functor preserves them.
• Stacks, Tag 0A5L, Lemma 13.33.5, the derived-category form for countable direct sums under exact countable direct sums; this file removes the countability.

theorem CategoryTheory.Localization.sigma_hom_ext {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasRightCalculusOfFractions] {ι : Type w} [Limits.HasCoproductsOfShape ι C] [W.IsStableUnderCoproductsOfShape ι] {X : ι → C} {Y : C} {ψ ψ' : L.obj (∐ X) ⟶ L.obj Y} (h : ∀ (i : ι), CategoryStruct.comp (L.map (Limits.Sigma.ι X i)) ψ = CategoryStruct.comp (L.map (Limits.Sigma.ι X i)) ψ') : ψ = ψ'

Two morphisms out of L (∐ X) that agree on every summand are equal: written as right fractions with a common denominator t, the Ore condition against each Sigma.ι X i and map_eq_iff_precomp give, summand by summand, morphisms in W equalizing the two numerators, and Sigma.map of those is a morphism in W through which both fractions factor.

noncomputable def CategoryTheory.Localization.HasCoproductsOfShapeAux.cofanFraction {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasRightCalculusOfFractions] {ι : Type w} (X : ι → C) (t : Limits.Cofan fun (i : ι) => L.obj (X i)) (Y : C) (e : L.obj Y ≅ t.pt) (i : ι) : W.RightFraction (X i) Y

The right fraction representing a leg of a cofan under L, against a chosen preimage Y of its vertex.

Equations

• CategoryTheory.Localization.HasCoproductsOfShapeAux.cofanFraction L W X t Y e i = ⋯.choose

theorem CategoryTheory.Localization.HasCoproductsOfShapeAux.cofanFraction_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasRightCalculusOfFractions] {ι : Type w} (X : ι → C) (t : Limits.Cofan fun (i : ι) => L.obj (X i)) (Y : C) (e : L.obj Y ≅ t.pt) (i : ι) : (cofanFraction L W X t Y e i).map L ⋯ = CategoryStruct.comp (t.inj i) e.inv

The defining equation of cofanFraction, the choose_spec of Localization.exists_rightFraction.

instance CategoryTheory.Localization.HasCoproductsOfShapeAux.isIso_map_sigma_map_cofanFraction_s {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasRightCalculusOfFractions] {ι : Type w} [Limits.HasCoproductsOfShape ι C] [W.IsStableUnderCoproductsOfShape ι] (X : ι → C) (t : Limits.Cofan fun (i : ι) => L.obj (X i)) (Y : C) (e : L.obj Y ≅ t.pt) : IsIso (L.map (Limits.Sigma.map fun (i : ι) => (cofanFraction L W X t Y e i).s))

The common denominator of the legs' fractions is inverted by L.

noncomputable def CategoryTheory.Localization.HasCoproductsOfShapeAux.cofanDesc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasRightCalculusOfFractions] {ι : Type w} [Limits.HasCoproductsOfShape ι C] [W.IsStableUnderCoproductsOfShape ι] (X : ι → C) (t : Limits.Cofan fun (i : ι) => L.obj (X i)) (Y : C) (e : L.obj Y ≅ t.pt) : L.obj (∐ X) ⟶ t.pt

The morphism out of L (∐ X) induced by a cofan under L: the common denominator of the legs' fractions, then the numerators assembled by Sigma.desc, then the identification of the vertex.

Equations

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

theorem CategoryTheory.Localization.HasCoproductsOfShapeAux.cofanDesc_fac {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasRightCalculusOfFractions] {ι : Type w} [Limits.HasCoproductsOfShape ι C] [W.IsStableUnderCoproductsOfShape ι] (X : ι → C) (t : Limits.Cofan fun (i : ι) => L.obj (X i)) (Y : C) (e : L.obj Y ≅ t.pt) (i : ι) : CategoryStruct.comp (L.map (Limits.Sigma.ι X i)) (cofanDesc L W X t Y e) = t.inj i

cofanDesc restricts on each summand to the given leg.

noncomputable def CategoryTheory.Localization.isColimitCofan {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasRightCalculusOfFractions] {ι : Type w} [Limits.HasCoproductsOfShape ι C] [W.IsStableUnderCoproductsOfShape ι] (X : ι → C) : Limits.IsColimit (Limits.Cofan.mk (L.obj (∐ X)) fun (i : ι) => L.map (Limits.Sigma.ι X i))

L (∐ X) is a coproduct of the L (X i), with legs L (Sigma.ι X i): the description is cofanDesc against a preimage of the vertex, which exists because L is essentially surjective, and uniqueness is sigma_hom_ext.

Equations

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

theorem CategoryTheory.Localization.preservesCoproductsOfShape {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasRightCalculusOfFractions] (ι : Type w) [Limits.HasCoproductsOfShape ι C] [W.IsStableUnderCoproductsOfShape ι] : Limits.PreservesColimitsOfShape (Discrete ι) L

L preserves coproducts of shape ι: isColimitCofan transported along Discrete.natIsoFunctor. Unlike Mathlib's Localization.preservesProductsOfShape, which needs Finite J and no calculus of fractions, this holds for every ι given a right calculus.

theorem CategoryTheory.Localization.hasCoproductsOfShape {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasRightCalculusOfFractions] (ι : Type w) [Limits.HasCoproductsOfShape ι C] [W.IsStableUnderCoproductsOfShape ι] : Limits.HasCoproductsOfShape ι D

D has coproducts of shape ι: every family is isomorphic to the image of a family in C, whose coproduct L preserves.

instance CategoryTheory.Localization.hasCoproductsOfShapeLocalization {C : Type u₁} [Category.{v₁, u₁} C] (W : MorphismProperty C) [W.HasRightCalculusOfFractions] (ι : Type w) [Limits.HasCoproductsOfShape ι C] [W.IsStableUnderCoproductsOfShape ι] : Limits.HasCoproductsOfShape ι W.Localization

The universal localization has coproducts of shape ι.

instance CategoryTheory.Localization.preservesCoproductsOfShapeQ {C : Type u₁} [Category.{v₁, u₁} C] (W : MorphismProperty C) [W.HasRightCalculusOfFractions] (ι : Type w) [Limits.HasCoproductsOfShape ι C] [W.IsStableUnderCoproductsOfShape ι] : Limits.PreservesColimitsOfShape (Discrete ι) W.Q

The universal localization functor preserves coproducts of shape ι.