Loogle!

Result

Found 62 declarations mentioning CategoryTheory.ObjectProperty.isoModSerre.

• CategoryTheory.ObjectProperty.isoModSerre 📋 Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] : CategoryTheory.MorphismProperty C
• CategoryTheory.ObjectProperty.instHasTwoOutOfThreePropertyIsoModSerre 📋 Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] : P.isoModSerre.HasTwoOutOfThreeProperty
• CategoryTheory.ObjectProperty.instIsMultiplicativeIsoModSerre 📋 Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] : P.isoModSerre.IsMultiplicative
• CategoryTheory.ObjectProperty.instIsStableUnderBaseChangeIsoModSerre 📋 Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] : P.isoModSerre.IsStableUnderBaseChange
• CategoryTheory.ObjectProperty.instIsStableUnderCobaseChangeIsoModSerre 📋 Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] : P.isoModSerre.IsStableUnderCobaseChange
• CategoryTheory.ObjectProperty.instIsStableUnderRetractsIsoModSerre 📋 Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] : P.isoModSerre.IsStableUnderRetracts
• CategoryTheory.ObjectProperty.isoModSerre_of_isIso 📋 Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : P.isoModSerre f
• CategoryTheory.ObjectProperty.isoModSerre_of_epi 📋 Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] (hf : P.monoModSerre f) : P.isoModSerre f
• CategoryTheory.ObjectProperty.isoModSerre_of_mono 📋 Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] (hf : P.epiModSerre f) : P.isoModSerre f
• CategoryTheory.ObjectProperty.isoModSerre_iff_of_epi 📋 Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] : P.isoModSerre f ↔ P.monoModSerre f
• CategoryTheory.ObjectProperty.isoModSerre_iff_of_mono 📋 Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] : P.isoModSerre f ↔ P.epiModSerre f
• CategoryTheory.ObjectProperty.isoModSerre_iff 📋 Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] {X Y : C} (f : X ⟶ Y) : P.isoModSerre f ↔ P.monoModSerre f ∧ P.epiModSerre f
• CategoryTheory.ObjectProperty.isoModSerre_zero_iff 📋 Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] (X Y : C) : P.isoModSerre 0 ↔ P X ∧ P Y
• CategoryTheory.ObjectProperty.isomorphisms_le_isoModSerre 📋 Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] : CategoryTheory.MorphismProperty.isomorphisms C ≤ P.isoModSerre
• CategoryTheory.ObjectProperty.isoModSerre_isInvertedBy_iff 📋 Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : P.isoModSerre.IsInvertedBy F ↔ P ≤ F.kernel
• CategoryTheory.ObjectProperty.le_kernel_of_isoModSerre_isInvertedBy 📋 Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (hF : P.isoModSerre.IsInvertedBy F) : P ≤ F.kernel
• CategoryTheory.Abelian.isoModSerre_kernel_eq_inverseImage_isomorphisms 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] (G : CategoryTheory.Functor D C) [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] : G.kernel.isoModSerre = (CategoryTheory.MorphismProperty.isomorphisms C).inverseImage G
• CategoryTheory.Abelian.isLocalization_isoModSerre_kernel_of_leftAdjoint 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] {G : CategoryTheory.Functor D C} [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] {F : CategoryTheory.Functor C D} (adj : G ⊣ F) [F.Full] [F.Faithful] : G.IsLocalization G.kernel.isoModSerre
• CategoryTheory.Abelian.isoModSerre_kernel_eq_isLocal_of_rightAdjoint 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] {G : CategoryTheory.Functor D C} [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] {F : CategoryTheory.Functor C D} (adj : G ⊣ F) [F.Full] [F.Faithful] : G.kernel.isoModSerre = CategoryTheory.ObjectProperty.isLocal fun x => x ∈ Set.range F.obj
• CategoryTheory.ObjectProperty.SerreClassLocalization.instHasLeftCalculusOfFractionsIsoModSerre 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] : P.isoModSerre.HasLeftCalculusOfFractions
• CategoryTheory.ObjectProperty.SerreClassLocalization.instHasRightCalculusOfFractionsIsoModSerre 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] : P.isoModSerre.HasRightCalculusOfFractions
• CategoryTheory.ObjectProperty.SerreClassLocalization.abelian 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : CategoryTheory.Abelian D
• CategoryTheory.ObjectProperty.SerreClassLocalization.hasCoequalizers 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : CategoryTheory.Limits.HasCoequalizers D
• CategoryTheory.ObjectProperty.SerreClassLocalization.hasEqualizers 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : CategoryTheory.Limits.HasEqualizers D
• CategoryTheory.ObjectProperty.SerreClassLocalization.hasFiniteProducts 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : CategoryTheory.Limits.HasFiniteProducts D
• CategoryTheory.ObjectProperty.SerreClassLocalization.hasZeroObject 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : CategoryTheory.Limits.HasZeroObject D
• CategoryTheory.ObjectProperty.SerreClassLocalization.preservesEpimorphisms 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : L.PreservesEpimorphisms
• CategoryTheory.ObjectProperty.SerreClassLocalization.preservesFiniteColimits 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : CategoryTheory.Limits.PreservesFiniteColimits L
• CategoryTheory.ObjectProperty.SerreClassLocalization.preservesFiniteLimits 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : CategoryTheory.Limits.PreservesFiniteLimits L
• CategoryTheory.ObjectProperty.SerreClassLocalization.preservesMonomorphisms 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : L.PreservesMonomorphisms
• CategoryTheory.ObjectProperty.SerreClassLocalization.hasCokernels 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : CategoryTheory.Limits.HasCokernels D
• CategoryTheory.ObjectProperty.SerreClassLocalization.hasKernels 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : CategoryTheory.Limits.HasKernels D
• CategoryTheory.ObjectProperty.SerreClassLocalization.isNormalEpiCategory 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : CategoryTheory.IsNormalEpiCategory D
• CategoryTheory.ObjectProperty.SerreClassLocalization.isNormalMonoCategory 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : CategoryTheory.IsNormalMonoCategory D
• CategoryTheory.ObjectProperty.SerreClassLocalization.isZero_obj_iff 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] (X : C) : CategoryTheory.Limits.IsZero (L.obj X) ↔ P X
• CategoryTheory.ObjectProperty.SerreClassLocalization.inverseImage_epimorphisms 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : (CategoryTheory.MorphismProperty.epimorphisms D).inverseImage L = P.epiModSerre
• CategoryTheory.ObjectProperty.SerreClassLocalization.inverseImage_isomorphisms 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : (CategoryTheory.MorphismProperty.isomorphisms D).inverseImage L = P.isoModSerre
• CategoryTheory.ObjectProperty.SerreClassLocalization.inverseImage_monomorphisms 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : (CategoryTheory.MorphismProperty.monomorphisms D).inverseImage L = P.monoModSerre
• CategoryTheory.ObjectProperty.SerreClassLocalization.exactFunctor_comp_iff 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] {E : Type u''} [CategoryTheory.Category.{v'', u''} E] [CategoryTheory.Abelian E] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] (G : CategoryTheory.Functor D E) : CategoryTheory.exactFunctor C E (L.comp G) ↔ CategoryTheory.exactFunctor D E G
• CategoryTheory.ObjectProperty.SerreClassLocalization.preservesFiniteColimits_comp_iff 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] {E : Type u''} [CategoryTheory.Category.{v'', u''} E] [CategoryTheory.Abelian E] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] (G : CategoryTheory.Functor D E) : CategoryTheory.Limits.PreservesFiniteColimits (L.comp G) ↔ CategoryTheory.Limits.PreservesFiniteColimits G
• CategoryTheory.ObjectProperty.SerreClassLocalization.preservesFiniteLimits_comp_iff 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] {E : Type u''} [CategoryTheory.Category.{v'', u''} E] [CategoryTheory.Abelian E] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] (G : CategoryTheory.Functor D E) : CategoryTheory.Limits.PreservesFiniteLimits (L.comp G) ↔ CategoryTheory.Limits.PreservesFiniteLimits G
• CategoryTheory.ObjectProperty.SerreClassLocalization.epi_map_iff 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Epi (L.map f) ↔ P.epiModSerre f
• CategoryTheory.ObjectProperty.SerreClassLocalization.isIso_map_iff 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] {X Y : C} (f : X ⟶ Y) : CategoryTheory.IsIso (L.map f) ↔ P.isoModSerre f
• CategoryTheory.ObjectProperty.SerreClassLocalization.mono_map_iff 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Mono (L.map f) ↔ P.monoModSerre f
• CategoryTheory.ObjectProperty.SerreClassLocalization.whiskeringLeft 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] (E : Type u'') [CategoryTheory.Category.{v'', u''} E] [CategoryTheory.Abelian E] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : CategoryTheory.Functor (D ⥤ₑ E) (C ⥤ₑ E)
• CategoryTheory.ObjectProperty.SerreClassLocalization.preservesCokernel 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) L
• CategoryTheory.ObjectProperty.SerreClassLocalization.preservesKernel 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) L
• CategoryTheory.ObjectProperty.SerreClassLocalization.fullyFaithfulWhiskeringLeft 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] (E : Type u'') [CategoryTheory.Category.{v'', u''} E] [CategoryTheory.Abelian E] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : (CategoryTheory.ObjectProperty.SerreClassLocalization.whiskeringLeft L P E).FullyFaithful
• CategoryTheory.ObjectProperty.SerreClassLocalization.instFaithfulExactFunctorWhiskeringLeft 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] (E : Type u'') [CategoryTheory.Category.{v'', u''} E] [CategoryTheory.Abelian E] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : (CategoryTheory.ObjectProperty.SerreClassLocalization.whiskeringLeft L P E).Faithful
• CategoryTheory.ObjectProperty.SerreClassLocalization.instFullExactFunctorWhiskeringLeft 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] (E : Type u'') [CategoryTheory.Category.{v'', u''} E] [CategoryTheory.Abelian E] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : (CategoryTheory.ObjectProperty.SerreClassLocalization.whiskeringLeft L P E).Full
• CategoryTheory.ObjectProperty.SerreClassLocalization.epi_iff 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] {X Y : D} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ ∃ X' Y' f', ∃ (_ : CategoryTheory.Epi f'), Nonempty (CategoryTheory.Arrow.mk (L.map f') ≅ CategoryTheory.Arrow.mk f)
• CategoryTheory.ObjectProperty.SerreClassLocalization.mono_iff 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] {X Y : D} (f : X ⟶ Y) : CategoryTheory.Mono f ↔ ∃ X' Y' f', ∃ (_ : CategoryTheory.Mono f'), Nonempty (CategoryTheory.Arrow.mk (L.map f') ≅ CategoryTheory.Arrow.mk f)
• CategoryTheory.ObjectProperty.SerreClassLocalization.whiskeringLeft_obj_obj 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] (E : Type u'') [CategoryTheory.Category.{v'', u''} E] [CategoryTheory.Abelian E] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] (G : D ⥤ₑ E) : ((CategoryTheory.ObjectProperty.SerreClassLocalization.whiskeringLeft L P E).obj G).obj = L.comp G.obj
• CategoryTheory.ObjectProperty.SerreClassLocalization.essImage_whiskeringLeft 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] (E : Type u'') [CategoryTheory.Category.{v'', u''} E] [CategoryTheory.Abelian E] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : (CategoryTheory.ObjectProperty.SerreClassLocalization.whiskeringLeft L P E).essImage = fun G => P.isoModSerre.IsInvertedBy G.obj
• CategoryTheory.ObjectProperty.SerreClassLocalization.map_comp_eq_zero_iff_of_epi_mono 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] {X Z Y : C} (f : X ⟶ Z) (g : Z ⟶ Y) [CategoryTheory.Epi f] [CategoryTheory.Mono g] : CategoryTheory.CategoryStruct.comp (L.map f) (L.map g) = 0 ↔ P Z
• CategoryTheory.ObjectProperty.exists_comp_isoModSerre_eq_zero_iff 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] {X Y : C} (f : X ⟶ Y) : (∃ Y' s, ∃ (_ : P.isoModSerre s), CategoryTheory.CategoryStruct.comp f s = 0) ↔ P (CategoryTheory.Abelian.image f)
• CategoryTheory.ObjectProperty.exists_isoModSerre_comp_eq_zero_iff 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] {X Y : C} (f : X ⟶ Y) : (∃ X' s, ∃ (_ : P.isoModSerre s), CategoryTheory.CategoryStruct.comp s f = 0) ↔ P (CategoryTheory.Abelian.image f)
• CategoryTheory.ObjectProperty.epiModSerre.isoModSerre_image_ι 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CategoryTheory.ObjectProperty C} [P.IsSerreClass] {X Y : C} {f : X ⟶ Y} (hf : P.epiModSerre f) : P.isoModSerre (CategoryTheory.Abelian.image.ι f)
• CategoryTheory.ObjectProperty.monoModSerre.isoModSerre_factorThruImage 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CategoryTheory.ObjectProperty C} [P.IsSerreClass] {X Y : C} {f : X ⟶ Y} (hf : P.monoModSerre f) : P.isoModSerre (CategoryTheory.Abelian.factorThruImage f)
• CategoryTheory.ObjectProperty.SerreClassLocalization.map_eq_zero_iff 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] {X Y : C} (f : X ⟶ Y) : L.map f = 0 ↔ P (CategoryTheory.Abelian.image f)
• CategoryTheory.ObjectProperty.SerreClassLocalization.epi_map_tfae 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] {X Y : C} (f : X ⟶ Y) : [CategoryTheory.Epi (L.map f), P.epiModSerre f, ∀ ⦃Z : C⦄ (z : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (L.map f) (L.map z) = 0 → L.map z = 0].TFAE
• CategoryTheory.ObjectProperty.SerreClassLocalization.mono_map_tfae 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] {X Y : C} (f : X ⟶ Y) : [CategoryTheory.Mono (L.map f), P.monoModSerre f, ∀ ⦃Z : C⦄ (z : Z ⟶ X), CategoryTheory.CategoryStruct.comp (L.map z) (L.map f) = 0 → L.map z = 0].TFAE

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