The embedding C ⥤ Ind C as a strong braided monoidal functor

RS.Classical.Deligne.IndSchur assembles the comparison data of the embedding RS.indOf : C ⥤ Ind C — the unit comparison RS.indOfUnitIso, the tensor comparison RS.indOfTensorIso, and their compatibility with the associator and the braiding. This file supplies the two remaining coherences, the unitalities, and packages the whole as the Mathlib classes:

• RS.indOfLaxMonoidal — indOf is lax monoidal, with ε the forward direction of RS.indOfUnitIso and μ that of RS.indOfTensorIso;
• RS.indOfMonoidal — the comparisons are isomorphisms, so indOf is strong monoidal, with RS.indOfMonoidal_εIso/RS.indOfMonoidal_μIso and RS.indOf_oplax_η/RS.indOf_oplax_δ reading off the packaged data;
• RS.indOfBraided — and braided, for C braided.

The two coherences that RS.Classical.Deligne.IndSchur does not already supply are the unitalities RS.indOfUnitIso_hom_leftUnitor and RS.indOfUnitIso_hom_rightUnitor. The left one is RS.indOf_leftUnitor_hom of RS.Classical.Deligne.SchurTransport, which also carries the Day-level RS.dayCoyonedaIso_hom_leftUnitor and its Yoneda form RS.dayYonedaIso_hom_leftUnitor; this file supplies the mirror-image right-handed calculus, RS.dayCoyonedaIso_hom_rightUnitor and RS.dayYonedaIso_hom_rightUnitor.

The unitalities are proved the same way as the associativity: the embedding RS.indToDay into the Day presheaf category is fully faithful and monoidal, so it suffices to prove the corresponding identities for the Day comparison RS.dayYonedaIso and the Day unit RS.dayUnitIso. Those are decided, as everywhere in this lane, by evaluating both sides on the canonical element RS.dayCoyonedaUnitElt: the Day unitors are characterised on the Kan-extension unit by the leftUnitor_hom_unit_app and rightUnitor_hom_unit_app fields of Mathlib's CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.

theorem RS.whiskerLeft_dayUnitIso_inv_app_unitElt {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (a : D) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.MonoidalCategoryStruct.whiskerLeft { functor := CategoryTheory.coyoneda.obj (Opposite.op a) } (dayUnitIso D).inv).natTrans.app (CategoryTheory.MonoidalCategoryStruct.tensorObj a (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)))) (dayCoyonedaUnitElt a (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) = (CategoryTheory.ConcreteCategory.hom (({ functor := CategoryTheory.coyoneda.obj (Opposite.op a) }.η (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.MonoidalCategory.DayFunctor D (Type v)))).app (a, CategoryTheory.MonoidalCategoryStruct.tensorUnit D))) (CategoryTheory.CategoryStruct.id a, (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategory.DayFunctor.ν D (Type v))) PUnit.unit)

Left-whiskering the inverse of RS.dayUnitIso carries the canonical element at (a, 𝟙_ D) to the Kan-extension unit element assembled from the Day-unit element.

theorem RS.dayRightUnitor_hom_unit {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (K : CategoryTheory.MonoidalCategory.DayFunctor D (Type v)) (y : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (K.functor.obj y) (CategoryTheory.MonoidalCategory.DayFunctor.ν D (Type v))) (CategoryTheory.CategoryStruct.comp ((K.η (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.MonoidalCategory.DayFunctor D (Type v)))).app (y, CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) ((CategoryTheory.MonoidalCategoryStruct.rightUnitor K).hom.natTrans.app (CategoryTheory.MonoidalCategoryStruct.tensorObj y (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (K.functor.obj y)).hom (K.functor.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor y).inv)

The Day right unitor, characterised on the Kan-extension unit.

theorem RS.dayRightUnitor_hom_app_unitElt {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (a : D) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.MonoidalCategoryStruct.rightUnitor { functor := CategoryTheory.coyoneda.obj (Opposite.op a) }).hom.natTrans.app (CategoryTheory.MonoidalCategoryStruct.tensorObj a (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)))) ((CategoryTheory.ConcreteCategory.hom (({ functor := CategoryTheory.coyoneda.obj (Opposite.op a) }.η (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.MonoidalCategory.DayFunctor D (Type v)))).app (a, CategoryTheory.MonoidalCategoryStruct.tensorUnit D))) (CategoryTheory.CategoryStruct.id a, (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategory.DayFunctor.ν D (Type v))) PUnit.unit)) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor a).inv

Evaluation of the Day right unitor on the canonical element built from the Day-unit element.

