Theorems · Theorem · category theory

CategoryTheory.Subobject.map_comp

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Mono f] [inst_2 : CategoryTheory.Mono g] (x : CategoryTheory.Subobject X),
  (CategoryTheory.Subobject.map (CategoryTheory.CategoryStruct.comp f g)).obj x =
    (CategoryTheory.Subobject.map g).obj ((CategoryTheory.Subobject.map f).obj x)

Defined in

Mathlib.CategoryTheory.Subobject.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoCategoryTheory.Mono