Shrinking morphisms in localized categories

Given a class of morphisms W : MorphismProperty C, and two objects X and Y, we introduce a type-class HasSmallLocalizedHom.{w} W X Y which expresses that in the localized category with respect to W, the type of morphisms from X to Y is w-small for a certain universe w. Under this assumption, we define SmallHom.{w} W X Y : Type w as the shrunk type. For any localization functor L : C ⥤ D for W, we provide a bijection SmallHom.equiv.{w} W L : SmallHom.{w} W X Y ≃ (L.obj X ⟶ L.obj Y) that is compatible with the composition of morphisms.

class CategoryTheory.Localization.HasSmallLocalizedHom {C : Type u₁} [Category.{v₁, u₁} C] (W : MorphismProperty C) (X Y : C) : Prop

This property holds if the type of morphisms between X and Y in the localized category with respect to W : MorphismProperty C is small.

• small : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y)

theorem CategoryTheory.Localization.hasSmallLocalizedHom_iff {C : Type u₁} [Category.{v₁, u₁} C] (W : MorphismProperty C) {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) [L.IsLocalization W] {X Y : C} : HasSmallLocalizedHom W X Y ↔ Small.{w, v₂} (L.obj X ⟶ L.obj Y)

theorem CategoryTheory.Localization.hasSmallLocalizedHom_of_isLocalization {C : Type u₁} [Category.{v₁, u₁} C] (W : MorphismProperty C) {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) [L.IsLocalization W] {X Y : C} : HasSmallLocalizedHom W X Y

theorem CategoryTheory.Localization.small_of_hasSmallLocalizedHom {C : Type u₁} [Category.{v₁, u₁} C] (W : MorphismProperty C) {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) [L.IsLocalization W] (X Y : C) [HasSmallLocalizedHom W X Y] : Small.{w, v₂} (L.obj X ⟶ L.obj Y)

