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 : C)
(Y : C)
:
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)
Instances
theorem
CategoryTheory.Localization.HasSmallLocalizedHom.small
{C : Type u₁}
:
∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {W : CategoryTheory.MorphismProperty C} {X Y : C}
[self : CategoryTheory.Localization.HasSmallLocalizedHom W X Y], 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 : C}
{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 : C}
{Y : C}
:
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 : C)
(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 : C}
{Y : C}
{X' : C}
{Y' : C}
(e : X ≅ X')
(e' : Y ≅ Y')
:
theorem
CategoryTheory.Localization.hasSmallLocalizedHom_iff_target
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(W : CategoryTheory.MorphismProperty C)
(X : C)
{Y : C}
{Y' : C}
(f : Y ⟶ Y')
(hf : W f)
:
theorem
CategoryTheory.Localization.hasSmallLocalizedHom_iff_source
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(W : CategoryTheory.MorphismProperty C)
{X : C}
{X' : C}
(f : X ⟶ X')
(hf : W f)
(Y : C)
:
def
CategoryTheory.Localization.SmallHom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(W : CategoryTheory.MorphismProperty C)
(X : C)
(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)
Instances For
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 : C}
{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)
Instances For
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 : C}
{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 : C}
{Y : C}
[CategoryTheory.Localization.HasSmallLocalizedHom W X Y]
(f : 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)
Instances For
@[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 : C}
{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 : C}
{Y : C}
(f : Y ⟶ X)
(hf : W f)
[CategoryTheory.Localization.HasSmallLocalizedHom 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
Instances For
@[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 : C}
{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 : C}
{Y : C}
{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)
:
The composition on SmallHom W.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 : C}
{Y : C}
{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 : C}
{Y : C}
{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)
:
@[simp]
theorem
CategoryTheory.Localization.SmallHom.comp_mk_id
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{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 : C}
{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 : C}
{Y : C}
{Z : C}
{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 : C}
{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)
:
@[simp]
theorem
CategoryTheory.Localization.SmallHom.mkInv_comp_mk
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{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)
:
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 : C₁}
{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.
Instances For
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 : C₁}
{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 : C₁}
{Y : C₁}
{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)