Right-exactness of the tensor product on ind-objects

Deligne's 2.2, exactness half: the transported tensor product of Ind C preserves colimits in each variable, and the monoidal structure is preadditive.

For a small monoidal C the file proves, unconditionally:

• RS.indToDay — the monoidal embedding of Ind C into the Day presheaf category Cᵒᵖ ⊛⥤ Type v, with its Functor.Monoidal instance transported from RS.indDayEquivalence;
• RS.tensorLeft_ind_preservesColimitsOfShape and the right-hand and packaged (PreservesFilteredColimits) versions — tensorLeft X and tensorRight X on Ind C preserve all small filtered colimits, for every X : Ind C;
• RS.indOfTensorIso/RS.indOfTensorIsoSymm — the embedding indOf : C ⥤ Ind C is monoidal up to isomorphism, with naturality in each variable (RS.indOfTensorIso_hom_natural_right/_left); this rests on the corepresentability calculus for RS.dayCoyonedaIso (RS.eta_comp_dayCoyonedaIso_hom and the naturality lemmas for RS.dayYonedaIso).

For C additionally preadditive with finite colimits and a preadditive tensor ([Preadditive C] [HasFiniteColimits C] [MonoidalPreadditive C] — Deligne's setting, where C is abelian ℂ-linear with exact tensor):

• RS.isIso_coprodComparison_tensorLeft/_tensorRight — the binary coproduct comparisons of both tensoring functors on Ind C are invertible, by a three-stage filtered descent (RS.isIso_app_of_isIso_indOf) from the embedded case, which is conjugate under indOf to additivity of the tensor of C;
• RS.isZero_tensor_left_ind/_right_ind — tensoring kills zero objects;
• RS.tensorLeft_ind_additive/RS.tensorRight_ind_additive and MonoidalPreadditive (Ind C) — whiskering in Ind C is additive in each variable.

Filtered colimits are the only colimits Ind C possesses for general C; under [HasFiniteColimits C] it is cocomplete, and the finite-coproduct half of general right-exactness follows from the additivity above (see the acceptance tests at the bottom). Preservation of coequalizers demands genuine right-exactness of the tensor of C and is left to a follow-up lane.

The @[reducible] marking on the small coprodDiagram/ coprodCocone/coprodPairFunctor helpers is deliberate: their object fields must reduce at instance transparency for the show-retyped colimit proofs below to be stateable.

noncomputable def RS.indToDay {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor (CategoryTheory.Ind C) (CategoryTheory.MonoidalCategory.DayFunctor Cᵒᵖ (Type v))

The embedding of Ind C into the Day presheaf category: the indization equivalence onto the full monoidal subcategory of ind-objects, followed by the subcategory inclusion.

Equations

• RS.indToDay = (RS.indDayEquivalence C).functor.comp (CategoryTheory.ObjectProperty.ι (RS.IsIndDay C))

@[instance_reducible]

noncomputable instance RS.instMonoidalIndFullSubcategoryDayFunctorOppositeTypeIsIndDayFunctorIndDayEquivalence {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] : (indDayEquivalence C).functor.Monoidal

The forward functor of the indization equivalence is monoidal: the monoidal structure of Ind C is transported across it.

Equations

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

@[instance_reducible]

noncomputable instance RS.instMonoidalIndDayFunctorOppositeTypeIndToDay {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] : indToDay.Monoidal

The embedding into the Day presheaf category is monoidal.

Equations

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

instance RS.instFullIndDayFunctorOppositeTypeIndToDay {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] : indToDay.Full

instance RS.instFaithfulIndDayFunctorOppositeTypeIndToDay {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] : indToDay.Faithful

noncomputable def RS.indToDayCompIso {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] : indToDay ≅ (CategoryTheory.Ind.inclusion C).comp (CategoryTheory.MonoidalCategory.DayFunctor.equiv Cᵒᵖ (Type v)).inverse

The embedding of Ind C into the Day presheaf category is the inclusion into plain presheaves followed by the tautological equivalence with the Day synonym.

Equations

• RS.indToDayCompIso = CategoryTheory.Iso.refl RS.indToDay

instance RS.indToDay_preservesFilteredColimits {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (I : Type v) [CategoryTheory.SmallCategory I] [CategoryTheory.IsFiltered I] : CategoryTheory.Limits.PreservesColimitsOfShape I indToDay

The embedding into the Day presheaf category preserves small filtered colimits: the inclusion into plain presheaves creates them and the tautological Day equivalence preserves everything.

instance RS.tensorLeft_ind_preservesColimitsOfShape {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Ind C) (I : Type v) [CategoryTheory.SmallCategory I] [CategoryTheory.IsFiltered I] : CategoryTheory.Limits.PreservesColimitsOfShape I (CategoryTheory.MonoidalCategory.tensorLeft X)

Deligne 2.2, filtered half, left version: tensoring on the left in Ind C preserves small filtered colimits. The embedding into the Day presheaf category is monoidal, so it intertwines tensorLeft X with the Day-convolution tensorLeft of the image, which preserves all small colimits; the embedding preserves and reflects filtered colimits, so tensorLeft X preserves them.

instance RS.tensorRight_ind_preservesColimitsOfShape {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Ind C) (I : Type v) [CategoryTheory.SmallCategory I] [CategoryTheory.IsFiltered I] : CategoryTheory.Limits.PreservesColimitsOfShape I (CategoryTheory.MonoidalCategory.tensorRight X)

Deligne 2.2, filtered half, right version: tensoring on the right in Ind C preserves small filtered colimits.

instance RS.tensorLeft_ind_preservesFilteredColimits {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Ind C) : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.MonoidalCategory.tensorLeft X)

Filtered-colimit preservation by left tensoring, packaged.

instance RS.tensorRight_ind_preservesFilteredColimits {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Ind C) : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.MonoidalCategory.tensorRight X)

Filtered-colimit preservation by right tensoring, packaged.

noncomputable def RS.indOfDayIso {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] : indOf.comp indToDay ≅ CategoryTheory.yoneda.comp (CategoryTheory.MonoidalCategory.DayFunctor.equiv Cᵒᵖ (Type v)).inverse

The embedding into the Day presheaf category, restricted along indOf, is the Day synonym of the Yoneda embedding.

Equations

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

noncomputable def RS.indToDayIndOfIso {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (z : C) : indToDay.obj (indOf.obj z) ≅ { functor := CategoryTheory.yoneda.obj z }

The embedding sends indOf.obj z to the Day representable at z.

Equations

• RS.indToDayIndOfIso z = RS.indOfDayIso.app z

noncomputable def RS.indToDayTensorIso {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (x y : C) : indToDay.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (indOf.obj x) (indOf.obj y)) ≅ indToDay.obj (indOf.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj x y))

The embedding calculus for the tensor of two embedded objects: under indToDay, the tensor indOf.obj x ⊗ indOf.obj y is the Day tensor of the representables at x and y, which is the representable at x ⊗ y — that is, the image of indOf.obj (x ⊗ y).

Equations

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

noncomputable def RS.indToDayFullyFaithful {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] : indToDay.FullyFaithful

The fully faithful structure of the embedding into the Day presheaf category.

Equations

• RS.indToDayFullyFaithful = CategoryTheory.Functor.FullyFaithful.ofFullyFaithful RS.indToDay

noncomputable def RS.indOfTensorIso {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (x y : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (indOf.obj x) (indOf.obj y) ≅ indOf.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)

The tensor of two embedded objects of Ind C is the embedding of the tensor: indOf is monoidal up to isomorphism.

Equations

• RS.indOfTensorIso x y = RS.indToDayFullyFaithful.preimageIso (RS.indToDayTensorIso x y)

noncomputable def RS.indOfTensorIsoSymm {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (x y : C) : indOf.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (indOf.obj x) (indOf.obj y)

The embedding C ⥤ Ind C is monoidal up to isomorphism, in the orientation used downstream.

Equations

• RS.indOfTensorIsoSymm x y = (RS.indOfTensorIso x y).symm

theorem RS.corepresentableBy_homEquiv_uniqueUpToIso_hom {A : Type u_1} [CategoryTheory.Category.{u_3, u_1} A] {F : CategoryTheory.Functor A (Type u_2)} {X X' : A} (e : F.CorepresentableBy X) (e' : F.CorepresentableBy X') : e.homEquiv (e.uniqueUpToIso e').hom = e'.homEquiv (CategoryTheory.CategoryStruct.id X')

Characterisation of the canonical isomorphism between two corepresenting objects: its classification under the first corepresentability structure is the universal element of the second.

def RS.coyonedaTensorHom {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (a b : D) : CategoryTheory.coyoneda.obj (Opposite.op (a, b)) ⟶ (CategoryTheory.MonoidalCategory.tensor D).comp (CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.MonoidalCategoryStruct.tensorObj a b)))

The universal transformation classified by the Day tensor of two corepresentables: on a pair of morphisms it takes the tensor, (f, g) ↦ f ⊗ₘ g.

Equations

• RS.coyonedaTensorHom a b = { app := fun (X : D × D) => TypeCat.ofHom fun (fg : (a, b) ⟶ X) => CategoryTheory.MonoidalCategoryStruct.tensorHom fg.1 fg.2, naturality := ⋯ }

theorem RS.eta_comp_dayCoyonedaIso_hom {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (a b : D) : CategoryTheory.CategoryStruct.comp ({ functor := CategoryTheory.coyoneda.obj (Opposite.op a) }.η { functor := CategoryTheory.coyoneda.obj (Opposite.op b) }) ((CategoryTheory.MonoidalCategory.tensor D).whiskerLeft (dayCoyonedaIso a b).hom.natTrans) = coyonedaTensorHom a b

RS.dayCoyonedaIso classifies as the universal transformation (f, g) ↦ f ⊗ₘ g: composing the Day unit with its underlying natural transformation is RS.coyonedaTensorHom.

theorem RS.dayCoyonedaIso_hom_natural_right {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (a : D) {b b' : D} (h : b ⟶ b') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft { functor := CategoryTheory.coyoneda.obj (Opposite.op a) } { natTrans := CategoryTheory.coyoneda.map h.op }) (dayCoyonedaIso a b).hom = CategoryTheory.CategoryStruct.comp (dayCoyonedaIso a b').hom { natTrans := CategoryTheory.coyoneda.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft a h).op }

Naturality of RS.dayCoyonedaIso in the right variable.

theorem RS.dayCoyonedaIso_hom_natural_left {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] {a a' : D} (f : a ⟶ a') (b : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight { natTrans := CategoryTheory.coyoneda.map f.op } { functor := CategoryTheory.coyoneda.obj (Opposite.op b) }) (dayCoyonedaIso a b).hom = CategoryTheory.CategoryStruct.comp (dayCoyonedaIso a' b).hom { natTrans := CategoryTheory.coyoneda.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f b).op }

Naturality of RS.dayCoyonedaIso in the left variable.

theorem RS.yoneda_map_comp_objOpOp_inv {C : Type v} [CategoryTheory.SmallCategory C] {y y' : C} (g : y ⟶ y') : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map g) (CategoryTheory.Coyoneda.objOpOp y').inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Coyoneda.objOpOp y).inv (CategoryTheory.coyoneda.map g.op.op)

Naturality of Coyoneda.objOpOp, inverse form.

theorem RS.coyoneda_map_whiskerLeft_comp_objOpOp_hom {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (x : C) {y y' : C} (g : y ⟶ y') : CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Opposite.op x) g.op).op) (CategoryTheory.Coyoneda.objOpOp (CategoryTheory.MonoidalCategoryStruct.tensorObj x y')).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Coyoneda.objOpOp (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)).hom (CategoryTheory.yoneda.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft x g))

Naturality of Coyoneda.objOpOp, forward form, at a left whiskering of Cᵒᵖ.

theorem RS.coyoneda_map_whiskerRight_comp_objOpOp_hom {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] {x x' : C} (f : x ⟶ x') (y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.op (Opposite.op y)).op) (CategoryTheory.Coyoneda.objOpOp (CategoryTheory.MonoidalCategoryStruct.tensorObj x' y)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Coyoneda.objOpOp (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)).hom (CategoryTheory.yoneda.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f y))

Naturality of Coyoneda.objOpOp, forward form, at a right whiskering of Cᵒᵖ.

theorem RS.dayYonedaIso_hom_natural_right {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (x : C) {y y' : C} (g : y ⟶ y') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft { functor := CategoryTheory.yoneda.obj x } { natTrans := CategoryTheory.yoneda.map g }) (dayYonedaIso x y').hom = CategoryTheory.CategoryStruct.comp (dayYonedaIso x y).hom { natTrans := CategoryTheory.yoneda.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft x g) }

Naturality of RS.dayYonedaIso in the right variable.

theorem RS.dayYonedaIso_hom_natural_left {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] {x x' : C} (f : x ⟶ x') (y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight { natTrans := CategoryTheory.yoneda.map f } { functor := CategoryTheory.yoneda.obj y }) (dayYonedaIso x' y).hom = CategoryTheory.CategoryStruct.comp (dayYonedaIso x y).hom { natTrans := CategoryTheory.yoneda.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f y) }

Naturality of RS.dayYonedaIso in the left variable.

theorem RS.indToDay_map_comp_indToDayIndOfIso_hom {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] {z z' : C} (u : z ⟶ z') : CategoryTheory.CategoryStruct.comp (indToDay.map (indOf.map u)) (indToDayIndOfIso z').hom = CategoryTheory.CategoryStruct.comp (indToDayIndOfIso z).hom { natTrans := CategoryTheory.yoneda.map u }

Naturality of RS.indToDayIndOfIso in its object.

theorem RS.comp_indToDayIndOfIso_inv {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] {z z' : C} (u : z ⟶ z') : CategoryTheory.CategoryStruct.comp { natTrans := CategoryTheory.yoneda.map u } (indToDayIndOfIso z').inv = CategoryTheory.CategoryStruct.comp (indToDayIndOfIso z).inv (indToDay.map (indOf.map u))

Inverse form of RS.indToDay_map_comp_indToDayIndOfIso_hom.

theorem RS.indOfTensorIso_hom_natural_right {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (x : C) {y y' : C} (g : y ⟶ y') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (indOf.obj x) (indOf.map g)) (indOfTensorIso x y').hom = CategoryTheory.CategoryStruct.comp (indOfTensorIso x y).hom (indOf.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft x g))

Naturality of RS.indOfTensorIso in the right variable: the embedding-tensor comparison intertwines whiskering by an embedded object with the embedded whiskering.

theorem RS.indOfTensorIso_hom_natural_left {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] {x x' : C} (f : x ⟶ x') (y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (indOf.map f) (indOf.obj y)) (indOfTensorIso x' y).hom = CategoryTheory.CategoryStruct.comp (indOfTensorIso x y).hom (indOf.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f y))

Naturality of RS.indOfTensorIso in the left variable.

noncomputable def RS.indOfUnitIso {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ≅ indOf.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

The unit of Ind C is the embedded unit: the transported Day unit, identified through RS.dayUnitIso with the representable at 𝟙_ C and pulled back through the fully faithful monoidal embedding RS.indToDay.

Equations

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

def RS.coconeLeg {J : Type v₁} [CategoryTheory.Category.{v₁, v₁} J] {ℬ : Type u₃} [CategoryTheory.Category.{v₃, u₃} ℬ] {D : CategoryTheory.Functor J ℬ} (c : CategoryTheory.Limits.Cocone D) (j : J) : D.obj j ⟶ c.pt

A cocone leg, with its type stated at the cocone point.

Equations

• RS.coconeLeg c j = c.ι.app j

theorem RS.coconeLeg_w {J : Type v₁} [CategoryTheory.Category.{v₁, v₁} J] {ℬ : Type u₃} [CategoryTheory.Category.{v₃, u₃} ℬ] {D : CategoryTheory.Functor J ℬ} (c : CategoryTheory.Limits.Cocone D) {j k : J} (u : j ⟶ k) : CategoryTheory.CategoryStruct.comp (D.map u) (coconeLeg c k) = coconeLeg c j

@[reducible]

noncomputable def RS.coprodDiagram {J : Type v₁} [CategoryTheory.Category.{v₁, v₁} J] {ℬ : Type u₃} [CategoryTheory.Category.{v₃, u₃} ℬ] [CategoryTheory.Limits.HasBinaryCoproducts ℬ] (D₁ D₂ : CategoryTheory.Functor J ℬ) : CategoryTheory.Functor J ℬ

The pointwise binary coproduct of two diagrams of the same shape.

Equations

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

@[simp]

theorem RS.coprodDiagram_map {J : Type v₁} [CategoryTheory.Category.{v₁, v₁} J] {ℬ : Type u₃} [CategoryTheory.Category.{v₃, u₃} ℬ] [CategoryTheory.Limits.HasBinaryCoproducts ℬ] (D₁ D₂ : CategoryTheory.Functor J ℬ) {X✝ Y✝ : J} (u : X✝ ⟶ Y✝) : (coprodDiagram D₁ D₂).map u = CategoryTheory.Limits.coprod.map (D₁.map u) (D₂.map u)

@[simp]

theorem RS.coprodDiagram_obj {J : Type v₁} [CategoryTheory.Category.{v₁, v₁} J] {ℬ : Type u₃} [CategoryTheory.Category.{v₃, u₃} ℬ] [CategoryTheory.Limits.HasBinaryCoproducts ℬ] (D₁ D₂ : CategoryTheory.Functor J ℬ) (j : J) : (coprodDiagram D₁ D₂).obj j = (D₁.obj j ⨿ D₂.obj j)

def RS.coprodLeg {J : Type v₁} [CategoryTheory.Category.{v₁, v₁} J] {ℬ : Type u₃} [CategoryTheory.Category.{v₃, u₃} ℬ] [CategoryTheory.Limits.HasBinaryCoproducts ℬ] {D₁ D₂ : CategoryTheory.Functor J ℬ} (s : CategoryTheory.Limits.Cocone (coprodDiagram D₁ D₂)) (j : J) : D₁.obj j ⨿ D₂.obj j ⟶ s.pt

A leg of a cocone over a pointwise coproduct, with its type stated at the coproduct.

Equations

• RS.coprodLeg s j = s.ι.app j

theorem RS.coprodLeg_w {J : Type v₁} [CategoryTheory.Category.{v₁, v₁} J] {ℬ : Type u₃} [CategoryTheory.Category.{v₃, u₃} ℬ] [CategoryTheory.Limits.HasBinaryCoproducts ℬ] {D₁ D₂ : CategoryTheory.Functor J ℬ} (s : CategoryTheory.Limits.Cocone (coprodDiagram D₁ D₂)) {j k : J} (u : j ⟶ k) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (D₁.map u) (D₂.map u)) (coprodLeg s k) = coprodLeg s j

@[reducible]

noncomputable def RS.coprodCocone {J : Type v₁} [CategoryTheory.Category.{v₁, v₁} J] {ℬ : Type u₃} [CategoryTheory.Category.{v₃, u₃} ℬ] [CategoryTheory.Limits.HasBinaryCoproducts ℬ] {D₁ D₂ : CategoryTheory.Functor J ℬ} (c₁ : CategoryTheory.Limits.Cocone D₁) (c₂ : CategoryTheory.Limits.Cocone D₂) : CategoryTheory.Limits.Cocone (coprodDiagram D₁ D₂)

The coproduct of two cocones: a cocone over the pointwise coproduct diagram, with the coproduct of the two points as its point.

Equations

• RS.coprodCocone c₁ c₂ = { pt := c₁.pt ⨿ c₂.pt, ι := { app := fun (j : J) => CategoryTheory.Limits.coprod.map (RS.coconeLeg c₁ j) (RS.coconeLeg c₂ j), naturality := ⋯ } }

@[simp]

theorem RS.coprodCocone_ι_app {J : Type v₁} [CategoryTheory.Category.{v₁, v₁} J] {ℬ : Type u₃} [CategoryTheory.Category.{v₃, u₃} ℬ] [CategoryTheory.Limits.HasBinaryCoproducts ℬ] {D₁ D₂ : CategoryTheory.Functor J ℬ} (c₁ : CategoryTheory.Limits.Cocone D₁) (c₂ : CategoryTheory.Limits.Cocone D₂) (j : J) : (coprodCocone c₁ c₂).ι.app j = CategoryTheory.Limits.coprod.map (coconeLeg c₁ j) (coconeLeg c₂ j)

@[simp]

theorem RS.coprodCocone_pt {J : Type v₁} [CategoryTheory.Category.{v₁, v₁} J] {ℬ : Type u₃} [CategoryTheory.Category.{v₃, u₃} ℬ] [CategoryTheory.Limits.HasBinaryCoproducts ℬ] {D₁ D₂ : CategoryTheory.Functor J ℬ} (c₁ : CategoryTheory.Limits.Cocone D₁) (c₂ : CategoryTheory.Limits.Cocone D₂) : (coprodCocone c₁ c₂).pt = (c₁.pt ⨿ c₂.pt)

@[reducible]

noncomputable def RS.coprodCoconeFst {J : Type v₁} [CategoryTheory.Category.{v₁, v₁} J] {ℬ : Type u₃} [CategoryTheory.Category.{v₃, u₃} ℬ] [CategoryTheory.Limits.HasBinaryCoproducts ℬ] {D₁ D₂ : CategoryTheory.Functor J ℬ} (s : CategoryTheory.Limits.Cocone (coprodDiagram D₁ D₂)) : CategoryTheory.Limits.Cocone D₁

A cocone over the pointwise coproduct, restricted along the first inclusion to a cocone over the first diagram.

Equations

• RS.coprodCoconeFst s = { pt := s.pt, ι := { app := fun (j : J) => CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (RS.coprodLeg s j), naturality := ⋯ } }

@[simp]

theorem RS.coprodCoconeFst_ι_app {J : Type v₁} [CategoryTheory.Category.{v₁, v₁} J] {ℬ : Type u₃} [CategoryTheory.Category.{v₃, u₃} ℬ] [CategoryTheory.Limits.HasBinaryCoproducts ℬ] {D₁ D₂ : CategoryTheory.Functor J ℬ} (s : CategoryTheory.Limits.Cocone (coprodDiagram D₁ D₂)) (j : J) : (coprodCoconeFst s).ι.app j = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (coprodLeg s j)

@[simp]

theorem RS.coprodCoconeFst_pt {J : Type v₁} [CategoryTheory.Category.{v₁, v₁} J] {ℬ : Type u₃} [CategoryTheory.Category.{v₃, u₃} ℬ] [CategoryTheory.Limits.HasBinaryCoproducts ℬ] {D₁ D₂ : CategoryTheory.Functor J ℬ} (s : CategoryTheory.Limits.Cocone (coprodDiagram D₁ D₂)) : (coprodCoconeFst s).pt = s.pt

@[reducible]

noncomputable def RS.coprodCoconeSnd {J : Type v₁} [CategoryTheory.Category.{v₁, v₁} J] {ℬ : Type u₃} [CategoryTheory.Category.{v₃, u₃} ℬ] [CategoryTheory.Limits.HasBinaryCoproducts ℬ] {D₁ D₂ : CategoryTheory.Functor J ℬ} (s : CategoryTheory.Limits.Cocone (coprodDiagram D₁ D₂)) : CategoryTheory.Limits.Cocone D₂

A cocone over the pointwise coproduct, restricted along the second inclusion to a cocone over the second diagram.

Equations

• RS.coprodCoconeSnd s = { pt := s.pt, ι := { app := fun (j : J) => CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (RS.coprodLeg s j), naturality := ⋯ } }

@[simp]

theorem RS.coprodCoconeSnd_pt {J : Type v₁} [CategoryTheory.Category.{v₁, v₁} J] {ℬ : Type u₃} [CategoryTheory.Category.{v₃, u₃} ℬ] [CategoryTheory.Limits.HasBinaryCoproducts ℬ] {D₁ D₂ : CategoryTheory.Functor J ℬ} (s : CategoryTheory.Limits.Cocone (coprodDiagram D₁ D₂)) : (coprodCoconeSnd s).pt = s.pt

@[simp]

theorem RS.coprodCoconeSnd_ι_app {J : Type v₁} [CategoryTheory.Category.{v₁, v₁} J] {ℬ : Type u₃} [CategoryTheory.Category.{v₃, u₃} ℬ] [CategoryTheory.Limits.HasBinaryCoproducts ℬ] {D₁ D₂ : CategoryTheory.Functor J ℬ} (s : CategoryTheory.Limits.Cocone (coprodDiagram D₁ D₂)) (j : J) : (coprodCoconeSnd s).ι.app j = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (coprodLeg s j)

noncomputable def RS.isColimitCoprodCocone {J : Type v₁} [CategoryTheory.Category.{v₁, v₁} J] {ℬ : Type u₃} [CategoryTheory.Category.{v₃, u₃} ℬ] [CategoryTheory.Limits.HasBinaryCoproducts ℬ] {D₁ D₂ : CategoryTheory.Functor J ℬ} {c₁ : CategoryTheory.Limits.Cocone D₁} {c₂ : CategoryTheory.Limits.Cocone D₂} (h₁ : CategoryTheory.Limits.IsColimit c₁) (h₂ : CategoryTheory.Limits.IsColimit c₂) : CategoryTheory.Limits.IsColimit (coprodCocone c₁ c₂)

The coproduct of two colimit cocones is a colimit cocone over the pointwise coproduct diagram: colimits commute with binary coproducts.

Equations

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

@[reducible]

noncomputable def RS.coprodPairFunctor {𝒜 : Type u₂} [CategoryTheory.Category.{v₂, u₂} 𝒜] {ℬ : Type u₃} [CategoryTheory.Category.{v₃, u₃} ℬ] [CategoryTheory.Limits.HasBinaryCoproducts ℬ] (F G : CategoryTheory.Functor 𝒜 ℬ) : CategoryTheory.Functor 𝒜 ℬ

The pointwise binary coproduct of two functors.

Equations

• RS.coprodPairFunctor F G = { obj := fun (A : 𝒜) => F.obj A ⨿ G.obj A, map := fun {X Y : 𝒜} (u : X ⟶ Y) => CategoryTheory.Limits.coprod.map (F.map u) (G.map u), map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem RS.coprodPairFunctor_map {𝒜 : Type u₂} [CategoryTheory.Category.{v₂, u₂} 𝒜] {ℬ : Type u₃} [CategoryTheory.Category.{v₃, u₃} ℬ] [CategoryTheory.Limits.HasBinaryCoproducts ℬ] (F G : CategoryTheory.Functor 𝒜 ℬ) {X✝ Y✝ : 𝒜} (u : X✝ ⟶ Y✝) : (coprodPairFunctor F G).map u = CategoryTheory.Limits.coprod.map (F.map u) (G.map u)

@[simp]

theorem RS.coprodPairFunctor_obj {𝒜 : Type u₂} [CategoryTheory.Category.{v₂, u₂} 𝒜] {ℬ : Type u₃} [CategoryTheory.Category.{v₃, u₃} ℬ] [CategoryTheory.Limits.HasBinaryCoproducts ℬ] (F G : CategoryTheory.Functor 𝒜 ℬ) (A : 𝒜) : (coprodPairFunctor F G).obj A = (F.obj A ⨿ G.obj A)

theorem RS.preservesColimitsOfShape_coprodPairFunctor {J : Type v₁} [CategoryTheory.Category.{v₁, v₁} J] {𝒜 : Type u₂} [CategoryTheory.Category.{v₂, u₂} 𝒜] {ℬ : Type u₃} [CategoryTheory.Category.{v₃, u₃} ℬ] [CategoryTheory.Limits.HasBinaryCoproducts ℬ] (F G : CategoryTheory.Functor 𝒜 ℬ) [CategoryTheory.Limits.PreservesColimitsOfShape J F] [CategoryTheory.Limits.PreservesColimitsOfShape J G] : CategoryTheory.Limits.PreservesColimitsOfShape J (coprodPairFunctor F G)

theorem RS.preservesColimitsOfShape_const_of_isConnected {J : Type v₁} [CategoryTheory.Category.{v₁, v₁} J] {𝒜 : Type u₂} [CategoryTheory.Category.{v₂, u₂} 𝒜] {ℬ : Type u₃} [CategoryTheory.Category.{v₃, u₃} ℬ] [CategoryTheory.IsConnected J] (W : ℬ) : CategoryTheory.Limits.PreservesColimitsOfShape J ((CategoryTheory.Functor.const 𝒜).obj W)

theorem RS.isIso_app_of_isIso_indOf {C : Type v} [CategoryTheory.SmallCategory C] {L R : CategoryTheory.Functor (CategoryTheory.Ind C) (CategoryTheory.Ind C)} [CategoryTheory.Limits.PreservesFilteredColimits L] [CategoryTheory.Limits.PreservesFilteredColimits R] (γ : L ⟶ R) (hbase : ∀ (c : C), CategoryTheory.IsIso (γ.app (indOf.obj c))) (A : CategoryTheory.Ind C) : CategoryTheory.IsIso (γ.app A)

Filtered descent for pointwise-invertible transformations: a natural transformation between endofunctors of Ind C that both preserve filtered colimits is invertible everywhere as soon as it is invertible on the embedded objects, since every ind-object is a filtered colimit of embedded objects.

theorem RS.isIso_of_coprod_eq_whiskerLeft_indOf {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasFiniteColimits C] (a x y : C) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj a x ⨿ CategoryTheory.MonoidalCategoryStruct.tensorObj a y ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj a (x ⨿ y)) [CategoryTheory.IsIso w] (hw₁ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl w = CategoryTheory.MonoidalCategoryStruct.whiskerLeft a CategoryTheory.Limits.coprod.inl) (hw₂ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr w = CategoryTheory.MonoidalCategoryStruct.whiskerLeft a CategoryTheory.Limits.coprod.inr) (v : CategoryTheory.MonoidalCategoryStruct.tensorObj (indOf.obj a) (indOf.obj x) ⨿ CategoryTheory.MonoidalCategoryStruct.tensorObj (indOf.obj a) (indOf.obj y) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (indOf.obj a) (indOf.obj x ⨿ indOf.obj y)) (hv₁ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl v = CategoryTheory.MonoidalCategoryStruct.whiskerLeft (indOf.obj a) CategoryTheory.Limits.coprod.inl) (hv₂ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr v = CategoryTheory.MonoidalCategoryStruct.whiskerLeft (indOf.obj a) CategoryTheory.Limits.coprod.inr) : CategoryTheory.IsIso v

Abstract form of the embedded base case, left version: a morphism satisfying the two defining equations of the binary coproduct comparison for tensorLeft (indOf.obj a) at a pair of embedded objects is invertible, provided the corresponding comparison in C is.

theorem RS.isIso_of_coprod_eq_whiskerRight_indOf {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasFiniteColimits C] (a x y : C) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj x a ⨿ CategoryTheory.MonoidalCategoryStruct.tensorObj y a ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (x ⨿ y) a) [CategoryTheory.IsIso w] (hw₁ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl w = CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inl a) (hw₂ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr w = CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inr a) (v : CategoryTheory.MonoidalCategoryStruct.tensorObj (indOf.obj x) (indOf.obj a) ⨿ CategoryTheory.MonoidalCategoryStruct.tensorObj (indOf.obj y) (indOf.obj a) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (indOf.obj x ⨿ indOf.obj y) (indOf.obj a)) (hv₁ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl v = CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inl (indOf.obj a)) (hv₂ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr v = CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inr (indOf.obj a)) : CategoryTheory.IsIso v

Abstract form of the embedded base case, right version.

theorem RS.isIso_coprodComparison_tensorLeft_indOf₀ {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] (a x y : C) : CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorLeft (indOf.obj a)) (indOf.obj x) (indOf.obj y))

The embedded base case, left version: the binary coproduct comparison for tensoring on the left by an embedded object is invertible at a pair of embedded objects.

theorem RS.isIso_coprodComparison_tensorRight_indOf₀ {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] (a x y : C) : CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorRight (indOf.obj a)) (indOf.obj x) (indOf.obj y))

The embedded base case, right version.

theorem RS.isIso_coprodComparison_tensorLeft_indOf₁ {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] (a x : C) (Y : CategoryTheory.Ind C) : CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorLeft (indOf.obj a)) (indOf.obj x) Y)

Stage two, left version: the comparison for tensoring on the left by an embedded object, at one embedded and one arbitrary argument. Filtered descent in the second coproduct argument.

theorem RS.isIso_coprodComparison_tensorRight_indOf₁ {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] (a x : C) (Y : CategoryTheory.Ind C) : CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorRight (indOf.obj a)) (indOf.obj x) Y)

Stage two, right version.

theorem RS.isIso_coprodComparison_tensorLeft_indOf₂ {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] (a : C) (X Y : CategoryTheory.Ind C) : CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorLeft (indOf.obj a)) X Y)

