Loogle!

Result

Found 54 declarations mentioning CategoryTheory.ObjectProperty.trW.

• CategoryTheory.ObjectProperty.trW 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (P : CategoryTheory.ObjectProperty C) : CategoryTheory.MorphismProperty C
• CategoryTheory.ObjectProperty.instRespectsIsoTrW 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (P : CategoryTheory.ObjectProperty C) : P.trW.RespectsIso
• CategoryTheory.ObjectProperty.instContainsIdentitiesTrWOfContainsZero 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] : P.trW.ContainsIdentities
• CategoryTheory.ObjectProperty.instIsStableUnderFiniteProductsTrWOfIsTriangulated 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (P : CategoryTheory.ObjectProperty C) [P.IsTriangulated] : P.trW.IsStableUnderFiniteProducts
• CategoryTheory.ObjectProperty.instIsCompatibleWithShiftTrWIntOfIsStableUnderShift 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderShift ℤ] : P.trW.IsCompatibleWithShift ℤ
• CategoryTheory.ObjectProperty.trW_isoClosure 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (P : CategoryTheory.ObjectProperty C) : P.isoClosure.trW = P.trW
• CategoryTheory.ObjectProperty.instHasLeftCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.IsTriangulated C] [P.IsTriangulated] : P.trW.HasLeftCalculusOfFractions
• CategoryTheory.ObjectProperty.instHasRightCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.IsTriangulated C] [P.IsTriangulated] : P.trW.HasRightCalculusOfFractions
• CategoryTheory.ObjectProperty.instIsMultiplicativeTrWOfIsTriangulatedOfIsTriangulated 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.IsTriangulated C] [P.IsTriangulated] : P.trW.IsMultiplicative
• CategoryTheory.ObjectProperty.trW_of_isIso 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : P.trW f
• CategoryTheory.ObjectProperty.instIsCompatibleWithTriangulationTrWOfIsTriangulatedOfIsTriangulated 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.IsTriangulated C] [P.IsTriangulated] : P.trW.IsCompatibleWithTriangulation
• CategoryTheory.ObjectProperty.trW.mk 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (P : CategoryTheory.ObjectProperty C) {T : CategoryTheory.Pretriangulated.Triangle C} (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h : P T.obj₃) : P.trW T.mor₁
• CategoryTheory.ObjectProperty.trW_iff_of_distinguished 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : P.trW T.mor₁ ↔ P T.obj₃
• CategoryTheory.ObjectProperty.trW.mk' 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderShift ℤ] {T : CategoryTheory.Pretriangulated.Triangle C} (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h : P T.obj₁) : P.trW T.mor₂
• CategoryTheory.ObjectProperty.trW_iff_of_distinguished' 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderShift ℤ] [P.IsClosedUnderIsomorphisms] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : P.trW T.mor₂ ↔ P T.obj₁
• CategoryTheory.ObjectProperty.trW_monotone 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {P Q : CategoryTheory.ObjectProperty C} (h : P ≤ Q) : P.trW ≤ Q.trW
• CategoryTheory.ObjectProperty.trW.shift 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {P : CategoryTheory.ObjectProperty C} [P.IsStableUnderShift ℤ] {X₁ X₂ : C} {f : X₁ ⟶ X₂} (hf : P.trW f) (n : ℤ) : P.trW ((CategoryTheory.shiftFunctor C n).map f)
• CategoryTheory.ObjectProperty.trW.unshift 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderShift ℤ] {X₁ X₂ : C} {f : X₁ ⟶ X₂} {n : ℤ} (hf : P.trW ((CategoryTheory.shiftFunctor C n).map f)) : P.trW f
• CategoryTheory.ObjectProperty.inverseImage_trW_isInverted 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor D C) [F.CommShift ℤ] [F.IsTriangulated] [P.IsClosedUnderIsomorphisms] {E : Type u_4} [CategoryTheory.Category.{u_5, u_4} E] (L : CategoryTheory.Functor C E) [L.IsLocalization P.trW] : (P.inverseImage F).trW.IsInvertedBy (F.comp L)
• CategoryTheory.ObjectProperty.smul_mem_trW_iff 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (P : CategoryTheory.ObjectProperty C) {X Y : C} (f : X ⟶ Y) (n : ℤˣ) : P.trW (n • f) ↔ P.trW f
• CategoryTheory.ObjectProperty.inverseImage_trW_iff 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor D C) [F.CommShift ℤ] [F.IsTriangulated] [P.IsClosedUnderIsomorphisms] {X Y : D} (s : X ⟶ Y) : (P.inverseImage F).trW s ↔ P.trW (F.map s)
• CategoryTheory.ObjectProperty.trW_iff 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (P : CategoryTheory.ObjectProperty C) {X Y : C} (f : X ⟶ Y) : P.trW f ↔ ∃ Z g h, ∃ (_ : CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), P Z
• CategoryTheory.ObjectProperty.trW_iff' 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderShift ℤ] {Y Z : C} (g : Y ⟶ Z) : P.trW g ↔ ∃ X f h, ∃ (_ : CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), P X
• CategoryTheory.Functor.mem_homologicalKernel_trW_iff 📋 Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
  {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Abelian A] [F.IsHomological] [F.ShiftSequence ℤ] {X Y : C} (f : X ⟶ Y) : F.homologicalKernel.trW f ↔ ∀ (n : ℤ), CategoryTheory.IsIso ((F.shift n).map f)
