Theorems · Definition · category theory

CategoryTheory.IsAddMonHom.Normal.recOn

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {G H : C} →
        [inst_2 : CategoryTheory.AddGrpObj G] →
          [inst_3 : CategoryTheory.AddGrpObj H] →
            {φ : H ⟶ G} →
              {motive : CategoryTheory.IsAddMonHom.Normal φ → Sort u} →
                (t : CategoryTheory.IsAddMonHom.Normal φ) →
                  ((mono : CategoryTheory.Mono φ) →
                      (isAddMonHom : CategoryTheory.IsAddMonHom φ) →
                        (exists_comp_eq_addConj :
                            ∃ ψ,
                              CategoryTheory.CategoryStruct.comp ψ φ =
                                CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G φ)
                                  (CategoryTheory.AddGrpObj.addConj G)) →
                          motive ⋯) →
                    motive t

Defined in

Mathlib.CategoryTheory.Monoidal.Cartesian.Normal

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CartesianMonoidalCategoryCategoryTheory.AddGrpObjCategoryTheory.AddGrpObj