Stage three, left version: descent in the first coproduct argument.

theorem RS.isIso_coprodComparison_tensorRight_indOf₂ {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] (a : C) (X Y : CategoryTheory.Ind C) : CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorRight (indOf.obj a)) X Y)

Stage three, right version.

theorem RS.isIso_coprodComparison_tensorLeft {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] (A X Y : CategoryTheory.Ind C) : CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorLeft A) X Y)

The binary coproduct comparison for left tensoring in Ind C is invertible: final descent in the tensoring object.

theorem RS.isIso_coprodComparison_tensorRight {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] (A X Y : CategoryTheory.Ind C) : CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorRight A) X Y)

The binary coproduct comparison for right tensoring in Ind C is invertible.

theorem RS.isZero_of_isInitial_isTerminal {𝒜 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒜] {X : 𝒜} (hI : CategoryTheory.Limits.IsInitial X) (hT : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Limits.IsZero X

An object that is both initial and terminal is a zero object.

theorem RS.isZero_indOf {C : Type v} [CategoryTheory.SmallCategory C] {W : C} (hW : CategoryTheory.Limits.IsZero W) : CategoryTheory.Limits.IsZero (indOf.obj W)

The embedding C ⥤ Ind C carries zero objects to zero objects: it preserves the initial and the terminal object.

theorem RS.isZero_colimit_of_isZero {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] {I : Type v} [CategoryTheory.SmallCategory I] (K : CategoryTheory.Functor I (CategoryTheory.Ind C)) [CategoryTheory.Limits.HasColimit K] (h : ∀ (i : I), CategoryTheory.Limits.IsZero (K.obj i)) : CategoryTheory.Limits.IsZero (CategoryTheory.Limits.colimit K)

A colimit all of whose stages vanish vanishes.

theorem RS.isZero_tensor_left_ind {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] (A : CategoryTheory.Ind C) {Z : CategoryTheory.Ind C} (hZ : CategoryTheory.Limits.IsZero Z) : CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorObj A Z)

