Preservation of coproducts from finite and filtered

A functor preserving finite coproducts and Finset-shaped colimits preserves arbitrary coproducts: the coproduct is the filtered colimit of its finite subcoproducts, and the functor preserves every stage and the colimit itself. Mathlib carries the existence half of this construction; the preservation half is supplied here. The consumer is the tensor product on the ind-category, which is exact and preserves filtered colimits, and must be seen to preserve the coend presentations of §3.

instance RS.isIso_sigmaComparison_stage {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {α : Type w} [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasFiniteCoproducts D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteCoproducts G] (f : α → C) (S : Finset (CategoryTheory.Discrete α)) : CategoryTheory.IsIso (CategoryTheory.Limits.sigmaComparison G fun (x : ↥S) => (CategoryTheory.Discrete.functor f).obj ↑x)

The stagewise comparison morphism at a finite stage is invertible for a functor preserving finite coproducts.

theorem RS.stage_ι_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {α : Type w} [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasFiniteCoproducts D] (G : CategoryTheory.Functor C D) (f : α → C) (S : Finset (CategoryTheory.Discrete α)) (x : ↥S) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (y : ↥S) => (CategoryTheory.Discrete.functor fun (z : α) => G.obj (f z)).obj ↑y) x) (CategoryTheory.Limits.sigmaComparison G fun (y : ↥S) => (CategoryTheory.Discrete.functor f).obj ↑y) = G.map (CategoryTheory.Limits.Sigma.ι (fun (y : ↥S) => (CategoryTheory.Discrete.functor f).obj ↑y) x)

The stage-level comparison computation, restated at the exact syntactic form of the Finset diagram's coproduct families.

theorem RS.stage_ι_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {α : Type w} [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasFiniteCoproducts D] (G : CategoryTheory.Functor C D) (f : α → C) (S : Finset (CategoryTheory.Discrete α)) (x : ↥S) {Z : D} (h : G.obj (∐ fun (y : ↥S) => (CategoryTheory.Discrete.functor f).obj ↑y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (y : ↥S) => (CategoryTheory.Discrete.functor fun (z : α) => G.obj (f z)).obj ↑y) x) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.sigmaComparison G fun (y : ↥S) => (CategoryTheory.Discrete.functor f).obj ↑y) h) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Sigma.ι (fun (y : ↥S) => (CategoryTheory.Discrete.functor f).obj ↑y) x)) h

The stage-level comparison computation, restated at the exact syntactic form of the Finset diagram's coproduct families.

noncomputable def RS.liftToFinsetComparison {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {α : Type w} [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasFiniteCoproducts D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteCoproducts G] (f : α → C) : CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj (CategoryTheory.Discrete.functor fun (x : α) => G.obj (f x)) ≅ (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj (CategoryTheory.Discrete.functor f)).comp G

The stagewise coproduct comparisons of a functor preserving finite coproducts, assembled into an isomorphism of Finset diagrams.

Equations

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

theorem RS.preservesCoproduct_of_finite_and_filtered {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {α : Type w} [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasFiniteCoproducts D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteCoproducts G] [CategoryTheory.Limits.HasColimitsOfShape (Finset (CategoryTheory.Discrete α)) C] [CategoryTheory.Limits.HasColimitsOfShape (Finset (CategoryTheory.Discrete α)) D] [CategoryTheory.Limits.PreservesColimitsOfShape (Finset (CategoryTheory.Discrete α)) G] (f : α → C) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) G

Preservation of coproducts from finite and filtered: a functor preserving finite coproducts and Finset-shaped colimits preserves every coproduct indexed by α.

theorem RS.preservesColimitsOfShape_discrete_of_finite_and_filtered {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {α : Type w} [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasFiniteCoproducts D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteCoproducts G] [CategoryTheory.Limits.HasColimitsOfShape (Finset (CategoryTheory.Discrete α)) C] [CategoryTheory.Limits.HasColimitsOfShape (Finset (CategoryTheory.Discrete α)) D] [CategoryTheory.Limits.PreservesColimitsOfShape (Finset (CategoryTheory.Discrete α)) G] : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete α) G

Shape form of the preservation of coproducts from finite and filtered.