Theorems · Theorem · category theory
CategoryTheory.Localization.SmallShiftedHom.equiv_chgUniv
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
{W : CategoryTheory.MorphismProperty C} {M : Type w'} [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C M]
[inst_4 : CategoryTheory.HasShift D M] (L : CategoryTheory.Functor C D) [inst_5 : L.IsLocalization W]
[inst_6 : L.CommShift M] {X Y : C} {m : M} [inst_7 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
[inst_8 : 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- Cited by
- 1 results in Mathlib
- Foundations
- Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites24
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homproof · cited by 32,603
- CategoryTheory.Functor.objstatement and proof · cited by 19,642
- CategoryTheory.CategoryStruct.compproof · cited by 17,999
- CategoryTheory.Functorstatement and proof · cited by 16,252
- Equivstatement · cited by 8,337
- CategoryTheory.Iso.homproof · cited by 7,684
- CategoryTheory.NatTrans.appproof · cited by 7,406
- AddMonoidstatement and proof · cited by 2,864
- CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
- CategoryTheory.shiftFunctorproof · cited by 1,553
Cited by1
Results whose statement or proof uses this declaration.
- CategoryTheory.Abelian.Ext.homEquiv_chgUnivproof · cited by 0