Loogle!

Result

Found 54 declarations mentioning CategoryTheory.Limits.PreservesFilteredColimitsOfSize.

• CategoryTheory.Limits.PreservesFilteredColimitsOfSize 📋 Mathlib.CategoryTheory.Limits.Preserves.Filtered
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : Prop
• CategoryTheory.Limits.preservesFilteredColimitsOfSize_shrink 📋 Mathlib.CategoryTheory.Limits.Preserves.Filtered
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
• CategoryTheory.Limits.preservesSmallestFilteredColimits_of_preservesFilteredColimits 📋 Mathlib.CategoryTheory.Limits.Preserves.Filtered
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
• CategoryTheory.Limits.PreservesColimits.preservesFilteredColimits 📋 Mathlib.CategoryTheory.Limits.Preserves.Filtered
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
• CategoryTheory.Limits.preservesFilteredColimitsOfSize_of_univLE 📋 Mathlib.CategoryTheory.Limits.Preserves.Filtered
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
• CategoryTheory.Limits.PreservesFilteredColimitsOfSize.mk 📋 Mathlib.CategoryTheory.Limits.Preserves.Filtered
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (preserves_filtered_colimits : ∀ (J : Type w) [inst : CategoryTheory.Category.{w', w} J] [CategoryTheory.IsFiltered J], CategoryTheory.Limits.PreservesColimitsOfShape J F) : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F
• CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits 📋 Mathlib.CategoryTheory.Limits.Preserves.Filtered
  {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} D} {F : CategoryTheory.Functor C D} [self : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F] (J : Type w) [CategoryTheory.Category.{w', w} J] [CategoryTheory.IsFiltered J] : CategoryTheory.Limits.PreservesColimitsOfShape J F
• CategoryTheory.Limits.comp_preservesFilteredColimits 📋 Mathlib.CategoryTheory.Limits.Preserves.Filtered
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w', v₂, v₃, u₂, u₃} G] : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w', v₁, v₃, u₁, u₃} (F.comp G)
• CategoryTheory.FinallySmall.preservesColimitsOfShape_of_isFiltered 📋 Mathlib.CategoryTheory.Filtered.FinallySmall
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.FinallySmall C] {D : Type u_1} {E : Type u_2} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Category.{v_2, u_2} E] (F : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v_1, v_2, u_1, u_2} F] : CategoryTheory.Limits.PreservesColimitsOfShape C F
• CategoryTheory.Limits.instPreservesFilteredColimitsOfSizeUnderForget 📋 Mathlib.CategoryTheory.Limits.Preserves.Over
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X : C} : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u_2, u_3, v_1, v_1, max u_1 v_1, u_1} (CategoryTheory.Under.forget X)
• CategoryTheory.Functor.IsFinitelyAccessible_iff_preservesFilteredColimitsOfSize 📋 Mathlib.CategoryTheory.Presentable.Finite
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F : CategoryTheory.Functor C D} : F.IsFinitelyAccessible ↔ CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v, v', u, u'} F
• CategoryTheory.instPreservesFilteredColimitsOfSizeObjOppositeFunctorTypeCoyonedaOpOfIsFinitelyPresentable 📋 Mathlib.CategoryTheory.Presentable.Finite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.IsFinitelyPresentable X] : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v, v, u, v + 1} (CategoryTheory.coyoneda.obj (Opposite.op X))
• CategoryTheory.isFinitelyPresentable_iff_preservesFilteredColimitsOfSize 📋 Mathlib.CategoryTheory.Presentable.Finite
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} : CategoryTheory.IsFinitelyPresentable X ↔ CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v, v, u, v + 1} (CategoryTheory.coyoneda.obj (Opposite.op X))
• CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfShapeOppositeElementsFiberForget 📋 Mathlib.CategoryTheory.Sites.Point.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w'} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)] [CategoryTheory.LocallySmall.{w, v, u} C] : CategoryTheory.Limits.PreservesColimitsOfShape Φ.fiber.Elementsᵒᵖ (CategoryTheory.forget A)
• CategoryTheory.GrothendieckTopology.Point.W_isInvertedBy_presheafFiber' 📋 Mathlib.CategoryTheory.Sites.Point.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w'} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)] [CategoryTheory.LocallySmall.{w, v, u} C] [J.WEqualsLocallyBijective A] [(CategoryTheory.forget A).ReflectsIsomorphisms] : J.W.IsInvertedBy Φ.presheafFiber
• CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso 📋 Mathlib.CategoryTheory.Sites.Point.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] {B : Type u''} [CategoryTheory.Category.{v'', u''} B] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} B] (F : CategoryTheory.Functor A B) [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F] [J.HasSheafCompose F] : (CategoryTheory.sheafCompose J F).comp Φ.sheafFiber ≅ Φ.sheafFiber.comp F
• CategoryTheory.GrothendieckTopology.Point.presheafFiberCompIso 📋 Mathlib.CategoryTheory.Sites.Point.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] {B : Type u''} [CategoryTheory.Category.{v'', u''} B] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} B] (F : CategoryTheory.Functor A B) [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F] : ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).comp Φ.presheafFiber ≅ Φ.presheafFiber.comp F
• CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_jointly_surjective 📋 Mathlib.CategoryTheory.Sites.Point.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w'} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] {P : CategoryTheory.Functor Cᵒᵖ A} [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)] [CategoryTheory.LocallySmall.{w, v, u} C] (p : CategoryTheory.ToType (Φ.presheafFiber.obj P)) : ∃ X x z, (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z = p
• CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_map_injective 📋 Mathlib.CategoryTheory.Sites.Point.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w'} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] {P Q : CategoryTheory.Functor Cᵒᵖ A} [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)] [CategoryTheory.LocallySmall.{w, v, u} C] (f : P ⟶ Q) [CategoryTheory.Presheaf.IsLocallyInjective J f] : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (Φ.presheafFiber.map f))
• CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_map_surjective 📋 Mathlib.CategoryTheory.Sites.Point.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w'} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] {P Q : CategoryTheory.Functor Cᵒᵖ A} [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)] [CategoryTheory.LocallySmall.{w, v, u} C] (f : P ⟶ Q) [CategoryTheory.Presheaf.IsLocallySurjective J f] : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Φ.presheafFiber.map f))
• CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_map_bijective 📋 Mathlib.CategoryTheory.Sites.Point.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w'} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] {P Q : CategoryTheory.Functor Cᵒᵖ A} [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)] [CategoryTheory.LocallySmall.{w, v, u} C] (f : P ⟶ Q) [CategoryTheory.Presheaf.IsLocallyInjective J f] [CategoryTheory.Presheaf.IsLocallySurjective J f] : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom (Φ.presheafFiber.map f))
• CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_jointly_surjective₂ 📋 Mathlib.CategoryTheory.Sites.Point.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w'} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] {P : CategoryTheory.Functor Cᵒᵖ A} [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)] [CategoryTheory.LocallySmall.{w, v, u} C] (p₁ p₂ : CategoryTheory.ToType (Φ.presheafFiber.obj P)) : ∃ X x z₁ z₂, (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z₁ = p₁ ∧ (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z₂ = p₂
• CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberCompIso_hom_app 📋 Mathlib.CategoryTheory.Sites.Point.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] {B : Type u''} [CategoryTheory.Category.{v'', u''} B] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} B] (F : CategoryTheory.Functor A B) [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F] (X : C) (x : Φ.fiber.obj X) (P : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (P.comp F)) ((Φ.presheafFiberCompIso F).hom.app P) = F.map (Φ.toPresheafFiber X x P)
• CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberCompIso_hom_app_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] {B : Type u''} [CategoryTheory.Category.{v'', u''} B] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} B] (F : CategoryTheory.Functor A B) [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F] (X : C) (x : Φ.fiber.obj X) (P : CategoryTheory.Functor Cᵒᵖ A) {Z : B} (h : F.obj (Φ.presheafFiber.obj P) ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (P.comp F)) (CategoryTheory.CategoryStruct.comp ((Φ.presheafFiberCompIso F).hom.app P) h) = CategoryTheory.CategoryStruct.comp (F.map (Φ.toPresheafFiber X x P)) h
• CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_eq_iff' 📋 Mathlib.CategoryTheory.Sites.Point.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w'} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] {P : CategoryTheory.Functor Cᵒᵖ A} [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)] [CategoryTheory.LocallySmall.{w, v, u} C] (X : C) (x : Φ.fiber.obj X) (z₁ z₂ : CategoryTheory.ToType (P.obj (Opposite.op X))) : (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z₁ = (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z₂ ↔ ∃ Y f y, (CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f)) y = x ∧ (CategoryTheory.ConcreteCategory.hom (P.map f.op)) z₁ = (CategoryTheory.ConcreteCategory.hom (P.map f.op)) z₂
• CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso_hom_app 📋 Mathlib.CategoryTheory.Sites.Point.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] {B : Type u''} [CategoryTheory.Category.{v'', u''} B] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} B] (F : CategoryTheory.Functor A B) [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F] [J.HasSheafCompose F] (X : CategoryTheory.Sheaf J A) : (Φ.sheafFiberCompIso F).hom.app X = CategoryTheory.CategoryStruct.comp ((Φ.presheafFiberCompIso F).hom.app X.obj) (CategoryTheory.CategoryStruct.id (F.obj (Φ.presheafFiber.obj X.obj)))
• CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso_inv_app 📋 Mathlib.CategoryTheory.Sites.Point.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] {B : Type u''} [CategoryTheory.Category.{v'', u''} B] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} B] (F : CategoryTheory.Functor A B) [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F] [J.HasSheafCompose F] (X : CategoryTheory.Sheaf J A) : (Φ.sheafFiberCompIso F).inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (F.obj (Φ.presheafFiber.obj X.obj))) ((Φ.presheafFiberCompIso F).inv.app X.obj)
• AlgebraicGeometry.Scheme.instHasSheafifyAffineEtaleTopology 📋 Mathlib.AlgebraicGeometry.Sites.AffineEtale
  {S : AlgebraicGeometry.Scheme} {A : Type u'} [CategoryTheory.Category.{u, u'} A] {FA : A → A → Type u_1} {CD : A → Type u} [(X Y : A) → FunLike (FA X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [CategoryTheory.Limits.HasColimits A] [CategoryTheory.Limits.HasLimits A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A)] : CategoryTheory.HasSheafify (AlgebraicGeometry.Scheme.AffineEtale.topology S) A
• AlgebraicGeometry.Scheme.instHasSheafifyEtaleSmallEtaleTopology 📋 Mathlib.AlgebraicGeometry.Sites.AffineEtale
  {S : AlgebraicGeometry.Scheme} {A : Type u'} [CategoryTheory.Category.{u, u'} A] {FA : A → A → Type u_1} {CD : A → Type u} [(X Y : A) → FunLike (FA X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [CategoryTheory.Limits.HasColimits A] [CategoryTheory.Limits.HasLimits A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A)] : CategoryTheory.HasSheafify S.smallEtaleTopology A
• AlgebraicGeometry.Scheme.instWEqualsLocallyBijectiveAffineEtaleTopology 📋 Mathlib.AlgebraicGeometry.Sites.AffineEtale
  {S : AlgebraicGeometry.Scheme} {A : Type u'} [CategoryTheory.Category.{u, u'} A] {FA : A → A → Type u_1} {CD : A → Type u} [(X Y : A) → FunLike (FA X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [CategoryTheory.Limits.HasColimits A] [CategoryTheory.Limits.HasLimits A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A)] : (AlgebraicGeometry.Scheme.AffineEtale.topology S).WEqualsLocallyBijective A
• AlgebraicGeometry.Scheme.instWEqualsLocallyBijectiveEtaleSmallEtaleTopology 📋 Mathlib.AlgebraicGeometry.Sites.AffineEtale
  {S : AlgebraicGeometry.Scheme} {A : Type u'} [CategoryTheory.Category.{u, u'} A] {FA : A → A → Type u_1} {CD : A → Type u} [(X Y : A) → FunLike (FA X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [CategoryTheory.Limits.HasColimits A] [CategoryTheory.Limits.HasLimits A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A)] : S.smallEtaleTopology.WEqualsLocallyBijective A
• AlgebraicGeometry.Scheme.instAbelianSheafAffineEtaleTopology 📋 Mathlib.AlgebraicGeometry.Sites.AffineEtale
  {S : AlgebraicGeometry.Scheme} {A : Type u'} [CategoryTheory.Category.{u, u'} A] {FA : A → A → Type u_1} {CD : A → Type u} [(X Y : A) → FunLike (FA X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [CategoryTheory.Limits.HasColimits A] [CategoryTheory.Limits.HasLimits A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A)] [CategoryTheory.Abelian A] : CategoryTheory.Abelian (CategoryTheory.Sheaf (AlgebraicGeometry.Scheme.AffineEtale.topology S) A)
• AlgebraicGeometry.Scheme.instAbelianSheafEtaleSmallEtaleTopology 📋 Mathlib.AlgebraicGeometry.Sites.AffineEtale
  {S : AlgebraicGeometry.Scheme} {A : Type u'} [CategoryTheory.Category.{u, u'} A] {FA : A → A → Type u_1} {CD : A → Type u} [(X Y : A) → FunLike (FA X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [CategoryTheory.Limits.HasColimits A] [CategoryTheory.Limits.HasLimits A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A)] [CategoryTheory.Abelian A] : CategoryTheory.Abelian (CategoryTheory.Sheaf S.smallEtaleTopology A)
• AlgebraicGeometry.Scheme.isGrothendieckAbelian_sheaf_affineEtaleTopology 📋 Mathlib.AlgebraicGeometry.Sites.AffineEtale
  (S : AlgebraicGeometry.Scheme) (A : Type u') [CategoryTheory.Category.{u, u'} A] {FA : A → A → Type u_1} {CD : A → Type u} [(X Y : A) → FunLike (FA X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [CategoryTheory.Limits.HasColimits A] [CategoryTheory.Limits.HasLimits A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A)] [CategoryTheory.Abelian A] [CategoryTheory.IsGrothendieckAbelian.{u, u, u'} A] : CategoryTheory.IsGrothendieckAbelian.{u, u + 1, max (max u' (u + 1)) u} (CategoryTheory.Sheaf (AlgebraicGeometry.Scheme.AffineEtale.topology S) A)
• AlgebraicGeometry.Scheme.isGrothendieckAbelian_sheaf_smallEtaleTopology 📋 Mathlib.AlgebraicGeometry.Sites.AffineEtale
  (S : AlgebraicGeometry.Scheme) (A : Type u') [CategoryTheory.Category.{u, u'} A] {FA : A → A → Type u_1} {CD : A → Type u} [(X Y : A) → FunLike (FA X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [CategoryTheory.Limits.HasColimits A] [CategoryTheory.Limits.HasLimits A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A)] [CategoryTheory.Abelian A] [CategoryTheory.IsGrothendieckAbelian.{u, u, u'} A] : CategoryTheory.IsGrothendieckAbelian.{u, u + 1, max (max u' (u + 1)) u} (CategoryTheory.Sheaf S.smallEtaleTopology A)
• CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms 📋 Mathlib.CategoryTheory.Sites.Point.Conservative
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)] [hJ : J.HasSheafCompose (CategoryTheory.forget A)] : CategoryTheory.JointlyReflectIsomorphisms fun Φ => Φ.obj.sheafFiber
• CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectEpimorphisms 📋 Mathlib.CategoryTheory.Sites.Point.Conservative
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)] [hJ : J.HasSheafCompose (CategoryTheory.forget A)] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.Limits.HasProducts A] : CategoryTheory.JointlyReflectEpimorphisms fun Φ => Φ.obj.sheafFiber
• CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyFaithful 📋 Mathlib.CategoryTheory.Sites.Point.Conservative
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)] [hJ : J.HasSheafCompose (CategoryTheory.forget A)] [CategoryTheory.AB5OfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasFiniteLimits A] : CategoryTheory.JointlyFaithful fun Φ => Φ.obj.sheafFiber
• CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectMonomorphisms 📋 Mathlib.CategoryTheory.Sites.Point.Conservative
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)] [hJ : J.HasSheafCompose (CategoryTheory.forget A)] [CategoryTheory.AB5OfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasFiniteLimits A] : CategoryTheory.JointlyReflectMonomorphisms fun Φ => Φ.obj.sheafFiber
• CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.W_iff 📋 Mathlib.CategoryTheory.Sites.Point.Conservative
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)] [hJ : J.HasSheafCompose (CategoryTheory.forget A)] {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.Limits.HasProducts A] : J.W f ↔ ∀ (Φ : P.FullSubcategory), CategoryTheory.IsIso (Φ.obj.presheafFiber.map f)
• CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_isLocallySurjective 📋 Mathlib.CategoryTheory.Sites.Point.Conservative
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)] [J.WEqualsLocallyBijective (Type w)] [CategoryTheory.HasSheafify J (Type w)] {X Y : CategoryTheory.Functor Cᵒᵖ A} (f : X ⟶ Y) (hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Φ.obj.presheafFiber.map f))) : CategoryTheory.Presheaf.IsLocallySurjective J f
• CategoryTheory.ObjectProperty.ind_inverseImage_le 📋 Mathlib.CategoryTheory.ObjectProperty.Ind
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v, u_2, u, u_1} F] : (P.inverseImage F).ind ≤ P.ind.inverseImage F
• PartOrdEmb.Limits.instPreservesFilteredColimitsOfSizeForgetOrderEmbeddingCarrier 📋 Mathlib.Order.Category.PartOrdEmb
  : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u + 1, u + 1} (CategoryTheory.forget PartOrdEmb)
• CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfShapeOppositeElementsFiberObjFunctorCurriedTensor 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.LocallySmall.{w, v, u} C] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorLeft X)] (M : A) : CategoryTheory.Limits.PreservesColimitsOfShape Φ.fiber.Elementsᵒᵖ ((CategoryTheory.MonoidalCategory.curriedTensor A).obj M)
• CategoryTheory.GrothendieckTopology.Point.instMonoidalFunctorOppositePresheafFiber 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorRight X)] : Φ.presheafFiber.Monoidal
• CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfShapeOppositeElementsFiberObjFunctorFlipCurriedTensor 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.LocallySmall.{w, v, u} C] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorRight X)] (M : A) : CategoryTheory.Limits.PreservesColimitsOfShape Φ.fiber.Elementsᵒᵖ ((CategoryTheory.MonoidalCategory.curriedTensor A).flip.obj M)
• CategoryTheory.GrothendieckTopology.Point.instMonoidalSheafSheafFiber 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorRight X)] [J.W.IsMonoidal] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.Limits.HasProducts A] : Φ.sheafFiber.Monoidal
• CategoryTheory.GrothendieckTopology.Point.instIsIsoδFunctorOppositePresheafFiber 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorRight X)] (P₁ P₂ : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.δ Φ.presheafFiber P₁ P₂)
• CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_ε 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorRight X)] (X : C) (x : Φ.fiber.obj X) : CategoryTheory.Functor.LaxMonoidal.ε Φ.presheafFiber = Φ.toPresheafFiber X x (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor Cᵒᵖ A))
• CategoryTheory.GrothendieckTopology.Point.instIsMonoidalFunctorOppositeHomPresheafToSheafCompSheafFiberIso 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorRight X)] [J.W.IsMonoidal] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.Limits.HasProducts A] : CategoryTheory.NatTrans.IsMonoidal (Φ.presheafToSheafCompSheafFiberIso A).hom
• CategoryTheory.GrothendieckTopology.Point.tensorHom_comp_toPresheafFiber_μ 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorRight X)] (X : C) (x : Φ.fiber.obj X) (G₁ G₂ : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (Φ.toPresheafFiber X x G₁) (Φ.toPresheafFiber X x G₂)) (CategoryTheory.Functor.LaxMonoidal.μ Φ.presheafFiber G₁ G₂) = Φ.toPresheafFiber X x (CategoryTheory.MonoidalCategoryStruct.tensorObj G₁ G₂)
• CategoryTheory.GrothendieckTopology.Point.tensorHom_comp_toPresheafFiber_μ_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorRight X)] (X : C) (x : Φ.fiber.obj X) (G₁ G₂ : CategoryTheory.Functor Cᵒᵖ A) {Z : A} (h : Φ.presheafFiber.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj G₁ G₂) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (Φ.toPresheafFiber X x G₁) (Φ.toPresheafFiber X x G₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ Φ.presheafFiber G₁ G₂) h) = CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (CategoryTheory.MonoidalCategoryStruct.tensorObj G₁ G₂)) h
• CategoryTheory.instIsMonoidalFunctorOppositeWOfHasSheafComposeForgetOfHasEnoughPoints 📋 Mathlib.CategoryTheory.Sites.Point.IsMonoidalW
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {J : CategoryTheory.GrothendieckTopology C} (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasProducts A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [CategoryTheory.HasWeakSheafify J A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorRight X)] [J.HasSheafCompose (CategoryTheory.forget A)] [J.HasEnoughPoints] : J.W.IsMonoidal
• CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.isMonoidal_W 📋 Mathlib.CategoryTheory.Sites.Point.IsMonoidalW
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasProducts A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [CategoryTheory.HasWeakSheafify J A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorRight X)] [J.HasSheafCompose (CategoryTheory.forget A)] : J.W.IsMonoidal

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 ce5dd8c