Theorems · Theorem · category theory

CategoryTheory.Localization.hasSmallLocalizedHom_iff_target

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) (X : C) {Y Y' : C}
  (f : Y ⟶ Y'),
  W f →
    (CategoryTheory.Localization.HasSmallLocalizedHom W X Y ↔ CategoryTheory.Localization.HasSmallLocalizedHom W X Y')

Defined in

Mathlib.CategoryTheory.Localization.SmallHom

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category