Theorems · Theorem · category theory

CategoryTheory.Localization.SmallHom.mkInv_comp_mk

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  [inst_1 : CategoryTheory.Localization.HasSmallLocalizedHom W X X]
  [inst_2 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y]
  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedHom W Y X] (f : Y ⟶ X) (hf : W f),
  (CategoryTheory.Localization.SmallHom.mkInv f hf).comp (CategoryTheory.Localization.SmallHom.mk W f) =
    CategoryTheory.Localization.SmallHom.mk W (CategoryTheory.CategoryStruct.id X)

Defined in

Mathlib.CategoryTheory.Localization.SmallHom

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Localization.HasSmallLocalizedHomCategoryTheory.Localization.HasSmallLocalizedHomCategoryTheory.Localization.HasSmallLocalizedHom