Theorems · Theorem · category theory

CategoryTheory.LocalizerMorphism.equiv_smallHomMap

∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] {W₁ : CategoryTheory.MorphismProperty C₁} {C₂ : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₂ : CategoryTheory.MorphismProperty C₂} {D₁ : Type u₃}
  [inst_2 : CategoryTheory.Category.{v₃, u₃} D₁] {D₂ : Type u₄} [inst_3 : CategoryTheory.Category.{v₄, u₄} D₂]
  (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) [inst_4 : L₁.IsLocalization W₁]
  (L₂ : CategoryTheory.Functor C₂ D₂) [inst_5 : L₂.IsLocalization W₂] {X Y : C₁}
  [inst_6 : CategoryTheory.Localization.HasSmallLocalizedHom W₁ X Y]
  [inst_7 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)]
  (G : CategoryTheory.Functor D₁ D₂) (e : Φ.functor.comp L₂ ≅ L₁.comp G)
  (f : CategoryTheory.Localization.SmallHom W₁ X Y),
  (CategoryTheory.Localization.SmallHom.equiv W₂ L₂) (Φ.smallHomMap f) =
    CategoryTheory.CategoryStruct.comp (e.hom.app X)
      (CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.Localization.SmallHom.equiv W₁ L₁) f)) (e.inv.app Y))

Defined in

Mathlib.CategoryTheory.Localization.SmallHom

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsLocalizationCategoryTheory.Functor.IsLocalizationCategoryTheory.Localization.HasSmallLocalizedHomCategoryTheory.Localization.HasSmallLocalizedHom