Loogle!
Result
Found 42 declarations mentioning CategoryTheory.shiftFunctorAdd.
- CategoryTheory.shiftFunctorAdd π Mathlib.CategoryTheory.Shift.Basic
(C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (i j : A) : CategoryTheory.shiftFunctor C (i + j) β (CategoryTheory.shiftFunctor C i).comp (CategoryTheory.shiftFunctor C j) - CategoryTheory.ShiftMkCore.shiftFunctorAdd_eq π Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] (h : CategoryTheory.ShiftMkCore C A) (a b : A) : CategoryTheory.shiftFunctorAdd C a b = h.add a b - CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd π Mathlib.CategoryTheory.Shift.Basic
(C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (i j : A) : CategoryTheory.shiftFunctorAdd' C i j (i + j) β― = CategoryTheory.shiftFunctorAdd C i j - CategoryTheory.shiftFunctorAdd_add_zero_hom_app π Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a : A) (X : C) : (CategoryTheory.shiftFunctorAdd C a 0).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom β―) ((CategoryTheory.shiftFunctorZero C A).inv.app ((CategoryTheory.shiftFunctor C a).obj X)) - CategoryTheory.shiftFunctorAdd_add_zero_inv_app π Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a : A) (X : C) : (CategoryTheory.shiftFunctorAdd C a 0).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero C A).hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.eqToHom β―) - CategoryTheory.shiftFunctorAdd_zero_add_hom_app π Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a : A) (X : C) : (CategoryTheory.shiftFunctorAdd C 0 a).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom β―) ((CategoryTheory.shiftFunctor C a).map ((CategoryTheory.shiftFunctorZero C A).inv.app X)) - CategoryTheory.shiftFunctorAdd_zero_add_inv_app π Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a : A) (X : C) : (CategoryTheory.shiftFunctorAdd C 0 a).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a).map ((CategoryTheory.shiftFunctorZero C A).hom.app X)) (CategoryTheory.eqToHom β―) - CategoryTheory.shiftFunctorAdd_assoc π Mathlib.CategoryTheory.Shift.Basic
(C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (aβ aβ aβ : A) : CategoryTheory.shiftFunctorAdd C (aβ + aβ) aβ βͺβ« CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorAdd C aβ aβ) (CategoryTheory.shiftFunctor C aβ) βͺβ« (CategoryTheory.shiftFunctor C aβ).associator (CategoryTheory.shiftFunctor C aβ) (CategoryTheory.shiftFunctor C aβ) = CategoryTheory.shiftFunctorAdd' C aβ (aβ + aβ) (aβ + aβ + aβ) β― βͺβ« (CategoryTheory.shiftFunctor C aβ).isoWhiskerLeft (CategoryTheory.shiftFunctorAdd C aβ aβ) - CategoryTheory.Functor.FullyFaithful.hasShift.map_add_hom_app π Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] {D : Type u_2} [CategoryTheory.Category.{v_1, u_2} D] [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (s : A β CategoryTheory.Functor C C) (i : (i : A) β (s i).comp F β F.comp (CategoryTheory.shiftFunctor D i)) (a b : A) (X : C) : F.map ((CategoryTheory.Functor.FullyFaithful.hasShift.add hF s i a b).hom.app X) = CategoryTheory.CategoryStruct.comp ((i (a + b)).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd D a b).hom.app (F.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((i a).inv.app X)) ((i b).inv.app ((s a).obj X)))) - CategoryTheory.Functor.FullyFaithful.hasShift.map_add_inv_app π Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] {D : Type u_2} [CategoryTheory.Category.{v_1, u_2} D] [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (s : A β CategoryTheory.Functor C C) (i : (i : A) β (s i).comp F β F.comp (CategoryTheory.shiftFunctor D i)) (a b : A) (X : C) : F.map ((CategoryTheory.Functor.FullyFaithful.hasShift.add hF s i a b).inv.app X) = CategoryTheory.CategoryStruct.comp ((i b).hom.app ((s a).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((i a).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd D a b).inv.app (F.obj X)) ((i (a + b)).inv.app X))) - CategoryTheory.shiftFunctorAdd_assoc_inv_app π Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (aβ aβ aβ : A) (X : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C aβ).map ((CategoryTheory.shiftFunctorAdd C aβ aβ).inv.app X)) ((CategoryTheory.shiftFunctorAdd C (aβ + aβ) aβ).inv.app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C aβ aβ).inv.app ((CategoryTheory.shiftFunctor C aβ).obj X)) ((CategoryTheory.shiftFunctorAdd' C aβ (aβ + aβ) (aβ + aβ + aβ) β―).inv.app X) - CategoryTheory.shiftFunctorAdd_assoc_hom_app π Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (aβ aβ aβ : A) (X : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C (aβ + aβ) aβ).hom.app X) ((CategoryTheory.shiftFunctor C aβ).map ((CategoryTheory.shiftFunctorAdd C aβ aβ).hom.app X)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C aβ (aβ + aβ) (aβ + aβ + aβ) β―).hom.app X) ((CategoryTheory.shiftFunctorAdd C aβ aβ).hom.app ((CategoryTheory.shiftFunctor C aβ).obj X)) - CategoryTheory.shiftFunctorAdd_assoc_hom_app_assoc π Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (aβ aβ aβ : A) (X : C) {Z : C} (h : (CategoryTheory.shiftFunctor C aβ).obj ((CategoryTheory.shiftFunctor C aβ).obj ((CategoryTheory.shiftFunctor C aβ).obj X)) βΆ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C (aβ + aβ) aβ).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C aβ).map ((CategoryTheory.shiftFunctorAdd C aβ aβ).hom.app X)) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C aβ (aβ + aβ) (aβ + aβ + aβ) β―).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C aβ aβ).hom.app ((CategoryTheory.shiftFunctor C aβ).obj X)) h) - CategoryTheory.shiftFunctorAdd_assoc_inv_app_assoc π Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (aβ aβ aβ : A) (X : C) {Z : C} (h : (CategoryTheory.shiftFunctor C (aβ + aβ + aβ)).obj X βΆ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C aβ).map ((CategoryTheory.shiftFunctorAdd C aβ aβ).inv.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C (aβ + aβ) aβ).inv.app X) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C aβ aβ).inv.app ((CategoryTheory.shiftFunctor C aβ).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C aβ (aβ + aβ) (aβ + aβ + aβ) β―).inv.app X) h) - CategoryTheory.shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app π Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddCommMonoid A] [CategoryTheory.HasShift C A] (mβ mβ mβ : A) (X : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm C mβ (mβ + mβ)).hom.app X) ((CategoryTheory.shiftFunctor C mβ).map ((CategoryTheory.shiftFunctorAdd C mβ mβ).hom.app X)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C mβ mβ).hom.app ((CategoryTheory.shiftFunctor C mβ).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C mβ).map ((CategoryTheory.shiftFunctorComm C mβ mβ).hom.app X)) ((CategoryTheory.shiftFunctorComm C mβ mβ).hom.app ((CategoryTheory.shiftFunctor C mβ).obj X))) - CategoryTheory.shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app_assoc π Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddCommMonoid A] [CategoryTheory.HasShift C A] (mβ mβ mβ : A) (X : C) {Z : C} (h : (CategoryTheory.shiftFunctor C mβ).obj ((CategoryTheory.shiftFunctor C mβ).obj ((CategoryTheory.shiftFunctor C mβ).obj X)) βΆ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm C mβ (mβ + mβ)).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C mβ).map ((CategoryTheory.shiftFunctorAdd C mβ mβ).hom.app X)) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C mβ mβ).hom.app ((CategoryTheory.shiftFunctor C mβ).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C mβ).map ((CategoryTheory.shiftFunctorComm C mβ mβ).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm C mβ mβ).hom.app ((CategoryTheory.shiftFunctor C mβ).obj X)) h)) - CategoryTheory.Functor.CommShift.isoAdd_inv_app π Mathlib.CategoryTheory.Shift.CommShift
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] {a b : A} (eβ : (CategoryTheory.shiftFunctor C a).comp F β F.comp (CategoryTheory.shiftFunctor D a)) (eβ : (CategoryTheory.shiftFunctor C b).comp F β F.comp (CategoryTheory.shiftFunctor D b)) (X : C) : (CategoryTheory.Functor.CommShift.isoAdd eβ eβ).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd D a b).hom.app (F.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map (eβ.inv.app X)) (CategoryTheory.CategoryStruct.comp (eβ.inv.app ((CategoryTheory.shiftFunctor C a).obj X)) (F.map ((CategoryTheory.shiftFunctorAdd C a b).inv.app X)))) - CategoryTheory.Functor.CommShift.isoAdd_hom_app π Mathlib.CategoryTheory.Shift.CommShift
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] {a b : A} (eβ : (CategoryTheory.shiftFunctor C a).comp F β F.comp (CategoryTheory.shiftFunctor D a)) (eβ : (CategoryTheory.shiftFunctor C b).comp F β F.comp (CategoryTheory.shiftFunctor D b)) (X : C) : (CategoryTheory.Functor.CommShift.isoAdd eβ eβ).hom.app X = CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd C a b).hom.app X)) (CategoryTheory.CategoryStruct.comp (eβ.hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map (eβ.hom.app X)) ((CategoryTheory.shiftFunctorAdd D a b).inv.app (F.obj X)))) - CategoryTheory.Functor.CommShift.isoAdd_hom_app_assoc π Mathlib.CategoryTheory.Shift.CommShift
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] {a b : A} (eβ : (CategoryTheory.shiftFunctor C a).comp F β F.comp (CategoryTheory.shiftFunctor D a)) (eβ : (CategoryTheory.shiftFunctor C b).comp F β F.comp (CategoryTheory.shiftFunctor D b)) (X : C) {Z : D} (h : (CategoryTheory.shiftFunctor D (a + b)).obj (F.obj X) βΆ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.CommShift.isoAdd eβ eβ).hom.app X) h = CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd C a b).hom.app X)) (CategoryTheory.CategoryStruct.comp (eβ.hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map (eβ.hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd D a b).inv.app (F.obj X)) h))) - CategoryTheory.Functor.CommShift.isoAdd_inv_app_assoc π Mathlib.CategoryTheory.Shift.CommShift
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] {a b : A} (eβ : (CategoryTheory.shiftFunctor C a).comp F β F.comp (CategoryTheory.shiftFunctor D a)) (eβ : (CategoryTheory.shiftFunctor C b).comp F β F.comp (CategoryTheory.shiftFunctor D b)) (X : C) {Z : D} (h : F.obj ((CategoryTheory.shiftFunctor C (a + b)).obj X) βΆ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.CommShift.isoAdd eβ eβ).inv.app X) h = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd D a b).hom.app (F.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map (eβ.inv.app X)) (CategoryTheory.CategoryStruct.comp (eβ.inv.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd C a b).inv.app X)) h))) - CategoryTheory.HasShift.Induced.add_hom_app_obj π Mathlib.CategoryTheory.Shift.Induced
{C : Type u_3} {D : Type u_1} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Category.{v_2, u_1} D] (F : CategoryTheory.Functor C D) {A : Type u_2} [AddMonoid A] [CategoryTheory.HasShift C A] (s : A β CategoryTheory.Functor D D) (i : (a : A) β F.comp (s a) β (CategoryTheory.shiftFunctor C a).comp F) [((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Full] [((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Faithful] (a b : A) (X : C) : (CategoryTheory.HasShift.Induced.add F s i a b).hom.app (F.obj X) = CategoryTheory.CategoryStruct.comp ((i (a + b)).hom.app X) (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd C a b).hom.app X)) (CategoryTheory.CategoryStruct.comp ((i b).inv.app ((CategoryTheory.shiftFunctor C a).obj X)) ((s b).map ((i a).inv.app X)))) - CategoryTheory.HasShift.Induced.add_inv_app_obj π Mathlib.CategoryTheory.Shift.Induced
{C : Type u_2} {D : Type u_1} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.Category.{v_2, u_1} D] (F : CategoryTheory.Functor C D) {A : Type u_3} [AddMonoid A] [CategoryTheory.HasShift C A] (s : A β CategoryTheory.Functor D D) (i : (a : A) β F.comp (s a) β (CategoryTheory.shiftFunctor C a).comp F) [((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Full] [((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Faithful] (a b : A) (X : C) : (CategoryTheory.HasShift.Induced.add F s i a b).inv.app (F.obj X) = CategoryTheory.CategoryStruct.comp ((s b).map ((i a).hom.app X)) (CategoryTheory.CategoryStruct.comp ((i b).hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd C a b).inv.app X)) ((i (a + b)).inv.app X))) - CategoryTheory.shiftFunctorAdd_hom_app_obj_of_induced π Mathlib.CategoryTheory.Shift.Induced
{C : Type u_3} {D : Type u_1} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Category.{v_2, u_1} D] (F : CategoryTheory.Functor C D) {A : Type u_2} [AddMonoid A] [CategoryTheory.HasShift C A] (s : A β CategoryTheory.Functor D D) (i : (a : A) β F.comp (s a) β (CategoryTheory.shiftFunctor C a).comp F) [((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Full] [((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Faithful] (a b : A) (X : C) : (CategoryTheory.shiftFunctorAdd D a b).hom.app (F.obj X) = CategoryTheory.CategoryStruct.comp ((i (a + b)).hom.app X) (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd C a b).hom.app X)) (CategoryTheory.CategoryStruct.comp ((i b).inv.app ((CategoryTheory.shiftFunctor C a).obj X)) ((s b).map ((i a).inv.app X)))) - CategoryTheory.shiftFunctorAdd_inv_app_obj_of_induced π Mathlib.CategoryTheory.Shift.Induced
{C : Type u_3} {D : Type u_1} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Category.{v_2, u_1} D] (F : CategoryTheory.Functor C D) {A : Type u_2} [AddMonoid A] [CategoryTheory.HasShift C A] (s : A β CategoryTheory.Functor D D) (i : (a : A) β F.comp (s a) β (CategoryTheory.shiftFunctor C a).comp F) [((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Full] [((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Faithful] (a b : A) (X : C) : (CategoryTheory.shiftFunctorAdd D a b).inv.app (F.obj X) = CategoryTheory.CategoryStruct.comp ((s b).map ((i a).hom.app X)) (CategoryTheory.CategoryStruct.comp ((i b).hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd C a b).inv.app X)) ((i (a + b)).inv.app X))) - CochainComplex.shiftFunctorAdd_eq π Mathlib.Algebra.Homology.HomotopyCategory.Shift
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (a b : β€) : CategoryTheory.shiftFunctorAdd (CochainComplex C β€) a b = CochainComplex.shiftFunctorAdd' C a b (a + b) β― - CochainComplex.shiftFunctorAdd_hom_app_f π Mathlib.Algebra.Homology.HomotopyCategory.Shift
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C β€) (a b n : β€) : ((CategoryTheory.shiftFunctorAdd (CochainComplex C β€) a b).hom.app K).f n = (HomologicalComplex.XIsoOfEq K β―).hom - CochainComplex.shiftFunctorAdd_inv_app_f π Mathlib.Algebra.Homology.HomotopyCategory.Shift
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C β€) (a b n : β€) : ((CategoryTheory.shiftFunctorAdd (CochainComplex C β€) a b).inv.app K).f n = (HomologicalComplex.XIsoOfEq K β―).hom - CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd_eq π Mathlib.CategoryTheory.Triangulated.TriangleShift
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C β€] [β (n : β€), (CategoryTheory.shiftFunctor C n).Additive] (a b : β€) : CategoryTheory.shiftFunctorAdd (CategoryTheory.Pretriangulated.Triangle C) a b = CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b (a + b) β― - CategoryTheory.Functor.shiftIso_add π Mathlib.CategoryTheory.Shift.ShiftSequence
{C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] (n m a a' a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') : F.shiftIso (m + n) a a'' β― = CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorAdd C m n) (F.shift a) βͺβ« (CategoryTheory.shiftFunctor C m).associator (CategoryTheory.shiftFunctor C n) (F.shift a) βͺβ« (CategoryTheory.shiftFunctor C m).isoWhiskerLeft (F.shiftIso n a a' ha') βͺβ« F.shiftIso m a' a'' ha'' - CategoryTheory.Functor.ShiftSequence.shiftIso_add π Mathlib.CategoryTheory.Shift.ShiftSequence
{C : Type u_1} {A : Type u_3} {instβ : CategoryTheory.Category.{v_1, u_1} C} {instβΒΉ : CategoryTheory.Category.{v_3, u_3} A} {F : CategoryTheory.Functor C A} {M : Type u_4} {instβΒ² : AddMonoid M} {instβΒ³ : CategoryTheory.HasShift C M} [self : F.ShiftSequence M] (n m a a' a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') : CategoryTheory.Functor.ShiftSequence.shiftIso (m + n) a a'' β― = CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorAdd C m n) (CategoryTheory.Functor.ShiftSequence.sequence F a) βͺβ« (CategoryTheory.shiftFunctor C m).associator (CategoryTheory.shiftFunctor C n) (CategoryTheory.Functor.ShiftSequence.sequence F a) βͺβ« (CategoryTheory.shiftFunctor C m).isoWhiskerLeft (CategoryTheory.Functor.ShiftSequence.shiftIso n a a' ha') βͺβ« CategoryTheory.Functor.ShiftSequence.shiftIso m a' a'' ha'' - CategoryTheory.Functor.ShiftSequence.mk π Mathlib.CategoryTheory.Shift.ShiftSequence
{C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} A] {F : CategoryTheory.Functor C A} {M : Type u_4} [AddMonoid M] [CategoryTheory.HasShift C M] (sequence : M β CategoryTheory.Functor C A) (isoZero : sequence 0 β F) (shiftIso : (n a a' : M) β n + a = a' β ((CategoryTheory.shiftFunctor C n).comp (sequence a) β sequence a')) (shiftIso_zero : β (a : M), shiftIso 0 a a β― = CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorZero C M) (sequence a) βͺβ« (sequence a).leftUnitor) (shiftIso_add : β (n m a a' a'' : M) (ha' : n + a = a') (ha'' : m + a' = a''), shiftIso (m + n) a a'' β― = CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorAdd C m n) (sequence a) βͺβ« (CategoryTheory.shiftFunctor C m).associator (CategoryTheory.shiftFunctor C n) (sequence a) βͺβ« (CategoryTheory.shiftFunctor C m).isoWhiskerLeft (shiftIso n a a' ha') βͺβ« shiftIso m a' a'' ha'') : F.ShiftSequence M - CategoryTheory.Functor.shiftIso_add_hom_app π Mathlib.CategoryTheory.Shift.ShiftSequence
{C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] (n m a a' a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) : (F.shiftIso (m + n) a a'' β―).hom.app X = CategoryTheory.CategoryStruct.comp ((F.shift a).map ((CategoryTheory.shiftFunctorAdd C m n).hom.app X)) (CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').hom.app ((CategoryTheory.shiftFunctor C m).obj X)) ((F.shiftIso m a' a'' ha'').hom.app X)) - CategoryTheory.Functor.shiftIso_add_inv_app π Mathlib.CategoryTheory.Shift.ShiftSequence
{C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] (n m a a' a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) : (F.shiftIso (m + n) a a'' β―).inv.app X = CategoryTheory.CategoryStruct.comp ((F.shiftIso m a' a'' ha'').inv.app X) (CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').inv.app ((CategoryTheory.shiftFunctor C m).obj X)) ((F.shift a).map ((CategoryTheory.shiftFunctorAdd C m n).inv.app X))) - CategoryTheory.SingleFunctors.mk π Mathlib.CategoryTheory.Shift.SingleFunctors
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (functor : A β CategoryTheory.Functor C D) (shiftIso : (n a a' : A) β n + a = a' β ((functor a').comp (CategoryTheory.shiftFunctor D n) β functor a)) (shiftIso_zero : β (a : A), shiftIso 0 a a β― = (functor a).isoWhiskerLeft (CategoryTheory.shiftFunctorZero D A)) (shiftIso_add : β (n m a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a''), shiftIso (m + n) a a'' β― = (functor a'').isoWhiskerLeft (CategoryTheory.shiftFunctorAdd D m n) βͺβ« ((functor a'').associator (CategoryTheory.shiftFunctor D m) (CategoryTheory.shiftFunctor D n)).symm βͺβ« CategoryTheory.Functor.isoWhiskerRight (shiftIso m a' a'' ha'') (CategoryTheory.shiftFunctor D n) βͺβ« shiftIso n a a' ha') : CategoryTheory.SingleFunctors C D A - CategoryTheory.SingleFunctors.shiftIso_add π Mathlib.CategoryTheory.Shift.SingleFunctors
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (self : CategoryTheory.SingleFunctors C D A) (n m a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') : self.shiftIso (m + n) a a'' β― = (self.functor a'').isoWhiskerLeft (CategoryTheory.shiftFunctorAdd D m n) βͺβ« ((self.functor a'').associator (CategoryTheory.shiftFunctor D m) (CategoryTheory.shiftFunctor D n)).symm βͺβ« CategoryTheory.Functor.isoWhiskerRight (self.shiftIso m a' a'' ha'') (CategoryTheory.shiftFunctor D n) βͺβ« self.shiftIso n a a' ha' - CategoryTheory.SingleFunctors.shiftIso_add_hom_app π Mathlib.CategoryTheory.Shift.SingleFunctors
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (n m a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) : (F.shiftIso (m + n) a a'' β―).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd D m n).hom.app ((F.functor a'').obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').hom.app X)) ((F.shiftIso n a a' ha').hom.app X)) - CategoryTheory.SingleFunctors.shiftIso_add_inv_app π Mathlib.CategoryTheory.Shift.SingleFunctors
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (n m a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) : (F.shiftIso (m + n) a a'' β―).inv.app X = CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').inv.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').inv.app X)) ((CategoryTheory.shiftFunctorAdd D m n).inv.app ((F.functor a'').obj X))) - CategoryTheory.oppositeShiftFunctorAdd_hom_app π Mathlib.CategoryTheory.Shift.Opposite
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} [AddMonoid A] [CategoryTheory.HasShift C A] (X : CategoryTheory.OppositeShift C A) (a b : A) : (CategoryTheory.shiftFunctorAdd (CategoryTheory.OppositeShift C A) a b).hom.app X = ((CategoryTheory.shiftFunctorAdd C a b).inv.app (Opposite.unop X)).op - CategoryTheory.oppositeShiftFunctorAdd_inv_app π Mathlib.CategoryTheory.Shift.Opposite
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} [AddMonoid A] [CategoryTheory.HasShift C A] (X : CategoryTheory.OppositeShift C A) (a b : A) : (CategoryTheory.shiftFunctorAdd (CategoryTheory.OppositeShift C A) a b).inv.app X = ((CategoryTheory.shiftFunctorAdd C a b).hom.app (Opposite.unop X)).op - CategoryTheory.ShiftedHom.opEquiv'_add_symm π Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C β€] {X Y : C} (n m a a' a'' : β€) (ha' : n + a = a') (ha'' : m + a' = a'') (x : Opposite.op ((CategoryTheory.shiftFunctor C a).obj Y) βΆ (CategoryTheory.shiftFunctor Cα΅α΅ (m + n)).obj (Opposite.op X)) : (CategoryTheory.ShiftedHom.opEquiv' (m + n) a a'' β―).symm x = (CategoryTheory.ShiftedHom.opEquiv' m a' a'' ha'').symm (Quiver.Hom.op ((CategoryTheory.ShiftedHom.opEquiv' n a a' ha').symm (CategoryTheory.CategoryStruct.comp x ((CategoryTheory.shiftFunctorAdd Cα΅α΅ m n).hom.app (Opposite.op X))))) - CategoryTheory.DifferentialObject.shiftFunctorAdd_hom_app_f π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (m n : S) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.DifferentialObject.shiftFunctorAdd C m n).hom.app X).f = (CategoryTheory.shiftFunctorAdd C m n).hom.app X.obj - CategoryTheory.DifferentialObject.shiftFunctorAdd_inv_app_f π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (m n : S) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.DifferentialObject.shiftFunctorAdd C m n).inv.app X).f = (CategoryTheory.shiftFunctorAdd C m n).inv.app X.obj
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using the Loogle command from the command palette. You can also try the
#loogle command from LeanSearchClient,
the CLI version, the Loogle
VS Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
πReal.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
π"differ"
finds all lemmas that have"differ"somewhere in their lemma name.By subexpression:
π_ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.The pattern can also be non-linear, as in
πReal.sqrt ?a * Real.sqrt ?aIf the pattern has parameters, they are matched in any order. Both of these will find
List.map:
π(?a -> ?b) -> List ?a -> List ?b
πList ?a -> (?a -> ?b) -> List ?bBy main conclusion:
π|- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of allβandβ) has the given shape.As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
π|- _ < _ β tsum _ < tsum _
will findtsum_lt_tsumeven though the hypothesisf i < g iis not the last.You can filter for definitions vs theorems: Using
β’ (_ : Type _)finds all definitions which provide data whileβ’ (_ : Prop)finds all theorems (and definitions of proofs).
If you pass more than one such search filter, separated by commas
Loogle will return lemmas which match all of them. The
search
π Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ β _
would find all lemmas which mention the constants Real.sin
and tsum, have "two" as a substring of the
lemma name, include a product and a power somewhere in the type,
and have a hypothesis of the form _ < _ (if
there were any such lemmas). Metavariables (?a) are
assigned independently in each filter.
The #lucky button will directly send you to the
documentation of the first hit.
Source code
You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.
This is Loogle revision 9f11169 serving mathlib revision 69fae59