• HomotopyCategory.quasiIso_eq_subcategoryAcyclic_W 📋 Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) = (HomotopyCategory.subcategoryAcyclic C).trW
• HomotopyCategory.quasiIso_eq_trW_subcategoryAcyclic 📋 Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) = (HomotopyCategory.subcategoryAcyclic C).trW
• DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic 📋 Mathlib.Algebra.Homology.DerivedCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : DerivedCategory.Qh.IsLocalization (HomotopyCategory.subcategoryAcyclic C).trW
• CategoryTheory.ObjectProperty.isColocal_trW 📋 Mathlib.CategoryTheory.Triangulated.Orthogonal
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [P.IsTriangulated] : P.trW.isColocal = P.leftOrthogonal
• CategoryTheory.ObjectProperty.isLocal_trW 📋 Mathlib.CategoryTheory.Triangulated.Orthogonal
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [P.IsTriangulated] : P.trW.isLocal = P.rightOrthogonal
• CategoryTheory.ObjectProperty.leftOrthogonal.map_bijective_of_isTriangulated 📋 Mathlib.CategoryTheory.Triangulated.Orthogonal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {P : CategoryTheory.ObjectProperty C} [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [P.IsTriangulated] [CategoryTheory.IsTriangulated C] {X : C} (hX : P.leftOrthogonal X) (L : CategoryTheory.Functor C D) [L.IsLocalization P.trW] (Y : C) : Function.Bijective L.map
• CategoryTheory.ObjectProperty.rightOrthogonal.map_bijective_of_isTriangulated 📋 Mathlib.CategoryTheory.Triangulated.Orthogonal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {P : CategoryTheory.ObjectProperty C} [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [P.IsTriangulated] [CategoryTheory.IsTriangulated C] {Y : C} (hY : P.rightOrthogonal Y) (L : CategoryTheory.Functor C D) [L.IsLocalization P.trW] (X : C) : Function.Bijective L.map
• CategoryTheory.ObjectProperty.trW_op 📋 Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (P : CategoryTheory.ObjectProperty C) [P.IsTriangulated] : P.op.trW = P.trW.op
• CategoryTheory.ObjectProperty.trW_of_op 📋 Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (P : CategoryTheory.ObjectProperty C) [P.IsTriangulated] {X Y : C} {f : X ⟶ Y} (hf : P.op.trW f.op) : P.trW f
• CategoryTheory.ObjectProperty.trW_op_iff 📋 Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (P : CategoryTheory.ObjectProperty C) [P.IsTriangulated] {X Y : Cᵒᵖ} {f : X ⟶ Y} : P.op.trW f ↔ P.trW f.unop
• CategoryTheory.ObjectProperty.trW_of_unop 📋 Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (P : CategoryTheory.ObjectProperty Cᵒᵖ) [P.IsTriangulated] {X Y : Cᵒᵖ} {f : X ⟶ Y} (hf : P.unop.trW f.unop) : P.trW f
• CategoryTheory.ObjectProperty.triangulatedLocalizerMorphism 📋 Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (A B : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [A.IsTriangulated] : CategoryTheory.LocalizerMorphism (B.inverseImage A.ι).trW B.trW
• CategoryTheory.ObjectProperty.IsVerdierLeftLocalizing.fac' 📋 Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A B : CategoryTheory.ObjectProperty C} [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] [A.IsVerdierLeftLocalizing B] {X Y : C} (s : X ⟶ Y) (hY : A Y) (hs : B.trW s) : ∃ Z s' a, A Z ∧ (A ⊓ B).trW s' ∧ CategoryTheory.CategoryStruct.comp a s = s'
• CategoryTheory.ObjectProperty.IsVerdierRightLocalizing.fac' 📋 Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A B : CategoryTheory.ObjectProperty C} [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] [A.IsVerdierRightLocalizing B] {X Y : C} (s : X ⟶ Y) (hX : A X) (hs : B.trW s) : ∃ Z s' b, A Z ∧ (A ⊓ B).trW s' ∧ CategoryTheory.CategoryStruct.comp s b = s'
• CategoryTheory.ObjectProperty.isVerdierLeftLocalizing_iff 📋 Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (A B : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] : A.IsVerdierLeftLocalizing B ↔ ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A Y → B.trW s → ∃ Z s' a, A Z ∧ (A ⊓ B).trW s' ∧ CategoryTheory.CategoryStruct.comp a s = s'
• CategoryTheory.ObjectProperty.isVerdierRightLocalizing_iff 📋 Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (A B : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] : A.IsVerdierRightLocalizing B ↔ ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A X → B.trW s → ∃ Z s' b, A Z ∧ (A ⊓ B).trW s' ∧ CategoryTheory.CategoryStruct.comp s b = s'
• CategoryTheory.ObjectProperty.instIsLocalizedFullyFaithfulFullSubcategoryTrWInverseImageιTriangulatedLocalizerMorphismOfIsVerdierLeftLocalizing 📋 Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (A B : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] [A.IsVerdierLeftLocalizing B] : (A.triangulatedLocalizerMorphism B).IsLocalizedFullyFaithful
• CategoryTheory.ObjectProperty.instIsLocalizedFullyFaithfulFullSubcategoryTrWInverseImageιTriangulatedLocalizerMorphismOfIsVerdierRightLocalizing 📋 Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (A B : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] [A.IsVerdierRightLocalizing B] : (A.triangulatedLocalizerMorphism B).IsLocalizedFullyFaithful
• CategoryTheory.ObjectProperty.instCommShiftFullSubcategoryFunctorTrWInverseImageιTriangulatedLocalizerMorphismInt 📋 Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (A B : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [A.IsTriangulated] : (A.triangulatedLocalizerMorphism B).functor.CommShift ℤ
• CategoryTheory.ObjectProperty.trW_inverseImage_ι_iff 📋 Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (A B : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [A.IsTriangulated] {X Y : A.FullSubcategory} (f : X ⟶ Y) : (B.inverseImage A.ι).trW f ↔ (A ⊓ B).trW f.hom
• CategoryTheory.ObjectProperty.instIsTriangulatedFullSubcategoryFunctorTrWInverseImageιTriangulatedLocalizerMorphism 📋 Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (A B : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [A.IsTriangulated] : (A.triangulatedLocalizerMorphism B).functor.IsTriangulated
• CategoryTheory.ObjectProperty.IsVerdierLeftLocalizing.fullyFaithful 📋 Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
  {C : Type u_1} {D₁ : Type u_3} {D₂ : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} D₁] [CategoryTheory.Category.{v_4, u_4} D₂] (A B : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] [A.IsVerdierLeftLocalizing B] {L₁ : CategoryTheory.Functor A.FullSubcategory D₁} {L₂ : CategoryTheory.Functor C D₂} {F : CategoryTheory.Functor D₁ D₂} [L₁.IsLocalization (B.inverseImage A.ι).trW] [L₂.IsLocalization B.trW] (e : L₁.comp F ≅ A.ι.comp L₂) : F.FullyFaithful
• CategoryTheory.ObjectProperty.IsVerdierRightLocalizing.fullyFaithful 📋 Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
  {C : Type u_1} {D₁ : Type u_3} {D₂ : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} D₁] [CategoryTheory.Category.{v_4, u_4} D₂] (A B : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] [A.IsVerdierRightLocalizing B] {L₁ : CategoryTheory.Functor A.FullSubcategory D₁} {L₂ : CategoryTheory.Functor C D₂} {F : CategoryTheory.Functor D₁ D₂} [L₁.IsLocalization (B.inverseImage A.ι).trW] [L₂.IsLocalization B.trW] (e : L₁.comp F ≅ A.ι.comp L₂) : F.FullyFaithful
• CategoryTheory.ObjectProperty.instFaithfulLocalizedFunctorFullSubcategoryTrWInverseImageιTriangulatedLocalizerMorphism 📋 Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
  {C : Type u_1} {D₁ : Type u_3} {D₂ : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} D₁] [CategoryTheory.Category.{v_4, u_4} D₂] (A B : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] [A.IsVerdierRightLocalizing B] (L₁ : CategoryTheory.Functor A.FullSubcategory D₁) (L₂ : CategoryTheory.Functor C D₂) [L₁.IsLocalization (B.inverseImage A.ι).trW] [L₂.IsLocalization B.trW] : ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Faithful
• CategoryTheory.ObjectProperty.instFullLocalizedFunctorFullSubcategoryTrWInverseImageιTriangulatedLocalizerMorphism 📋 Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
  {C : Type u_1} {D₁ : Type u_3} {D₂ : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} D₁] [CategoryTheory.Category.{v_4, u_4} D₂] (A B : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] [A.IsVerdierRightLocalizing B] (L₁ : CategoryTheory.Functor A.FullSubcategory D₁) (L₂ : CategoryTheory.Functor C D₂) [L₁.IsLocalization (B.inverseImage A.ι).trW] [L₂.IsLocalization B.trW] : ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Full
• CategoryTheory.ObjectProperty.instAdditiveLocalizedFunctorFullSubcategoryTrWInverseImageιTriangulatedLocalizerMorphism 📋 Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
  {C : Type u_1} {D₁ : Type u_3} {D₂ : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} D₁] [CategoryTheory.Category.{v_4, u_4} D₂] (A B : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] (L₁ : CategoryTheory.Functor A.FullSubcategory D₁) (L₂ : CategoryTheory.Functor C D₂) [L₁.IsLocalization (B.inverseImage A.ι).trW] [L₂.IsLocalization B.trW] [CategoryTheory.Preadditive D₁] [CategoryTheory.Preadditive D₂] [L₁.Additive] [L₂.Additive] : ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Additive
• CategoryTheory.ObjectProperty.instAdditiveLocalizedFunctorFullSubcategoryTrWInverseImageιTriangulatedLocalizerMorphism_1 📋 Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
  {C : Type u_1} {D₁ : Type u_3} {D₂ : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} D₁] [CategoryTheory.Category.{v_4, u_4} D₂] (A B : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] (L₁ : CategoryTheory.Functor A.FullSubcategory D₁) (L₂ : CategoryTheory.Functor C D₂) [L₁.IsLocalization (B.inverseImage A.ι).trW] [L₂.IsLocalization B.trW] [CategoryTheory.Preadditive D₁] [CategoryTheory.Preadditive D₂] [L₁.Additive] [L₂.Additive] : ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Additive
• CategoryTheory.ObjectProperty.inverseImage_opEquivalence_inverse_trW_inverseImage_ι_op 📋 Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (A B : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] : (B.op.inverseImage A.op.ι).trW.inverseImage A.opEquivalence.inverse = (B.inverseImage A.ι).op.trW
• HomotopyCategory.Plus.quasiIso_eq_subcategoryAcyclic_trW 📋 Mathlib.Algebra.Homology.DerivedCategory.Plus
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : HomotopyCategory.Plus.quasiIso C = (HomotopyCategory.Plus.subcategoryAcyclic C).trW
• DerivedCategory.Plus.instIsLocalizationPlusQhTrWSubcategoryAcyclic 📋 Mathlib.Algebra.Homology.DerivedCategory.Plus
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : DerivedCategory.Plus.Qh.IsLocalization (HomotopyCategory.Plus.subcategoryAcyclic C).trW

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:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. 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 ?a

   If 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 ?b

4. By 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 find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. 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