Theorems · Definition · category theory

CategoryTheory.IsMonHom.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.GrpObj G] →
          [inst_3 : CategoryTheory.GrpObj H] →
            {φ : H ⟶ G} →
              {motive : CategoryTheory.IsMonHom.Normal φ → Sort u} →
                (t : CategoryTheory.IsMonHom.Normal φ) →
                  ((mono : CategoryTheory.Mono φ) →
                      (isMonHom : CategoryTheory.IsMonHom φ) →
                        (exists_comp_eq_conj :
                            ∃ ψ,
                              CategoryTheory.CategoryStruct.comp ψ φ =
                                CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G φ)
                                  (CategoryTheory.GrpObj.conj 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.GrpObjCategoryTheory.GrpObj