theorem RS.dayCoyonedaIso_hom_rightUnitor {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (a : D) : CategoryTheory.CategoryStruct.comp (dayCoyonedaIso a (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).hom { natTrans := CategoryTheory.coyoneda.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor a).inv.op } = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft { functor := CategoryTheory.coyoneda.obj (Opposite.op a) } (dayUnitIso D).inv) (CategoryTheory.MonoidalCategoryStruct.rightUnitor { functor := CategoryTheory.coyoneda.obj (Opposite.op a) }).hom

Day convolution of corepresentables intertwines the right unitor.

noncomputable def RS.dayYonedaUnitIso {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.MonoidalCategory.DayFunctor Cᵒᵖ (Type v)) ≅ { functor := CategoryTheory.yoneda.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) }

The Day unit is the representable presheaf at the unit of C: the Yoneda form of RS.dayUnitIso.

Equations

• RS.dayYonedaUnitIso = RS.dayUnitIso Cᵒᵖ ≪≫ RS.dayMkIso (CategoryTheory.Coyoneda.objOpOp (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))

theorem RS.dayYonedaIso_hom_rightUnitor {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (x : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft { functor := CategoryTheory.yoneda.obj x } dayYonedaUnitIso.hom) (CategoryTheory.CategoryStruct.comp (dayYonedaIso x (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom { natTrans := CategoryTheory.yoneda.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor x).hom }) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor { functor := CategoryTheory.yoneda.obj x }).hom

The Day tensor of representables intertwines the right unitor: the Yoneda form of RS.dayCoyonedaIso_hom_rightUnitor.

theorem RS.indToDay_map_indOfUnitIso_hom_dayYonedaUnitIso {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] : indToDay.map indOfUnitIso.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η indToDay) (CategoryTheory.CategoryStruct.comp dayYonedaUnitIso.hom (indToDayIndOfIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv)

The embedding into the Day presheaf category carries the unit comparison to the Day unit: the RS.dayYonedaUnitIso reading of RS.indToDay_map_indOfUnitIso_hom.

theorem RS.indOfUnitIso_hom_leftUnitor {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (x : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight indOfUnitIso.hom (indOf.obj x)) (CategoryTheory.CategoryStruct.comp (indOfTensorIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) x).hom (indOf.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor x).hom)) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (indOf.obj x)).hom

The unit and tensor comparisons satisfy left unitality: the left-unitality axiom of the monoidal structure of indOf. This is RS.indOf_leftUnitor_hom read in the direction the LaxMonoidal field wants.

theorem RS.indOfUnitIso_hom_rightUnitor {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (x : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (indOf.obj x) indOfUnitIso.hom) (CategoryTheory.CategoryStruct.comp (indOfTensorIso x (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom (indOf.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor x).hom)) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (indOf.obj x)).hom

The unit and tensor comparisons satisfy right unitality: the right-unitality axiom of the monoidal structure of indOf.

@[instance_reducible]

noncomputable instance RS.indOfLaxMonoidal {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] : indOf.LaxMonoidal

The embedding C ⥤ Ind C is lax monoidal: the unit comparison RS.indOfUnitIso and the tensor comparison RS.indOfTensorIso satisfy the five coherences.

Equations

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

@[instance_reducible]

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

The embedding C ⥤ Ind C is strong monoidal: both comparisons are isomorphisms by construction.

Equations

• RS.indOfMonoidal = CategoryTheory.Functor.Monoidal.ofLaxMonoidal RS.indOf

@[instance_reducible]

noncomputable instance RS.indOfBraided {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : indOf.Braided

The embedding C ⥤ Ind C is braided.

Equations

• RS.indOfBraided = { toMonoidal := RS.indOfMonoidal, braided := ⋯ }

theorem RS.indOfMonoidal_εIso {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor.Monoidal.εIso indOf = indOfUnitIso

The unit comparison of the strong monoidal structure is RS.indOfUnitIso.

theorem RS.indOfMonoidal_μIso {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (x y : C) : CategoryTheory.Functor.Monoidal.μIso indOf x y = indOfTensorIso x y

The tensor comparison of the strong monoidal structure is RS.indOfTensorIso.

theorem RS.indOf_oplax_η {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor.OplaxMonoidal.η indOf = indOfUnitIso.inv

The counit of the strong monoidal structure is the inverse of RS.indOfUnitIso.

theorem RS.indOf_oplax_δ {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (x y : C) : CategoryTheory.Functor.OplaxMonoidal.δ indOf x y = (indOfTensorIso x y).inv

The cotensorator of the strong monoidal structure is the inverse of RS.indOfTensorIso.