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) : 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₁} [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

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 ((Functor.commShiftIso L a).hom.app X) (CategoryStruct.comp ((shiftFunctor D a).map ((equiv W L) f)) ((Functor.commShiftIso L 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)

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} {m : M} [HasSmallLocalizedShiftedHom W M X Y] (f : ShiftedHom X Y m) : SmallShiftedHom W X Y m

Constructor for SmallShiftedHom.

Equations

• CategoryTheory.Localization.SmallShiftedHom.mk W f = CategoryTheory.Localization.SmallHom.mk W f

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))

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)

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

• CategoryTheory.Localization.SmallShiftedHom.mk₀ W m₀ hm₀ f = CategoryTheory.Localization.SmallShiftedHom.mk W (CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ f)

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

The formal inverse in SmallShiftedHom.{w} W Y X m₀ of a morphism f : Y ⟶ X such that W f.

Equations

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

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 ((CategoryTheory.Functor.commShiftIso L m).app Y).homToEquiv

theorem CategoryTheory.Localization.SmallShiftedHom.equiv_apply {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} (f : SmallShiftedHom W X Y m) : (equiv W L) f = CategoryStruct.comp ((SmallHom.equiv W L) f) ((Functor.commShiftIso L m).app Y).hom

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 ((Functor.commShiftIso L n).hom.app X) (CategoryStruct.comp ((shiftFunctor D n).map ((SmallHom.equiv W L) f)) (CategoryStruct.comp ((shiftFunctor D n).map ((Functor.commShiftIso L a).hom.app Y)) (CategoryStruct.comp ((shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)) ((Functor.commShiftIso L 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 ((Functor.commShiftIso L 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) : (equiv W L) (f.comp g h) = ((equiv W L) f).comp ((equiv W L) g) h

@[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} (f : ShiftedHom X Y m) : (equiv W L) (mk W f) = f.map L

@[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)

@[simp]

theorem CategoryTheory.Localization.SmallShiftedHom.equiv_mk₀Inv {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 Y X] [W.RespectsIso] (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) (hf : W f) : (equiv W L) (mk₀Inv m₀ hm₀ f hf) = ShiftedHom.mk₀ m₀ hm₀ (isoOfHom L W f hf).inv

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₂₃) ⋯

@[simp]

theorem CategoryTheory.Localization.SmallShiftedHom.mk₀_comp_mk₀Inv {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] [HasSmallLocalizedShiftedHom W M Y Y] [HasSmallLocalizedShiftedHom W M Y X] [W.IsCompatibleWithShift M] [W.RespectsIso] (m₀ : M) (hm₀ : m₀ = 0) (f : Y ⟶ X) (hf : W f) : (mk₀ W m₀ hm₀ f).comp (mk₀Inv m₀ hm₀ f hf) ⋯ = mk₀ W m₀ hm₀ (CategoryStruct.id Y)

@[simp]

theorem CategoryTheory.Localization.SmallShiftedHom.mk₀Inv_comp_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] [HasSmallLocalizedShiftedHom W M X X] [HasSmallLocalizedShiftedHom W M Y X] [W.IsCompatibleWithShift M] [W.RespectsIso] (m₀ : M) (hm₀ : m₀ = 0) (f : Y ⟶ X) (hf : W f) : (mk₀Inv m₀ hm₀ f hf).comp (mk₀ W m₀ hm₀ f) ⋯ = mk₀ W m₀ hm₀ (CategoryStruct.id X)

@[simp]

theorem CategoryTheory.Localization.SmallShiftedHom.comp_mk₀_id {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] [HasSmallLocalizedShiftedHom W M Y Y] [W.IsCompatibleWithShift M] {m : M} (α : SmallShiftedHom W X Y m) (m₀ : M) (hm₀ : m₀ = 0) : α.comp (mk₀ W m₀ hm₀ (CategoryStruct.id Y)) ⋯ = α

@[simp]

theorem CategoryTheory.Localization.SmallShiftedHom.mk₀_id_comp {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] [HasSmallLocalizedShiftedHom W M X X] [HasSmallLocalizedShiftedHom W M Y Y] [W.IsCompatibleWithShift M] {m : M} (α : SmallShiftedHom W X Y m) (m₀ : M) (hm₀ : m₀ = 0) : (mk₀ W m₀ hm₀ (CategoryStruct.id X)).comp α ⋯ = α

noncomputable def CategoryTheory.Localization.SmallShiftedHom.postcompEquiv {C : Type u₁} [Category.{v₁, u₁} C] {W : MorphismProperty C} {M : Type w'} [AddMonoid M] [HasShift C M] {X Y Z : C} [W.RespectsIso] [W.IsCompatibleWithShift M] [HasSmallLocalizedShiftedHom W M X Y] [HasSmallLocalizedShiftedHom W M Y Z] [HasSmallLocalizedShiftedHom W M X Z] [HasSmallLocalizedShiftedHom W M Z Y] [HasSmallLocalizedShiftedHom W M Y Y] [HasSmallLocalizedShiftedHom W M Z Z] (f : Y ⟶ Z) (hf : W f) {a : M} : SmallShiftedHom W X Y a ≃ SmallShiftedHom W X Z a

The postcomposition on the types SmallShiftedHom W with a morphism which satisfies W is a bijection.

Equations

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

@[simp]

theorem CategoryTheory.Localization.SmallShiftedHom.postcompEquiv_symm_apply {C : Type u₁} [Category.{v₁, u₁} C] {W : MorphismProperty C} {M : Type w'} [AddMonoid M] [HasShift C M] {X Y Z : C} [W.RespectsIso] [W.IsCompatibleWithShift M] [HasSmallLocalizedShiftedHom W M X Y] [HasSmallLocalizedShiftedHom W M Y Z] [HasSmallLocalizedShiftedHom W M X Z] [HasSmallLocalizedShiftedHom W M Z Y] [HasSmallLocalizedShiftedHom W M Y Y] [HasSmallLocalizedShiftedHom W M Z Z] (f : Y ⟶ Z) (hf : W f) {a : M} (β : SmallShiftedHom W X Z a) : (postcompEquiv f hf).symm β = β.comp (mk₀Inv 0 ⋯ f hf) ⋯

@[simp]

theorem CategoryTheory.Localization.SmallShiftedHom.postcompEquiv_apply {C : Type u₁} [Category.{v₁, u₁} C] {W : MorphismProperty C} {M : Type w'} [AddMonoid M] [HasShift C M] {X Y Z : C} [W.RespectsIso] [W.IsCompatibleWithShift M] [HasSmallLocalizedShiftedHom W M X Y] [HasSmallLocalizedShiftedHom W M Y Z] [HasSmallLocalizedShiftedHom W M X Z] [HasSmallLocalizedShiftedHom W M Z Y] [HasSmallLocalizedShiftedHom W M Y Y] [HasSmallLocalizedShiftedHom W M Z Z] (f : Y ⟶ Z) (hf : W f) {a : M} (α : SmallShiftedHom W X Y a) : (postcompEquiv f hf) α = α.comp (mk₀ W 0 ⋯ f) ⋯

noncomputable def CategoryTheory.Localization.SmallShiftedHom.precompEquiv {C : Type u₁} [Category.{v₁, u₁} C] {W : MorphismProperty C} {M : Type w'} [AddMonoid M] [HasShift C M] {X Y Z : C} [W.RespectsIso] [W.IsCompatibleWithShift M] [HasSmallLocalizedShiftedHom W M X X] [HasSmallLocalizedShiftedHom W M Y Y] [HasSmallLocalizedShiftedHom W M X Y] [HasSmallLocalizedShiftedHom W M Y X] [HasSmallLocalizedShiftedHom W M Y Z] [HasSmallLocalizedShiftedHom W M X Z] [HasSmallLocalizedShiftedHom W M Z Z] (f : X ⟶ Y) (hf : W f) {a : M} : SmallShiftedHom W Y Z a ≃ SmallShiftedHom W X Z a

The precomposition on the types SmallShiftedHom W with a morphism which satisfies W is a bijection.

Equations

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

@[simp]

theorem CategoryTheory.Localization.SmallShiftedHom.precompEquiv_symm_apply {C : Type u₁} [Category.{v₁, u₁} C] {W : MorphismProperty C} {M : Type w'} [AddMonoid M] [HasShift C M] {X Y Z : C} [W.RespectsIso] [W.IsCompatibleWithShift M] [HasSmallLocalizedShiftedHom W M X X] [HasSmallLocalizedShiftedHom W M Y Y] [HasSmallLocalizedShiftedHom W M X Y] [HasSmallLocalizedShiftedHom W M Y X] [HasSmallLocalizedShiftedHom W M Y Z] [HasSmallLocalizedShiftedHom W M X Z] [HasSmallLocalizedShiftedHom W M Z Z] (f : X ⟶ Y) (hf : W f) {a : M} (β : SmallShiftedHom W X Z a) : (precompEquiv f hf).symm β = (mk₀Inv 0 ⋯ f hf).comp β ⋯

@[simp]

theorem CategoryTheory.Localization.SmallShiftedHom.precompEquiv_apply {C : Type u₁} [Category.{v₁, u₁} C] {W : MorphismProperty C} {M : Type w'} [AddMonoid M] [HasShift C M] {X Y Z : C} [W.RespectsIso] [W.IsCompatibleWithShift M] [HasSmallLocalizedShiftedHom W M X X] [HasSmallLocalizedShiftedHom W M Y Y] [HasSmallLocalizedShiftedHom W M X Y] [HasSmallLocalizedShiftedHom W M Y X] [HasSmallLocalizedShiftedHom W M Y Z] [HasSmallLocalizedShiftedHom W M X Z] [HasSmallLocalizedShiftedHom W M Z Z] (f : X ⟶ Y) (hf : W f) {a : M} (α : SmallShiftedHom W Y Z a) : (precompEquiv f hf) α = (mk₀ W 0 ⋯ f).comp α ⋯

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

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

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) : (equiv W L) (chgUniv e) = (equiv W L) e

noncomputable def CategoryTheory.LocalizerMorphism.smallShiftedHomMap {C₁ : Type u₁} [Category.{v₁, u₁} C₁] {C₂ : Type u₂} [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) {M : Type w'} [AddMonoid M] [HasShift C₁ M] [HasShift C₂ M] [Φ.functor.CommShift M] {X₁ Y₁ : C₁} {X₂ Y₂ : C₂} [Localization.HasSmallLocalizedShiftedHom W₁ M X₁ Y₁] [Localization.HasSmallLocalizedShiftedHom W₂ M X₂ X₂] [Localization.HasSmallLocalizedShiftedHom W₂ M X₂ Y₂] [Localization.HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂] (eX : Φ.functor.obj X₁ ≅ X₂) (eY : Φ.functor.obj Y₁ ≅ Y₂) {m : M} (f : Localization.SmallShiftedHom W₁ X₁ Y₁ m) : Localization.SmallShiftedHom W₂ X₂ Y₂ m

The action of a localizer morphism Φ on SmallShiftedHom.

Equations

• Φ.smallShiftedHomMap eX eY f = Φ.smallHomMap' eX ((CategoryTheory.Functor.commShiftIso Φ.functor m).app Y₁ ≪≫ (CategoryTheory.shiftFunctor C₂ m).mapIso eY) f

theorem CategoryTheory.LocalizerMorphism.equiv_smallShiftedHomMap {C₁ : Type u₁} [Category.{v₁, u₁} C₁] {C₂ : Type u₂} [Category.{v₂, u₂} C₂] {D₁ : Type u₁'} [Category.{v₁', u₁'} D₁] {D₂ : Type u₂'} [Category.{v₂', u₂'} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] {M : Type w'} [AddMonoid M] [HasShift C₁ M] [HasShift C₂ M] [HasShift D₁ M] [HasShift D₂ M] [L₁.CommShift M] [L₂.CommShift M] [Φ.functor.CommShift M] {X₁ Y₁ : C₁} {X₂ Y₂ : C₂} [Localization.HasSmallLocalizedShiftedHom W₁ M X₁ Y₁] [Localization.HasSmallLocalizedShiftedHom W₂ M X₂ X₂] [Localization.HasSmallLocalizedShiftedHom W₂ M X₂ Y₂] [Localization.HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂] (eX : Φ.functor.obj X₁ ≅ X₂) (eY : Φ.functor.obj Y₁ ≅ Y₂) (G : Functor D₁ D₂) [G.CommShift M] (e : Φ.functor.comp L₂ ≅ L₁.comp G) [NatTrans.CommShift e.hom M] {m : M} (f : Localization.SmallShiftedHom W₁ X₁ Y₁ m) : (Localization.SmallShiftedHom.equiv W₂ L₂) (Φ.smallShiftedHomMap eX eY f) = (ShiftedHom.mk₀ 0 ⋯ (CategoryStruct.comp (L₂.map eX.inv) (e.hom.app X₁))).comp ((((Localization.SmallShiftedHom.equiv W₁ L₁) f).map G).comp (ShiftedHom.mk₀ 0 ⋯ (CategoryStruct.comp (e.inv.app Y₁) (L₂.map eY.hom))) ⋯) ⋯

@[simp]

theorem CategoryTheory.LocalizerMorphism.smallShiftedHomMap_mk {C₁ : Type u₁} [Category.{v₁, u₁} C₁] {C₂ : Type u₂} [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) {M : Type w'} [AddMonoid M] [HasShift C₁ M] [HasShift C₂ M] [Φ.functor.CommShift M] {X₁ Y₁ : C₁} {X₂ Y₂ : C₂} [Localization.HasSmallLocalizedShiftedHom W₁ M X₁ Y₁] [Localization.HasSmallLocalizedShiftedHom W₂ M X₂ X₂] [Localization.HasSmallLocalizedShiftedHom W₂ M X₂ Y₂] [Localization.HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂] (eX : Φ.functor.obj X₁ ≅ X₂) (eY : Φ.functor.obj Y₁ ≅ Y₂) [W₁.IsCompatibleWithShift M] [W₂.IsCompatibleWithShift M] {m : M} (f : ShiftedHom X₁ Y₁ m) : Φ.smallShiftedHomMap eX eY (Localization.SmallShiftedHom.mk W₁ f) = Localization.SmallShiftedHom.mk W₂ ((ShiftedHom.mk₀ 0 ⋯ eX.inv).comp ((f.map Φ.functor).comp (ShiftedHom.mk₀ 0 ⋯ eY.hom) ⋯) ⋯)

theorem CategoryTheory.LocalizerMorphism.smallShiftedHomMap_mk₀ {C₁ : Type u₁} [Category.{v₁, u₁} C₁] {C₂ : Type u₂} [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) {M : Type w'} [AddMonoid M] [HasShift C₁ M] [HasShift C₂ M] [Φ.functor.CommShift M] {X₁ Y₁ : C₁} {X₂ Y₂ : C₂} [Localization.HasSmallLocalizedShiftedHom W₁ M X₁ Y₁] [Localization.HasSmallLocalizedShiftedHom W₂ M X₂ X₂] [Localization.HasSmallLocalizedShiftedHom W₂ M X₂ Y₂] [Localization.HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂] (eX : Φ.functor.obj X₁ ≅ X₂) (eY : Φ.functor.obj Y₁ ≅ Y₂) [W₁.IsCompatibleWithShift M] [W₂.IsCompatibleWithShift M] (m₀ : M) (hm₀ : m₀ = 0) (f : X₁ ⟶ Y₁) : Φ.smallShiftedHomMap eX eY (Localization.SmallShiftedHom.mk₀ W₁ m₀ hm₀ f) = Localization.SmallShiftedHom.mk₀ W₂ m₀ hm₀ (CategoryStruct.comp eX.inv (CategoryStruct.comp (Φ.functor.map f) eY.hom))

theorem CategoryTheory.LocalizerMorphism.smallShiftedHomMap_comp {C₁ : Type u₁} [Category.{v₁, u₁} C₁] {C₂ : Type u₂} [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) {M : Type w'} [AddMonoid M] [HasShift C₁ M] [HasShift C₂ M] [Φ.functor.CommShift M] {X₁ Y₁ Z₁ : C₁} {X₂ Y₂ Z₂ : C₂} [Localization.HasSmallLocalizedShiftedHom W₁ M X₁ Y₁] [Localization.HasSmallLocalizedShiftedHom W₂ M X₂ X₂] [Localization.HasSmallLocalizedShiftedHom W₂ M X₂ Y₂] [Localization.HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂] (eX : Φ.functor.obj X₁ ≅ X₂) (eY : Φ.functor.obj Y₁ ≅ Y₂) (eZ : Φ.functor.obj Z₁ ≅ Z₂) [W₁.IsCompatibleWithShift M] [W₂.IsCompatibleWithShift M] [Localization.HasSmallLocalizedShiftedHom W₁ M Y₁ Z₁] [Localization.HasSmallLocalizedShiftedHom W₂ M Z₂ Z₂] [Localization.HasSmallLocalizedShiftedHom W₂ M Y₂ Z₂] [Localization.HasSmallLocalizedShiftedHom W₁ M X₁ Z₁] [Localization.HasSmallLocalizedShiftedHom W₁ M Z₁ Z₁] [Localization.HasSmallLocalizedShiftedHom W₂ M X₂ Z₂] {a b c : M} (f : Localization.SmallShiftedHom W₁ X₁ Y₁ a) (g : Localization.SmallShiftedHom W₁ Y₁ Z₁ b) (h : b + a = c) : Φ.smallShiftedHomMap eX eZ (f.comp g h) = (Φ.smallShiftedHomMap eX eY f).comp (Φ.smallShiftedHomMap eY eZ g) h