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 : C)
(Y : C)
:
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.
Instances For
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 : C)
(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)
:
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)
:
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 : C)
(Y : C)
[CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M 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 : C)
(Y : C)
[CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
(m : M)
:
CategoryTheory.Localization.HasSmallLocalizedHom W X ((CategoryTheory.shiftFunctor C m).obj Y)
Equations
- ⋯ = ⋯
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 : C)
(Y : C)
[CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
(m : M)
:
CategoryTheory.Localization.HasSmallLocalizedHom W ((CategoryTheory.shiftFunctor C m).obj X) Y
Equations
- ⋯ = ⋯
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 : C)
(Y : C)
[CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
(m : M)
(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)
Equations
- ⋯ = ⋯
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 : C)
(Y : C)
[CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
(m : M)
(n : M)
(n' : M)
:
CategoryTheory.Localization.HasSmallLocalizedHom W ((CategoryTheory.shiftFunctor C m).obj X)
((CategoryTheory.shiftFunctor C n').obj ((CategoryTheory.shiftFunctor C n).obj Y))
Equations
- ⋯ = ⋯
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 : C}
{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
Instances For
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 : C}
{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 : C)
(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)
Instances For
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 : C}
{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 : M)
(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))
Instances For
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 : C}
{Y : C}
{Z : C}
{a : M}
{b : M}
{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)
:
The composition on SmallShiftedHom W.
Equations
- f.comp g h = CategoryTheory.Localization.SmallHom.comp f (g.shift a c h)
Instances For
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 : C}
{Y : C}
[CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
(m₀ : M)
(hm₀ : m₀ = 0)
(f : X ⟶ Y)
:
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.
Instances For
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 : C}
{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
Instances For
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 : C}
{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 : M)
(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 : C}
{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 : M)
(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 : C}
{Y : C}
{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 : M}
{b : M}
{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 : C}
{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 : C}
{Y : C}
{Z : C}
{T : C}
{a₁ : M}
{a₂ : M}
{a₃ : M}
{a₁₂ : M}
{a₂₃ : M}
{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₂₃) ⋯