Theorems · Theorem · category theory

CommRingCat.Colimits.cocone_naturality_components

∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) (j j' : J)
  (f : j ⟶ j') (x : ↑(F.obj j)),
  (CategoryTheory.ConcreteCategory.hom (CommRingCat.Colimits.coconeMorphism F j'))
      ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) =
    (CategoryTheory.ConcreteCategory.hom (CommRingCat.Colimits.coconeMorphism F j)) x

Defined in

Mathlib.Algebra.Category.Ring.Colimits

Cited by

0 results in Mathlib

Foundations

Depth 39 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.SmallCategory