Theorems · Definition · category theory

CategoryTheory.LocalizerMorphism.homMap

{C₁ : Type u_2} →
  {C₂ : Type u_3} →
    {D₁ : Type u_5} →
      {D₂ : Type u_6} →
        [inst : CategoryTheory.Category.{v_2, u_2} C₁] →
          [inst_1 : CategoryTheory.Category.{v_3, u_3} C₂] →
            [inst_2 : CategoryTheory.Category.{v_5, u_5} D₁] →
              [inst_3 : CategoryTheory.Category.{v_6, u_6} D₂] →
                {W₁ : CategoryTheory.MorphismProperty C₁} →
                  {W₂ : CategoryTheory.MorphismProperty C₂} →
                    (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) →
                      (L₁ : CategoryTheory.Functor C₁ D₁) →
                        [L₁.IsLocalization W₁] →
                          (L₂ : CategoryTheory.Functor C₂ D₂) →
                            [L₂.IsLocalization W₂] →
                              {X Y : C₁} → (L₁.obj X ⟶ L₁.obj Y) → (L₂.obj (Φ.functor.obj X) ⟶ L₂.obj (Φ.functor.obj Y))

If Φ : LocalizerMorphism W₁ W₂ is a morphism of localizers, L₁ and L₂ are localization functors for W₁ and W₂, then this is the induced map (L₁.obj X ⟶ L₁.obj Y) ⟶ (L₂.obj (Φ.functor.obj X) ⟶ L₂.obj (Φ.functor.obj Y)) for all objects X and Y.

Defined in

Mathlib.CategoryTheory.Localization.HomEquiv

Cited by

10 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsLocalizationCategoryTheory.Functor.IsLocalization