theorem CategoryTheory.Localization.hasSmallLocalizedHom_iff_of_isos {C : Type u₁} [Category.{v₁, u₁} C] (W : MorphismProperty C) {X Y X' Y' : C} (e : X ≅ X') (e' : Y ≅ Y') : HasSmallLocalizedHom W X Y ↔ HasSmallLocalizedHom W X' Y'

theorem CategoryTheory.Localization.hasSmallLocalizedHom_of_isos {C : Type u₁} [Category.{v₁, u₁} C] (W : MorphismProperty C) {X Y X' Y' : C} (e : X ≅ X') (e' : Y ≅ Y') [HasSmallLocalizedHom W X Y] : HasSmallLocalizedHom W X' Y'

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

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

def CategoryTheory.Localization.SmallHom {C : Type u₁} [Category.{v₁, u₁} C] (W : MorphismProperty C) (X Y : C) [HasSmallLocalizedHom W X Y] : Type w

The type of morphisms from X to Y in the localized category with respect to W : MorphismProperty C that is shrunk to Type w when HasSmallLocalizedHom.{w} W X Y holds.

noncomputable def CategoryTheory.Localization.SmallHom.equiv {C : Type u₁} [Category.{v₁, u₁} C] (W : MorphismProperty C) {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) [L.IsLocalization W] {X Y : C} [HasSmallLocalizedHom W X Y] : SmallHom W X Y ≃ (L.obj X ⟶ L.obj Y)

The canonical bijection SmallHom.{w} W X Y ≃ (L.obj X ⟶ L.obj Y) when L is a localization functor for W : MorphismProperty C and that HasSmallLocalizedHom.{w} W X Y holds.

theorem CategoryTheory.Localization.SmallHom.equiv_equiv_symm {C : Type u₁} [Category.{v₁, u₁} C] (W : MorphismProperty C) {D : Type u₂} [Category.{v₂, u₂} D] {D' : Type u₃} [Category.{v₃, u₃} D'] (L : Functor C D) [L.IsLocalization W] (L' : Functor C D') [L'.IsLocalization W] (G : Functor D D') (e : L.comp G ≅ L') {X Y : C} [HasSmallLocalizedHom W X Y] (f : L.obj X ⟶ L.obj Y) : (equiv W L') ((equiv W L).symm f) = CategoryStruct.comp (e.inv.app X) (CategoryStruct.comp (G.map f) (e.hom.app Y))

noncomputable def CategoryTheory.Localization.SmallHom.mk {C : Type u₁} [Category.{v₁, u₁} C] (W : MorphismProperty C) {X Y : C} [HasSmallLocalizedHom W X Y] (f : X ⟶ Y) : SmallHom W X Y

The element in SmallHom W X Y induced by f : X ⟶ Y.

@[simp]

theorem CategoryTheory.Localization.SmallHom.equiv_mk {C : Type u₁} [Category.{v₁, u₁} C] (W : MorphismProperty C) {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) [L.IsLocalization W] {X Y : C} [HasSmallLocalizedHom W X Y] (f : X ⟶ Y) : (equiv W L) (mk W f) = L.map f

noncomputable def CategoryTheory.Localization.SmallHom.mkInv {C : Type u₁} [Category.{v₁, u₁} C] {W : MorphismProperty C} {X Y : C} (f : Y ⟶ X) (hf : W f) [HasSmallLocalizedHom W X Y] : SmallHom W X Y

The formal inverse in SmallHom W X Y of a morphism f : Y ⟶ X such that W f.

@[simp]

theorem CategoryTheory.Localization.SmallHom.equiv_mkInv {C : Type u₁} [Category.{v₁, u₁} C] {W : MorphismProperty C} {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) [L.IsLocalization W] {X Y : C} (f : Y ⟶ X) (hf : W f) [HasSmallLocalizedHom W X Y] : (equiv W L) (mkInv f hf) = (isoOfHom L W f hf).inv

noncomputable def CategoryTheory.Localization.SmallHom.comp {C : Type u₁} [Category.{v₁, u₁} C] {W : MorphismProperty C} {X Y Z : C} [HasSmallLocalizedHom W X Y] [HasSmallLocalizedHom W Y Z] [HasSmallLocalizedHom W X Z] (α : SmallHom W X Y) (β : SmallHom W Y Z) : SmallHom W X Z

The composition on SmallHom W.

theorem CategoryTheory.Localization.SmallHom.equiv_comp {C : Type u₁} [Category.{v₁, u₁} C] {W : MorphismProperty C} {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) [L.IsLocalization W] {X Y Z : C} [HasSmallLocalizedHom W X Y] [HasSmallLocalizedHom W Y Z] [HasSmallLocalizedHom W X Z] (α : SmallHom W X Y) (β : SmallHom W Y Z) : (equiv W L) (α.comp β) = CategoryStruct.comp ((equiv W L) α) ((equiv W L) β)

theorem CategoryTheory.Localization.SmallHom.mk_comp_mk {C : Type u₁} [Category.{v₁, u₁} C] {W : MorphismProperty C} {X Y Z : C} [HasSmallLocalizedHom W X Y] [HasSmallLocalizedHom W Y Z] [HasSmallLocalizedHom W X Z] (f : X ⟶ Y) (g : Y ⟶ Z) : (mk W f).comp (mk W g) = mk W (CategoryStruct.comp f g)

@[simp]

theorem CategoryTheory.Localization.SmallHom.comp_mk_id {C : Type u₁} [Category.{v₁, u₁} C] {W : MorphismProperty C} {X Y : C} [HasSmallLocalizedHom W X Y] [HasSmallLocalizedHom W Y Y] (α : SmallHom W X Y) : α.comp (mk W (CategoryStruct.id Y)) = α

@[simp]

theorem CategoryTheory.Localization.SmallHom.mk_id_comp {C : Type u₁} [Category.{v₁, u₁} C] {W : MorphismProperty C} {X Y : C} [HasSmallLocalizedHom W X Y] [HasSmallLocalizedHom W X X] (α : SmallHom W X Y) : (mk W (CategoryStruct.id X)).comp α = α

@[simp]

theorem CategoryTheory.Localization.SmallHom.comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] {W : MorphismProperty C} {X Y Z T : C} [HasSmallLocalizedHom W X Y] [HasSmallLocalizedHom W X Z] [HasSmallLocalizedHom W X T] [HasSmallLocalizedHom W Y Z] [HasSmallLocalizedHom W Y T] [HasSmallLocalizedHom W Z T] (α : SmallHom W X Y) (β : SmallHom W Y Z) (γ : SmallHom W Z T) : (α.comp β).comp γ = α.comp (β.comp γ)

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Localization.SmallHom.chgUniv {C : Type u₁} [Category.{v₁, u₁} C] {W : MorphismProperty C} {X Y : C} [HasSmallLocalizedHom W X Y] [HasSmallLocalizedHom W X Y] : SmallHom W X Y ≃ SmallHom W X Y

Up to an equivalence, the type SmallHom.{w} W X Y n does not depend on the universe w.

theorem CategoryTheory.Localization.SmallHom.equiv_chgUniv {C : Type u₁} [Category.{v₁, u₁} C] {W : MorphismProperty C} {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) [L.IsLocalization W] {X Y : C} [HasSmallLocalizedHom W X Y] [HasSmallLocalizedHom W X Y] (e : SmallHom W X Y) : (equiv W L) (chgUniv e) = (equiv W L) e

noncomputable def CategoryTheory.LocalizerMorphism.smallHomMap {C₁ : Type u₁} [Category.{v₁, u₁} C₁] {W₁ : MorphismProperty C₁} {C₂ : Type u₂} [Category.{v₂, u₂} C₂] {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) {X Y : C₁} [Localization.HasSmallLocalizedHom W₁ X Y] [Localization.HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)] (f : Localization.SmallHom W₁ X Y) : Localization.SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)

