Theorems · Definition · category theory

CategoryTheory.RingObj.casesOn

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {R : C} →
          {motive : CategoryTheory.RingObj R → Sort u_1} →
            (t : CategoryTheory.RingObj R) →
              ([toAddGrpObj : CategoryTheory.AddGrpObj R] →
                  [toIsCommAddMonObj : CategoryTheory.IsCommAddMonObj R] →
                    [toMonObj : CategoryTheory.MonObj R] →
                      (mul_add :
                          CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R CategoryTheory.AddMonObj.add)
                              CategoryTheory.MonObj.mul =
                            CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.CartesianMonoidalCategory.lift
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R
                                    (CategoryTheory.SemiCartesianMonoidalCategory.fst R R))
                                  CategoryTheory.MonObj.mul)
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R
                                    (CategoryTheory.SemiCartesianMonoidalCategory.snd R R))
                                  CategoryTheory.MonObj.mul))
                              CategoryTheory.AddMonObj.add) →
                        (add_mul :
                            CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add R)
                                CategoryTheory.MonObj.mul =
                              CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.CartesianMonoidalCategory.lift
                                  (CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.MonoidalCategoryStruct.whiskerRight
                                      (CategoryTheory.SemiCartesianMonoidalCategory.fst R R) R)
                                    CategoryTheory.MonObj.mul)
                                  (CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.MonoidalCategoryStruct.whiskerRight
                                      (CategoryTheory.SemiCartesianMonoidalCategory.snd R R) R)
                                    CategoryTheory.MonObj.mul))
                                CategoryTheory.AddMonObj.add) →
                          motive
                            { toAddGrpObj := toAddGrpObj, toIsCommAddMonObj := toIsCommAddMonObj, toMonObj := toMonObj,
                              mul_add := mul_add, add_mul := add_mul }) →
                motive t

Defined in

Mathlib.CategoryTheory.Monoidal.Ring

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CartesianMonoidalCategoryCategoryTheory.BraidedCategory