Theorems · Theorem · category theory

CategoryTheory.Subobject.ofMkLEMk_comp_ofMkLE_assoc

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ A₂ : C} (f : A₁ ⟶ B) [inst_1 : CategoryTheory.Mono f]
  (g : A₂ ⟶ B) [inst_2 : CategoryTheory.Mono g] (X : CategoryTheory.Subobject B)
  (h₁ : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g) (h₂ : CategoryTheory.Subobject.mk g ≤ X) {Z : C}
  (h : CategoryTheory.Subobject.underlying.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLEMk f g h₁)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLE g X h₂) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLE f X ⋯) h

Defined in

Mathlib.CategoryTheory.Subobject.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoCategoryTheory.Mono