Tensoring a vanishing ind-object on the left kills it: descend along a presentation of the other factor and use that tensoring in C is additive.

theorem RS.isZero_tensor_right_ind {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] (A : CategoryTheory.Ind C) {Z : CategoryTheory.Ind C} (hZ : CategoryTheory.Limits.IsZero Z) : CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorObj Z A)

Tensoring a vanishing ind-object on the right kills it.

theorem RS.preservesZeroMorphisms_tensorLeft_ind {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] (A : CategoryTheory.Ind C) : (CategoryTheory.MonoidalCategory.tensorLeft A).PreservesZeroMorphisms

Left tensoring on Ind C preserves zero morphisms.

theorem RS.preservesZeroMorphisms_tensorRight_ind {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] (A : CategoryTheory.Ind C) : (CategoryTheory.MonoidalCategory.tensorRight A).PreservesZeroMorphisms

Right tensoring on Ind C preserves zero morphisms.

theorem RS.preservesBinaryCoproducts_tensorLeft_ind {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] (A : CategoryTheory.Ind C) : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (CategoryTheory.MonoidalCategory.tensorLeft A)

Left tensoring on Ind C preserves binary coproducts.

theorem RS.preservesBinaryCoproducts_tensorRight_ind {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] (A : CategoryTheory.Ind C) : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (CategoryTheory.MonoidalCategory.tensorRight A)

Right tensoring on Ind C preserves binary coproducts.

instance RS.tensorLeft_ind_additive {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] (A : CategoryTheory.Ind C) : (CategoryTheory.MonoidalCategory.tensorLeft A).Additive

Left tensoring on Ind C is additive.

instance RS.tensorRight_ind_additive {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] (A : CategoryTheory.Ind C) : (CategoryTheory.MonoidalCategory.tensorRight A).Additive

Right tensoring on Ind C is additive.

instance RS.instMonoidalPreadditiveInd_leanPool {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] : CategoryTheory.MonoidalPreadditive (CategoryTheory.Ind C)

Deligne 2.2, preadditive half: the transported monoidal structure on Ind C is preadditive — whiskering is additive in each variable.