Shrinking morphisms in localized categories equipped with shifts

If C is a category equipped with a shift by an additive monoid M, and W : MorphismProperty C is compatible with the shift, we define a type-class HasSmallLocalizedShiftedHom.{w} W X Y which says that all the types of morphisms from X⟦a⟧ to Y⟦b⟧ in the localized category are w-small for a certain universe. Then, we define types SmallShiftedHom.{w} W X Y m : Type w for all m : M, and endow these with a composition which transports the composition on the types ShiftedHom (L.obj X) (L.obj Y) m when L : C ⥤ D is any localization functor for W.

@[reducible, inline]

abbrev CategoryTheory.Localization.HasSmallLocalizedShiftedHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) (M : Type w') [AddMonoid M] [CategoryTheory.HasShift C M] (X Y : C) : Prop

Given objects X and Y in a category C, this is the property that all the types of morphisms from X⟦a⟧ to Y⟦b⟧ are w-small in the localized category with respect to a class of morphisms W.

Equations

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

theorem CategoryTheory.Localization.hasSmallLocalizedShiftedHom_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (W : CategoryTheory.MorphismProperty C) (M : Type w') [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.HasShift D M] (L : CategoryTheory.Functor C D) [L.IsLocalization W] [L.CommShift M] (X Y : C) : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y ↔ ∀ (a b : M), Small.{w, v₂} ((CategoryTheory.shiftFunctor D a).obj (L.obj X) ⟶ (CategoryTheory.shiftFunctor D b).obj (L.obj Y))

theorem CategoryTheory.Localization.hasSmallLocalizedShiftedHom_iff_target {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) (M : Type w') [AddMonoid M] [CategoryTheory.HasShift C M] (X : C) {Y : C} [W.IsCompatibleWithShift M] {Y' : C} (f : Y ⟶ Y') (hf : W f) : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y ↔ CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y'

theorem CategoryTheory.Localization.hasSmallLocalizedShiftedHom_iff_source {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) (M : Type w') [AddMonoid M] [CategoryTheory.HasShift C M] {X : C} [W.IsCompatibleWithShift M] {X' : C} (f : X ⟶ X') (hf : W f) (Y : C) : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y ↔ CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X' Y

theorem CategoryTheory.Localization.hasSmallLocalizedHom_of_hasSmallLocalizedShiftedHom₀ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) (M : Type w') [AddMonoid M] [CategoryTheory.HasShift C M] (X Y : C) [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] : CategoryTheory.Localization.HasSmallLocalizedHom W X Y

instance CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {M : Type w'} [AddMonoid M] [CategoryTheory.HasShift C M] (X Y : C) [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] (m : M) : CategoryTheory.Localization.HasSmallLocalizedHom W X ((CategoryTheory.shiftFunctor C m).obj Y)

instance CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor_1 {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {M : Type w'} [AddMonoid M] [CategoryTheory.HasShift C M] (X Y : C) [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] (m : M) : CategoryTheory.Localization.HasSmallLocalizedHom W ((CategoryTheory.shiftFunctor C m).obj X) Y

instance CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor_2 {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {M : Type w'} [AddMonoid M] [CategoryTheory.HasShift C M] (X Y : C) [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] (m m' n : M) : CategoryTheory.Localization.HasSmallLocalizedHom W ((CategoryTheory.shiftFunctor C m').obj ((CategoryTheory.shiftFunctor C m).obj X)) ((CategoryTheory.shiftFunctor C n).obj Y)

instance CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor_3 {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {M : Type w'} [AddMonoid M] [CategoryTheory.HasShift C M] (X Y : C) [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] (m n n' : M) : CategoryTheory.Localization.HasSmallLocalizedHom W ((CategoryTheory.shiftFunctor C m).obj X) ((CategoryTheory.shiftFunctor C n').obj ((CategoryTheory.shiftFunctor C n).obj Y))

noncomputable def CategoryTheory.Localization.SmallHom.shift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {M : Type w'} [AddMonoid M] [CategoryTheory.HasShift C M] [W.IsCompatibleWithShift M] {X Y : C} [CategoryTheory.Localization.HasSmallLocalizedHom W X Y] (f : CategoryTheory.Localization.SmallHom W X Y) (a : M) [CategoryTheory.Localization.HasSmallLocalizedHom W ((CategoryTheory.shiftFunctor C a).obj X) ((CategoryTheory.shiftFunctor C a).obj Y)] : CategoryTheory.Localization.SmallHom W ((CategoryTheory.shiftFunctor C a).obj X) ((CategoryTheory.shiftFunctor C a).obj Y)

Given f : SmallHom W X Y and a : M, this is the element in SmallHom W (X⟦a⟧) (Y⟦a⟧) obtained by shifting by a.

Equations

• f.shift a = (W.shiftLocalizerMorphism a).smallHomMap f

theorem CategoryTheory.Localization.SmallHom.equiv_shift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {W : CategoryTheory.MorphismProperty C} {M : Type w'} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.HasShift D M] [W.IsCompatibleWithShift M] (L : CategoryTheory.Functor C D) [L.IsLocalization W] [L.CommShift M] {X Y : C} [CategoryTheory.Localization.HasSmallLocalizedHom W X Y] (f : CategoryTheory.Localization.SmallHom W X Y) (a : M) [CategoryTheory.Localization.HasSmallLocalizedHom W ((CategoryTheory.shiftFunctor C a).obj X) ((CategoryTheory.shiftFunctor C a).obj Y)] : (CategoryTheory.Localization.SmallHom.equiv W L) (f.shift a) = CategoryTheory.CategoryStruct.comp ((L.commShiftIso a).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map ((CategoryTheory.Localization.SmallHom.equiv W L) f)) ((L.commShiftIso a).inv.app Y))

def CategoryTheory.Localization.SmallShiftedHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {M : Type w'} [AddMonoid M] [CategoryTheory.HasShift C M] (X Y : C) [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] (m : M) : Type w

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

Equations

• CategoryTheory.Localization.SmallShiftedHom W X Y m = CategoryTheory.Localization.SmallHom W X ((CategoryTheory.shiftFunctor C m).obj Y)

noncomputable def CategoryTheory.Localization.SmallShiftedHom.shift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {M : Type w'} [AddMonoid M] [CategoryTheory.HasShift C M] [W.IsCompatibleWithShift M] {X Y : C} {a : M} [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Y] (f : CategoryTheory.Localization.SmallShiftedHom W X Y a) (n a' : M) (h : a + n = a') : CategoryTheory.Localization.SmallHom W ((CategoryTheory.shiftFunctor C n).obj X) ((CategoryTheory.shiftFunctor C a').obj Y)

Given f : SmallShiftedHom.{w} W X Y a, this is the element in SmallHom.{w} W (X⟦n⟧) (Y⟦a'⟧) that is obtained by shifting by n when a + n = a'.

Equations

• f.shift n a' h = (CategoryTheory.Localization.SmallHom.shift f n).comp (CategoryTheory.Localization.SmallHom.mk W ((CategoryTheory.shiftFunctorAdd' C a n a' h).inv.app Y))

noncomputable def CategoryTheory.Localization.SmallShiftedHom.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {M : Type w'} [AddMonoid M] [CategoryTheory.HasShift C M] [W.IsCompatibleWithShift M] {X Y Z : C} {a b c : M} [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Z] [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Z] [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z Z] (f : CategoryTheory.Localization.SmallShiftedHom W X Y a) (g : CategoryTheory.Localization.SmallShiftedHom W Y Z b) (h : b + a = c) : CategoryTheory.Localization.SmallShiftedHom W X Z c

The composition on SmallShiftedHom W.

Equations

• f.comp g h = CategoryTheory.Localization.SmallHom.comp f (g.shift a c h)

noncomputable def CategoryTheory.Localization.SmallShiftedHom.mk₀ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {M : Type w'} [AddMonoid M] [CategoryTheory.HasShift C M] {X Y : C} [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) : CategoryTheory.Localization.SmallShiftedHom W X Y m₀

The canonical map (X ⟶ Y) → SmallShiftedHom.{w} W X Y m₀ when m₀ = 0 and [HasSmallLocalizedShiftedHom.{w} W M X Y] holds.

Equations

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

noncomputable def CategoryTheory.Localization.SmallShiftedHom.equiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (W : CategoryTheory.MorphismProperty C) {M : Type w'} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.HasShift D M] (L : CategoryTheory.Functor C D) [L.IsLocalization W] [L.CommShift M] {X Y : C} [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] {m : M} : CategoryTheory.Localization.SmallShiftedHom W X Y m ≃ CategoryTheory.ShiftedHom (L.obj X) (L.obj Y) m

The bijection SmallShiftedHom.{w} W X Y m ≃ ShiftedHom (L.obj X) (L.obj Y) m for all m : M, and X and Y in C when L : C ⥤ D is a localization functor for W : MorphismProperty C such that the category D is equipped with a shift by M and L commutes with the shifts.

Equations

• CategoryTheory.Localization.SmallShiftedHom.equiv W L = (CategoryTheory.Localization.SmallHom.equiv W L).trans ((L.commShiftIso m).app Y).homToEquiv

theorem CategoryTheory.Localization.SmallShiftedHom.equiv_shift' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (W : CategoryTheory.MorphismProperty C) {M : Type w'} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.HasShift D M] (L : CategoryTheory.Functor C D) [L.IsLocalization W] [L.CommShift M] {X Y : C} [W.IsCompatibleWithShift M] {a : M} [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Y] (f : CategoryTheory.Localization.SmallShiftedHom W X Y a) (n a' : M) (h : a + n = a') : (CategoryTheory.Localization.SmallHom.equiv W L) (f.shift n a' h) = CategoryTheory.CategoryStruct.comp ((L.commShiftIso n).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D n).map ((CategoryTheory.Localization.SmallHom.equiv W L) f)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D n).map ((L.commShiftIso a).hom.app Y)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)) ((L.commShiftIso a').inv.app Y))))

theorem CategoryTheory.Localization.SmallShiftedHom.equiv_shift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (W : CategoryTheory.MorphismProperty C) {M : Type w'} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.HasShift D M] (L : CategoryTheory.Functor C D) [L.IsLocalization W] [L.CommShift M] {X Y : C} [W.IsCompatibleWithShift M] {a : M} [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Y] (f : CategoryTheory.Localization.SmallShiftedHom W X Y a) (n a' : M) (h : a + n = a') : (CategoryTheory.Localization.SmallShiftedHom.equiv W L) (f.shift n a' h) = CategoryTheory.CategoryStruct.comp ((L.commShiftIso n).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D n).map ((CategoryTheory.Localization.SmallShiftedHom.equiv W L) f)) ((CategoryTheory.shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)))

theorem CategoryTheory.Localization.SmallShiftedHom.equiv_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (W : CategoryTheory.MorphismProperty C) {M : Type w'} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.HasShift D M] (L : CategoryTheory.Functor C D) [L.IsLocalization W] [L.CommShift M] {X Y Z : C} [W.IsCompatibleWithShift M] [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Z] [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Z] [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z Z] {a b c : M} (f : CategoryTheory.Localization.SmallShiftedHom W X Y a) (g : CategoryTheory.Localization.SmallShiftedHom W Y Z b) (h : b + a = c) : (CategoryTheory.Localization.SmallShiftedHom.equiv W L) (f.comp g h) = ((CategoryTheory.Localization.SmallShiftedHom.equiv W L) f).comp ((CategoryTheory.Localization.SmallShiftedHom.equiv W L) g) h

@[simp]

theorem CategoryTheory.Localization.SmallShiftedHom.equiv_mk₀ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (W : CategoryTheory.MorphismProperty C) {M : Type w'} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.HasShift D M] (L : CategoryTheory.Functor C D) [L.IsLocalization W] [L.CommShift M] {X Y : C} [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) : (CategoryTheory.Localization.SmallShiftedHom.equiv W L) (CategoryTheory.Localization.SmallShiftedHom.mk₀ W m₀ hm₀ f) = CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ (L.map f)

theorem CategoryTheory.Localization.SmallShiftedHom.comp_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {M : Type w'} [AddMonoid M] [CategoryTheory.HasShift C M] [W.IsCompatibleWithShift M] {X Y Z T : C} {a₁ a₂ a₃ a₁₂ a₂₃ a : M} [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Z] [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X T] [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Z] [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y T] [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z T] [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z Z] [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M T T] (α : CategoryTheory.Localization.SmallShiftedHom W X Y a₁) (β : CategoryTheory.Localization.SmallShiftedHom W Y Z a₂) (γ : CategoryTheory.Localization.SmallShiftedHom W Z T a₃) (h₁₂ : a₂ + a₁ = a₁₂) (h₂₃ : a₃ + a₂ = a₂₃) (h : a₃ + a₂ + a₁ = a) : (α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ h₂₃) ⋯

noncomputable def CategoryTheory.Localization.SmallShiftedHom.chgUniv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {M : Type w'} [AddMonoid M] [CategoryTheory.HasShift C M] {X Y : C} {m : M} [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] : CategoryTheory.Localization.SmallShiftedHom W X Y m ≃ CategoryTheory.Localization.SmallShiftedHom W X Y m

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

Equations

• CategoryTheory.Localization.SmallShiftedHom.chgUniv = CategoryTheory.Localization.SmallHom.chgUniv

theorem CategoryTheory.Localization.SmallShiftedHom.equiv_chgUniv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {W : CategoryTheory.MorphismProperty C} {M : Type w'} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.HasShift D M] (L : CategoryTheory.Functor C D) [L.IsLocalization W] [L.CommShift M] {X Y : C} {m : M} [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] (e : CategoryTheory.Localization.SmallShiftedHom W X Y m) : (CategoryTheory.Localization.SmallShiftedHom.equiv W L) (CategoryTheory.Localization.SmallShiftedHom.chgUniv e) = (CategoryTheory.Localization.SmallShiftedHom.equiv W L) e