The action of a localizer morphism on SmallHom.

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

@[simp]

theorem CategoryTheory.LocalizerMorphism.smallHomMap_mk {C₁ : Type u₁} [Category.{v₁, u₁} C₁] {W₁ : MorphismProperty C₁} {C₂ : Type u₂} [Category.{v₂, u₂} C₂] {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) {X Y : C₁} [Localization.HasSmallLocalizedHom W₁ X Y] [Localization.HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)] (f : X ⟶ Y) : Φ.smallHomMap (Localization.SmallHom.mk W₁ f) = Localization.SmallHom.mk W₂ (Φ.functor.map f)

theorem CategoryTheory.LocalizerMorphism.smallHomMap_comp {C₁ : Type u₁} [Category.{v₁, u₁} C₁] {W₁ : MorphismProperty C₁} {C₂ : Type u₂} [Category.{v₂, u₂} C₂] {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) {X Y Z : C₁} [Localization.HasSmallLocalizedHom W₁ X Y] [Localization.HasSmallLocalizedHom W₁ Y Z] [Localization.HasSmallLocalizedHom W₁ X Z] [Localization.HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)] [Localization.HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Z)] [Localization.HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Z)] (f : Localization.SmallHom W₁ X Y) (g : Localization.SmallHom W₁ Y Z) : Φ.smallHomMap (f.comp g) = (Φ.smallHomMap f).comp (Φ.smallHomMap g)

