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₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) [L.IsLocalization W] {X Y : C} : CategoryTheory.Localization.HasSmallLocalizedHom W X Y ↔ Small.{w, v₂} (L.obj X ⟶ L.obj Y)

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

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

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

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

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

def CategoryTheory.Localization.SmallHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) (X Y : C) [CategoryTheory.Localization.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.

Equations

• CategoryTheory.Localization.SmallHom W X Y = Shrink.{?u.44, max ?u.42 ?u.43} (W.Q.obj X ⟶ W.Q.obj Y)

noncomputable def CategoryTheory.Localization.SmallHom.equiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) [L.IsLocalization W] {X Y : C} [CategoryTheory.Localization.HasSmallLocalizedHom W X Y] : CategoryTheory.Localization.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.

Equations

• CategoryTheory.Localization.SmallHom.equiv W L = (equivShrink (W.Q.obj X ⟶ W.Q.obj Y)).symm.trans (CategoryTheory.Localization.homEquiv W W.Q L)

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

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

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

Equations

• CategoryTheory.Localization.SmallHom.mk W f = (CategoryTheory.Localization.SmallHom.equiv W W.Q).symm (W.Q.map f)

@[simp]

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

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

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

Equations

• CategoryTheory.Localization.SmallHom.mkInv f hf = (CategoryTheory.Localization.SmallHom.equiv W W.Q).symm (CategoryTheory.Localization.isoOfHom W.Q W f hf).inv

@[simp]

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

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

The composition on SmallHom W.

Equations

• One or more equations did not get rendered due to their size.

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The action of a localizer morphism on SmallHom.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.LocalizerMorphism.equiv_smallHomMap {C₁ : Type u₁} [CategoryTheory.Category.{v₁, u₁} C₁] {W₁ : CategoryTheory.MorphismProperty C₁} {C₂ : Type u₂} [CategoryTheory.Category.{v₂, u₂} C₂] {W₂ : CategoryTheory.MorphismProperty C₂} {D₁ : Type u₃} [CategoryTheory.Category.{v₃, u₃} D₁] {D₂ : Type u₄} [CategoryTheory.Category.{v₄, u₄} D₂] (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] {X Y : C₁} [CategoryTheory.Localization.HasSmallLocalizedHom W₁ X Y] [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))

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