Theorems · Theorem · category theory

CategoryTheory.Under.mapComp_eq

∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.Under.map (CategoryTheory.CategoryStruct.comp f g) =
    (CategoryTheory.Under.map g).comp (CategoryTheory.Under.map f)

Mapping by the composite morphism f ≫ g is the same as mapping by f then by g.

Defined in

Mathlib.CategoryTheory.Comma.Over.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category