noncomputable def CategoryTheory.LocalizerMorphism.smallHomMap' {C₁ : Type u₁} [Category.{v₁, u₁} C₁] {W₁ : MorphismProperty C₁} {C₂ : Type u₂} [Category.{v₂, u₂} C₂] {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) {X Y : C₁} [Localization.HasSmallLocalizedHom W₁ X Y] {X' Y' : C₂} [Localization.HasSmallLocalizedHom W₂ X' X'] [Localization.HasSmallLocalizedHom W₂ X' Y'] [Localization.HasSmallLocalizedHom W₂ Y' Y'] (eX : Φ.functor.obj X ≅ X') (eY : Φ.functor.obj Y ≅ Y') (f : Localization.SmallHom W₁ X Y) : Localization.SmallHom W₂ X' Y'

The action of a localizer morphism Φ on SmallHom. In this version, we allow the replacement of objects Φ.functor.obj by isomorphic objects.

theorem CategoryTheory.LocalizerMorphism.equiv_smallHomMap' {C₁ : Type u₁} [Category.{v₁, u₁} C₁] {W₁ : MorphismProperty C₁} {C₂ : Type u₂} [Category.{v₂, u₂} C₂] {W₂ : MorphismProperty C₂} {D₁ : Type u₃} [Category.{v₃, u₃} D₁] {D₂ : Type u₄} [Category.{v₄, u₄} D₂] (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] {X Y : C₁} [Localization.HasSmallLocalizedHom W₁ X Y] {X' Y' : C₂} [Localization.HasSmallLocalizedHom W₂ X' X'] [Localization.HasSmallLocalizedHom W₂ X' Y'] [Localization.HasSmallLocalizedHom W₂ Y' Y'] (eX : Φ.functor.obj X ≅ X') (eY : Φ.functor.obj Y ≅ Y') (G : Functor D₁ D₂) (e : Φ.functor.comp L₂ ≅ L₁.comp G) (f : Localization.SmallHom W₁ X Y) : (Localization.SmallHom.equiv W₂ L₂) (Φ.smallHomMap' eX eY f) = CategoryStruct.comp (L₂.map eX.inv) (CategoryStruct.comp (e.hom.app X) (CategoryStruct.comp (G.map ((Localization.SmallHom.equiv W₁ L₁) f)) (CategoryStruct.comp (e.inv.app Y) (L₂.map eY.hom))))

@[simp]

theorem CategoryTheory.LocalizerMorphism.smallHomMap'_mk {C₁ : Type u₁} [Category.{v₁, u₁} C₁] {W₁ : MorphismProperty C₁} {C₂ : Type u₂} [Category.{v₂, u₂} C₂] {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) {X Y : C₁} [Localization.HasSmallLocalizedHom W₁ X Y] {X' Y' : C₂} [Localization.HasSmallLocalizedHom W₂ X' X'] [Localization.HasSmallLocalizedHom W₂ X' Y'] [Localization.HasSmallLocalizedHom W₂ Y' Y'] (eX : Φ.functor.obj X ≅ X') (eY : Φ.functor.obj Y ≅ Y') (f : X ⟶ Y) : Φ.smallHomMap' eX eY (Localization.SmallHom.mk W₁ f) = Localization.SmallHom.mk W₂ (CategoryStruct.comp eX.inv (CategoryStruct.comp (Φ.functor.map f) eY.hom))

theorem CategoryTheory.LocalizerMorphism.smallHomMap'_comp {C₁ : Type u₁} [Category.{v₁, u₁} C₁] {W₁ : MorphismProperty C₁} {C₂ : Type u₂} [Category.{v₂, u₂} C₂] {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) {X Y Z : C₁} [Localization.HasSmallLocalizedHom W₁ X Y] [Localization.HasSmallLocalizedHom W₁ Y Z] [Localization.HasSmallLocalizedHom W₁ X Z] {X' Y' Z' : C₂} [Localization.HasSmallLocalizedHom W₂ X' X'] [Localization.HasSmallLocalizedHom W₂ Y' Y'] [Localization.HasSmallLocalizedHom W₂ Z' Z'] [Localization.HasSmallLocalizedHom W₂ X' Y'] [Localization.HasSmallLocalizedHom W₂ Y' Z'] [Localization.HasSmallLocalizedHom W₂ X' Z'] (eX : Φ.functor.obj X ≅ X') (eY : Φ.functor.obj Y ≅ Y') (eZ : Φ.functor.obj Z ≅ Z') (f : Localization.SmallHom W₁ X Y) (g : Localization.SmallHom W₁ Y Z) : Φ.smallHomMap' eX eZ (f.comp g) = (Φ.smallHomMap' eX eY f).comp (Φ.smallHomMap' eY eZ g)