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₁}
[Category.{v₁, u₁} C]
(W : MorphismProperty C)
(M : Type w')
[AddMonoid M]
[HasShift C M]
(X 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₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(W : MorphismProperty C)
(M : Type w')
[AddMonoid M]
[HasShift C M]
[HasShift D M]
(L : Functor C D)
[L.IsLocalization W]
[L.CommShift M]
(X Y : C)
:
HasSmallLocalizedShiftedHom W M X Y ↔ ∀ (a b : M), Small.{w, v₂} ((shiftFunctor D a).obj (L.obj X) ⟶ (shiftFunctor D b).obj (L.obj Y))
theorem
CategoryTheory.Localization.hasSmallLocalizedShiftedHom_iff_target
{C : Type u₁}
[Category.{v₁, u₁} C]
(W : MorphismProperty C)
(M : Type w')
[AddMonoid M]
[HasShift C M]
(X : C)
{Y : C}
[W.IsCompatibleWithShift M]
{Y' : C}
(f : Y ⟶ Y')
(hf : W f)
:
HasSmallLocalizedShiftedHom W M X Y ↔ HasSmallLocalizedShiftedHom W M X Y'
theorem
CategoryTheory.Localization.hasSmallLocalizedShiftedHom_iff_source
{C : Type u₁}
[Category.{v₁, u₁} C]
(W : MorphismProperty C)
(M : Type w')
[AddMonoid M]
[HasShift C M]
{X : C}
[W.IsCompatibleWithShift M]
{X' : C}
(f : X ⟶ X')
(hf : W f)
(Y : C)
:
HasSmallLocalizedShiftedHom W M X Y ↔ HasSmallLocalizedShiftedHom W M X' Y
theorem
CategoryTheory.Localization.hasSmallLocalizedHom_of_hasSmallLocalizedShiftedHom₀
{C : Type u₁}
[Category.{v₁, u₁} C]
(W : MorphismProperty C)
(M : Type w')
[AddMonoid M]
[HasShift C M]
(X Y : C)
[HasSmallLocalizedShiftedHom W M X Y]
:
HasSmallLocalizedHom W X Y
instance
CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor
{C : Type u₁}
[Category.{v₁, u₁} C]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
(X Y : C)
[HasSmallLocalizedShiftedHom W M X Y]
(m : M)
:
HasSmallLocalizedHom W X ((shiftFunctor C m).obj Y)
instance
CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor_1
{C : Type u₁}
[Category.{v₁, u₁} C]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
(X Y : C)
[HasSmallLocalizedShiftedHom W M X Y]
(m : M)
:
HasSmallLocalizedHom W ((shiftFunctor C m).obj X) Y
instance
CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor_2
{C : Type u₁}
[Category.{v₁, u₁} C]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
(X Y : C)
[HasSmallLocalizedShiftedHom W M X Y]
(m m' n : M)
:
HasSmallLocalizedHom W ((shiftFunctor C m').obj ((shiftFunctor C m).obj X)) ((shiftFunctor C n).obj Y)
instance
CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor_3
{C : Type u₁}
[Category.{v₁, u₁} C]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
(X Y : C)
[HasSmallLocalizedShiftedHom W M X Y]
(m n n' : M)
:
HasSmallLocalizedHom W ((shiftFunctor C m).obj X) ((shiftFunctor C n').obj ((shiftFunctor C n).obj Y))
noncomputable def
CategoryTheory.Localization.SmallHom.shift
{C : Type u₁}
[Category.{v₁, u₁} C]
{W : MorphismProperty C}
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[W.IsCompatibleWithShift M]
{X Y : C}
[HasSmallLocalizedHom W X Y]
(f : SmallHom W X Y)
(a : M)
[HasSmallLocalizedHom W ((shiftFunctor C a).obj X) ((shiftFunctor C a).obj Y)]
:
SmallHom W ((shiftFunctor C a).obj X) ((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₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{W : MorphismProperty C}
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[HasShift D M]
[W.IsCompatibleWithShift M]
(L : Functor C D)
[L.IsLocalization W]
[L.CommShift M]
{X Y : C}
[HasSmallLocalizedHom W X Y]
(f : SmallHom W X Y)
(a : M)
[HasSmallLocalizedHom W ((shiftFunctor C a).obj X) ((shiftFunctor C a).obj Y)]
:
(equiv W L) (f.shift a) = CategoryStruct.comp ((L.commShiftIso a).hom.app X)
(CategoryStruct.comp ((shiftFunctor D a).map ((equiv W L) f)) ((L.commShiftIso a).inv.app Y))
def
CategoryTheory.Localization.SmallShiftedHom
{C : Type u₁}
[Category.{v₁, u₁} C]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
(X Y : C)
[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₁}
[Category.{v₁, u₁} C]
{W : MorphismProperty C}
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[W.IsCompatibleWithShift M]
{X Y : C}
{a : M}
[HasSmallLocalizedShiftedHom W M X Y]
[HasSmallLocalizedShiftedHom W M Y Y]
(f : SmallShiftedHom W X Y a)
(n a' : M)
(h : a + n = a')
:
SmallHom W ((shiftFunctor C n).obj X) ((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₁}
[Category.{v₁, u₁} C]
{W : MorphismProperty C}
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[W.IsCompatibleWithShift M]
{X Y Z : C}
{a b c : M}
[HasSmallLocalizedShiftedHom W M X Y]
[HasSmallLocalizedShiftedHom W M Y Z]
[HasSmallLocalizedShiftedHom W M X Z]
[HasSmallLocalizedShiftedHom W M Z Z]
(f : SmallShiftedHom W X Y a)
(g : SmallShiftedHom W Y Z b)
(h : b + a = c)
:
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)
Instances For
noncomputable def
CategoryTheory.Localization.SmallShiftedHom.mk₀
{C : Type u₁}
[Category.{v₁, u₁} C]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
{X Y : C}
[HasSmallLocalizedShiftedHom W M X Y]
(m₀ : M)
(hm₀ : m₀ = 0)
(f : X ⟶ Y)
:
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.
Instances For
noncomputable def
CategoryTheory.Localization.SmallShiftedHom.equiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[HasShift D M]
(L : Functor C D)
[L.IsLocalization W]
[L.CommShift M]
{X Y : C}
[HasSmallLocalizedShiftedHom W M X Y]
{m : M}
:
SmallShiftedHom W X Y m ≃ 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₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[HasShift D M]
(L : Functor C D)
[L.IsLocalization W]
[L.CommShift M]
{X Y : C}
[W.IsCompatibleWithShift M]
{a : M}
[HasSmallLocalizedShiftedHom W M X Y]
[HasSmallLocalizedShiftedHom W M Y Y]
(f : SmallShiftedHom W X Y a)
(n a' : M)
(h : a + n = a')
:
(SmallHom.equiv W L) (f.shift n a' h) = CategoryStruct.comp ((L.commShiftIso n).hom.app X)
(CategoryStruct.comp ((shiftFunctor D n).map ((SmallHom.equiv W L) f))
(CategoryStruct.comp ((shiftFunctor D n).map ((L.commShiftIso a).hom.app Y))
(CategoryStruct.comp ((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₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[HasShift D M]
(L : Functor C D)
[L.IsLocalization W]
[L.CommShift M]
{X Y : C}
[W.IsCompatibleWithShift M]
{a : M}
[HasSmallLocalizedShiftedHom W M X Y]
[HasSmallLocalizedShiftedHom W M Y Y]
(f : SmallShiftedHom W X Y a)
(n a' : M)
(h : a + n = a')
:
(equiv W L) (f.shift n a' h) = CategoryStruct.comp ((L.commShiftIso n).hom.app X)
(CategoryStruct.comp ((shiftFunctor D n).map ((equiv W L) f)) ((shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)))
theorem
CategoryTheory.Localization.SmallShiftedHom.equiv_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[HasShift D M]
(L : Functor C D)
[L.IsLocalization W]
[L.CommShift M]
{X Y Z : C}
[W.IsCompatibleWithShift M]
[HasSmallLocalizedShiftedHom W M X Y]
[HasSmallLocalizedShiftedHom W M Y Z]
[HasSmallLocalizedShiftedHom W M X Z]
[HasSmallLocalizedShiftedHom W M Z Z]
{a b c : M}
(f : SmallShiftedHom W X Y a)
(g : SmallShiftedHom W Y Z b)
(h : b + a = c)
:
@[simp]
theorem
CategoryTheory.Localization.SmallShiftedHom.equiv_mk₀
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[HasShift D M]
(L : Functor C D)
[L.IsLocalization W]
[L.CommShift M]
{X Y : C}
[HasSmallLocalizedShiftedHom W M X Y]
(m₀ : M)
(hm₀ : m₀ = 0)
(f : X ⟶ Y)
:
(equiv W L) (mk₀ W m₀ hm₀ f) = ShiftedHom.mk₀ m₀ hm₀ (L.map f)
theorem
CategoryTheory.Localization.SmallShiftedHom.comp_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[W.IsCompatibleWithShift M]
{X Y Z T : C}
{a₁ a₂ a₃ a₁₂ a₂₃ a : M}
[HasSmallLocalizedShiftedHom W M X Y]
[HasSmallLocalizedShiftedHom W M X Z]
[HasSmallLocalizedShiftedHom W M X T]
[HasSmallLocalizedShiftedHom W M Y Z]
[HasSmallLocalizedShiftedHom W M Y T]
[HasSmallLocalizedShiftedHom W M Z T]
[HasSmallLocalizedShiftedHom W M Z Z]
[HasSmallLocalizedShiftedHom W M T T]
(α : SmallShiftedHom W X Y a₁)
(β : SmallShiftedHom W Y Z a₂)
(γ : 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₁}
[Category.{v₁, u₁} C]
{W : MorphismProperty C}
{M : Type w'}
[AddMonoid M]
[HasShift C M]
{X Y : C}
{m : M}
[HasSmallLocalizedShiftedHom W M X Y]
[HasSmallLocalizedShiftedHom W M X Y]
:
SmallShiftedHom W X Y m ≃ 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
Instances For
theorem
CategoryTheory.Localization.SmallShiftedHom.equiv_chgUniv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{W : MorphismProperty C}
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[HasShift D M]
(L : Functor C D)
[L.IsLocalization W]
[L.CommShift M]
{X Y : C}
{m : M}
[HasSmallLocalizedShiftedHom W M X Y]
[HasSmallLocalizedShiftedHom W M X Y]
(e : SmallShiftedHom W X Y m)
: