The monoidal structure on ind-objects

Deligne's 2.2: the tensor product of a small ℂ-tensorielle category extends to its ind-completion by (colim Xᵢ) ⊗ (colim Yⱼ) = colim (Xᵢ ⊗ Yⱼ). Here the extension is packaged through Day convolution: presheaves on C carry the Day monoidal structure (Cᵒᵖ ⊛⥤ Type v, with the instances of DayType.lean), the ind-objects are closed under it — the Day tensor preserves colimits in each variable and sends a pair of representables to the representable of the tensor — and Ind C inherits the structure through Ind.equivalence and the full monoidal subcategory of the ind-property.

def RS.IsIndDay (C : Type v) [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.MonoidalCategory.DayFunctor Cᵒᵖ (Type v)) : Prop

The ind-property, read on the Day synonym of the presheaf category.

Equations

• RS.IsIndDay C F = CategoryTheory.Limits.IsIndObject F.functor

instance RS.isIndDay_isMonoidal (C : Type v) [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.ObjectProperty.IsMonoidal (IsIndDay C)

The ind-property is monoidal: it holds for the unit and is stable under the Day tensor.

instance RS.isIndDay_closedUnderIso (C : Type v) [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms (IsIndDay C)

The ind-property respects isomorphisms.

noncomputable def RS.indDayCongr (C : Type v) [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Limits.IsIndObject ≌ CategoryTheory.ObjectProperty.FullSubcategory (IsIndDay C)

The wrapper equivalence between the ind-subcategory of the presheaf category and the ind-subcategory of its Day synonym.

Equations

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

noncomputable def RS.indDayEquivalence (C : Type v) [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Ind C ≌ CategoryTheory.ObjectProperty.FullSubcategory (IsIndDay C)

Ind C is equivalent to the monoidal full subcategory of ind-objects of the Day presheaf category.

Equations

• RS.indDayEquivalence C = (CategoryTheory.Ind.equivalence C).trans (RS.indDayCongr C)

@[instance_reducible]

noncomputable instance RS.indMonoidalCategory (C : Type v) [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.MonoidalCategory (CategoryTheory.Ind C)

Deligne 2.2, structure half: the tensor product of a small monoidal category extends to its ind-completion — the Day tensor structure transported across the indization equivalence.

Equations

• RS.indMonoidalCategory C = CategoryTheory.Monoidal.transport (RS.indDayEquivalence C).symm

@[instance_reducible]

instance RS.symmetricCategoryOp {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] : CategoryTheory.SymmetricCategory Dᵒᵖ

The opposite of a symmetric category is symmetric (the braided instance exists in Mathlib at this pin; the symmetric one does not).

Equations

• RS.symmetricCategoryOp = { toBraidedCategory := instBraidedCategoryOpposite, symmetry := ⋯ }

@[instance_reducible]

noncomputable instance RS.indBraidedCategory (C : Type v) [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.BraidedCategory (CategoryTheory.Ind C)

The braiding transports as well: Ind C of a braided small category is braided.

Equations

• RS.indBraidedCategory C = { braiding := RS.indBraidedCategory._aux_1 C, braiding_naturality_right := ⋯, braiding_naturality_left := ⋯, hexagon_forward := ⋯, hexagon_reverse := ⋯ }

@[instance_reducible]

noncomputable instance RS.indSymmetricCategory (C : Type v) [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] : CategoryTheory.SymmetricCategory (CategoryTheory.Ind C)

And the symmetry: Ind C of a symmetric small category is symmetric.

Equations

• RS.indSymmetricCategory C = { toBraidedCategory := RS.indBraidedCategory C, symmetry := ⋯ }