Theorems · Definition · category theory

CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.mk.noConfusion

{C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {V : Type u₂} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} V} →
        {inst_2 : CategoryTheory.MonoidalCategory C} →
          {inst_3 : CategoryTheory.MonoidalCategory V} →
            {D : Type u₃} →
              {inst_4 : CategoryTheory.Category.{v₃, u₃} D} →
                {P : Sort u} →
                  {ι : CategoryTheory.Functor D (CategoryTheory.Functor C V)} →
                    {fullyFaithulι : ι.FullyFaithful} →
                      {tensorObj : D → D → D} →
                        {convolutions' :
                            (d d' : D) → CategoryTheory.MonoidalCategory.DayConvolution (ι.obj d) (ι.obj d')} →
                          {tensorObjIsoConvolution :
                              (d d' : D) →
                                ι.obj (tensorObj d d') ≅
                                  CategoryTheory.MonoidalCategory.DayConvolution.convolution (ι.obj d) (ι.obj d')} →
                            {convolutionUnitApp :
                                (d d' : D) →
                                  (x y : C) →
                                    CategoryTheory.MonoidalCategoryStruct.tensorObj ((ι.obj d).obj x)
                                        ((ι.obj d').obj y) ⟶
                                      (ι.obj (tensorObj d d')).obj
                                        (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)} →
                              {convolutionUnitApp_eq :
                                  autoParam
                                    (∀ (d d' : D) (x y : C),
                                      convolutionUnitApp d d' x y =
                                        CategoryTheory.CategoryStruct.comp
                                          ((CategoryTheory.MonoidalCategory.DayConvolution.unit (ι.obj d)
                                                (ι.obj d')).app
                                            (x, y))
                                          ((tensorObjIsoConvolution d d').inv.app
                                            (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)))
                                    CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.convolutionUnitApp_eq._autoParam} →
                                {tensorHom :
                                    {d₁ d₂ d₁' d₂' : D} →
                                      (d₁ ⟶ d₂) → (d₁' ⟶ d₂') → (tensorObj d₁ d₁' ⟶ tensorObj d₂ d₂')} →
                                  {tensorHom_eq :
                                      autoParam
                                        (∀ {d₁ d₂ d₁' d₂' : D} (f : d₁ ⟶ d₂) (f' : d₁' ⟶ d₂'),
                                          ι.map (tensorHom f f') =
                                            CategoryTheory.CategoryStruct.comp (tensorObjIsoConvolution d₁ d₁').hom
                                              (CategoryTheory.CategoryStruct.comp
                                                (CategoryTheory.MonoidalCategory.DayConvolution.map (ι.map f)
                                                  (ι.map f'))
                                                (tensorObjIsoConvolution d₂ d₂').inv))
                                        CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorHom_eq._autoParam} →
                                    {tensorUnit : D} →
                                      {tensorUnitConvolutionUnit :
                                          CategoryTheory.MonoidalCategory.DayConvolutionUnit (ι.obj tensorUnit)} →
                                        {ι' : CategoryTheory.Functor D (CategoryTheory.Functor C V)} →
                                          {fullyFaithulι' : ι'.FullyFaithful} →
                                            {tensorObj' : D → D → D} →
                                              {convolutions'' :
                                                  (d d' : D) →
                                                    CategoryTheory.MonoidalCategory.DayConvolution (ι'.obj d)
                                                      (ι'.obj d')} →
                                                {tensorObjIsoConvolution' :
                                                    (d d' : D) →
                                                      ι'.obj (tensorObj' d d') ≅
                                                        CategoryTheory.MonoidalCategory.DayConvolution.convolution
                                                          (ι'.obj d) (ι'.obj d')} →
                                                  {convolutionUnitApp' :
                                                      (d d' : D) →
                                                        (x y : C) →
                                                          CategoryTheory.MonoidalCategoryStruct.tensorObj
                                                              ((ι'.obj d).obj x) ((ι'.obj d').obj y) ⟶
                                                            (ι'.obj (tensorObj' d d')).obj
                                                              (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)} →
                                                    {convolutionUnitApp_eq' :
                                                        autoParam
                                                          (∀ (d d' : D) (x y : C),
                                                            convolutionUnitApp' d d' x y =
                                                              CategoryTheory.CategoryStruct.comp
                                                                ((CategoryTheory.MonoidalCategory.DayConvolution.unit
                                                                      (ι'.obj d) (ι'.obj d')).app
                                                                  (x, y))
                                                                ((tensorObjIsoConvolution' d d').inv.app
                                                                  (CategoryTheory.MonoidalCategoryStruct.tensorObj x
                                                                    y)))
                                                          CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.convolutionUnitApp_eq._autoParam} →
                                                      {tensorHom' :
                                                          {d₁ d₂ d₁' d₂' : D} →
                                                            (d₁ ⟶ d₂) →
                                                              (d₁' ⟶ d₂') → (tensorObj' d₁ d₁' ⟶ tensorObj' d₂ d₂')} →
                                                        {tensorHom_eq' :
                                                            autoParam
                                                              (∀ {d₁ d₂ d₁' d₂' : D} (f : d₁ ⟶ d₂) (f' : d₁' ⟶ d₂'),
                                                                ι'.map (tensorHom' f f') =
                                                                  CategoryTheory.CategoryStruct.comp
                                                                    (tensorObjIsoConvolution' d₁ d₁').hom
                                                                    (CategoryTheory.CategoryStruct.comp
                                                                      (CategoryTheory.MonoidalCategory.DayConvolution.map
                                                                        (ι'.map f) (ι'.map f'))
                                                                      (tensorObjIsoConvolution' d₂ d₂').inv))
                                                              CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorHom_eq._autoParam} →
                                                          {tensorUnit' : D} →
                                                            {tensorUnitConvolutionUnit' :
                                                                CategoryTheory.MonoidalCategory.DayConvolutionUnit
                                                                  (ι'.obj tensorUnit')} →
                                                              { ι := ι, fullyFaithulι := fullyFaithulι,
                                                                    tensorObj := tensorObj,
                                                                    convolutions' := convolutions',
                                                                    tensorObjIsoConvolution := tensorObjIsoConvolution,
                                                                    convolutionUnitApp := convolutionUnitApp,
                                                                    convolutionUnitApp_eq := convolutionUnitApp_eq,
                                                                    tensorHom := tensorHom,
                                                                    tensorHom_eq := tensorHom_eq,
                                                                    tensorUnit := tensorUnit,
                                                                    tensorUnitConvolutionUnit :=
                                                                      tensorUnitConvolutionUnit } =
                                                                  { ι := ι', fullyFaithulι := fullyFaithulι',
                                                                    tensorObj := tensorObj',
                                                                    convolutions' := convolutions'',
                                                                    tensorObjIsoConvolution := tensorObjIsoConvolution',
                                                                    convolutionUnitApp := convolutionUnitApp',
                                                                    convolutionUnitApp_eq := convolutionUnitApp_eq',
                                                                    tensorHom := tensorHom',
                                                                    tensorHom_eq := tensorHom_eq',
                                                                    tensorUnit := tensorUnit',
                                                                    tensorUnitConvolutionUnit :=
                                                                      tensorUnitConvolutionUnit' } →
                                                                (ι ≍ ι' →
                                                                    fullyFaithulι ≍ fullyFaithulι' →
                                                                      tensorObj ≍ tensorObj' →
                                                                        convolutions' ≍ convolutions'' →
                                                                          tensorObjIsoConvolution ≍
                                                                              tensorObjIsoConvolution' →
                                                                            convolutionUnitApp ≍ convolutionUnitApp' →
                                                                              tensorHom ≍ tensorHom' →
                                                                                tensorUnit ≍ tensorUnit' →
                                                                                  tensorUnitConvolutionUnit ≍
                                                                                      tensorUnitConvolutionUnit' →
                                                                                    P) →
                                                                  P

Defined in

Mathlib.CategoryTheory.Monoidal.DayConvolution

Cited by

0 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Classical.choice, Quot.sound