Theorems · Definition · category theory

CategoryTheory.LocalizerMorphism.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₂} →
            (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) →
              {X Y : C₁} →
                [inst_2 : CategoryTheory.Localization.HasSmallLocalizedHom W₁ X Y] →
                  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)] →
                    CategoryTheory.Localization.SmallHom W₁ X Y →
                      CategoryTheory.Localization.SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)

The action of a localizer morphism on SmallHom.

Defined in

Mathlib.CategoryTheory.Localization.SmallHom

Cited by

5 results in Mathlib

Foundations

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

Assumes

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