Loogle!

Result

Found 95 declarations mentioning CategoryTheory.GrothendieckTopology.Subcanonical.

• CategoryTheory.GrothendieckTopology.Subcanonical 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) : Prop
• CategoryTheory.GrothendieckTopology.instSubcanonicalCanonicalTopology 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] : (CategoryTheory.Sheaf.canonicalTopology C).Subcanonical
• CategoryTheory.GrothendieckTopology.le_canonical 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : J ≤ CategoryTheory.Sheaf.canonicalTopology C
• CategoryTheory.GrothendieckTopology.Subcanonical.le_canonical 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.GrothendieckTopology C} [self : J.Subcanonical] : J ≤ CategoryTheory.Sheaf.canonicalTopology C
• CategoryTheory.GrothendieckTopology.Subcanonical.mk 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (le_canonical : J ≤ CategoryTheory.Sheaf.canonicalTopology C) : J.Subcanonical
• CategoryTheory.GrothendieckTopology.Subcanonical.of_le 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J K : CategoryTheory.GrothendieckTopology C} (h : J ≤ K) [K.Subcanonical] : J.Subcanonical
• CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) [P.IsRepresentable] : CategoryTheory.Presieve.IsSheaf J P
• CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (h : ∀ (X : C), CategoryTheory.Presieve.IsSheaf J (CategoryTheory.yoneda.obj X)) : J.Subcanonical
• CategoryTheory.GrothendieckTopology.uliftYoneda 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : CategoryTheory.Functor C (CategoryTheory.Sheaf J (Type (max v w)))
• CategoryTheory.GrothendieckTopology.yoneda 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : CategoryTheory.Functor C (CategoryTheory.Sheaf J (Type v))
• CategoryTheory.GrothendieckTopology.fullyFaithfulUliftYoneda 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : (CategoryTheory.GrothendieckTopology.uliftYoneda.{w, v, u} J).FullyFaithful
• CategoryTheory.GrothendieckTopology.instFaithfulSheafTypeUliftYoneda 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : (CategoryTheory.GrothendieckTopology.uliftYoneda.{w, v, u} J).Faithful
• CategoryTheory.GrothendieckTopology.instFaithfulSheafTypeYoneda 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : J.yoneda.Faithful
• CategoryTheory.GrothendieckTopology.instFullSheafTypeUliftYoneda 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : (CategoryTheory.GrothendieckTopology.uliftYoneda.{w, v, u} J).Full
• CategoryTheory.GrothendieckTopology.instFullSheafTypeYoneda 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : J.yoneda.Full
• CategoryTheory.GrothendieckTopology.yonedaFullyFaithful 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : J.yoneda.FullyFaithful
• CategoryTheory.GrothendieckTopology.uliftYonedaIsoYoneda 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{max w v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : CategoryTheory.GrothendieckTopology.uliftYoneda.{w, max v w, u} J ≅ J.yoneda
• CategoryTheory.GrothendieckTopology.uliftYoneda_obj_obj_obj 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] (X : C) (X✝ : Cᵒᵖ) : ((CategoryTheory.GrothendieckTopology.uliftYoneda.{w, v, u} J).obj X).obj.obj X✝ = ULift.{w, v} (Opposite.unop X✝ ⟶ X)
• CategoryTheory.GrothendieckTopology.yoneda_obj_obj 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] (X : C) : (J.yoneda.obj X).obj = CategoryTheory.yoneda.obj X
• CategoryTheory.GrothendieckTopology.uliftYonedaCompSheafToPresheaf 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : (CategoryTheory.GrothendieckTopology.uliftYoneda.{w, v, u} J).comp (CategoryTheory.sheafToPresheaf J (Type (max v w))) ≅ CategoryTheory.uliftYoneda.{w, v, u}
• CategoryTheory.GrothendieckTopology.yonedaCompSheafToPresheaf 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : J.yoneda.comp (CategoryTheory.sheafToPresheaf J (Type v)) ≅ CategoryTheory.yoneda
• CategoryTheory.GrothendieckTopology.yoneda_map_hom 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (J.yoneda.map f).hom = CategoryTheory.yoneda.map f
• CategoryTheory.GrothendieckTopology.uliftYoneda_obj_obj_map_hom_apply_down 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] (X : C) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) (x : ULift.{w, v} (((CategoryTheory.sheafToPresheaf J (Type v)).obj (J.yoneda.obj X)).obj X✝)) : ((CategoryTheory.ConcreteCategory.hom (((CategoryTheory.GrothendieckTopology.uliftYoneda.{w, v, u} J).obj X).obj.map f)) x).down = CategoryTheory.CategoryStruct.comp f.unop x.down
• CategoryTheory.GrothendieckTopology.uliftYonedaIsoYoneda_inv_app_hom_app_hom_apply_down 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{max w v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] (X : C) (X✝ : Cᵒᵖ) (x : Opposite.unop X✝ ⟶ X) : ((CategoryTheory.ConcreteCategory.hom ((J.uliftYonedaIsoYoneda.inv.app X).hom.app X✝)) x).down = x
• CategoryTheory.GrothendieckTopology.uliftYonedaIsoYoneda_hom_app_hom_app_hom_apply 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{max w v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] (X : C) (X✝ : Cᵒᵖ) (x : ULift.{w, max v w} (Opposite.unop X✝ ⟶ X)) : (CategoryTheory.ConcreteCategory.hom ((J.uliftYonedaIsoYoneda.hom.app X).hom.app X✝)) x = x.down
• CategoryTheory.GrothendieckTopology.uliftYonedaCompSheafToPresheaf_hom_app_app_hom_apply 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] (X : C) (X✝ : Cᵒᵖ) (a : (((CategoryTheory.GrothendieckTopology.uliftYoneda.{w, v, u} J).comp (CategoryTheory.sheafToPresheaf J (Type (max v w)))).obj X).obj X✝) : (CategoryTheory.ConcreteCategory.hom ((J.uliftYonedaCompSheafToPresheaf.hom.app X).app X✝)) a = a
• CategoryTheory.GrothendieckTopology.uliftYonedaCompSheafToPresheaf_inv_app_app_hom_apply 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] (X : C) (X✝ : Cᵒᵖ) (a : (((CategoryTheory.GrothendieckTopology.uliftYoneda.{w, v, u} J).comp (CategoryTheory.sheafToPresheaf J (Type (max v w)))).obj X).obj X✝) : (CategoryTheory.ConcreteCategory.hom ((J.uliftYonedaCompSheafToPresheaf.inv.app X).app X✝)) a = a
• CategoryTheory.GrothendieckTopology.uliftYoneda_map_hom_app_hom_apply_down 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (X : Cᵒᵖ) (x : ULift.{w, v} (((CategoryTheory.sheafToPresheaf J (Type v)).obj (J.yoneda.obj X✝)).obj X)) : ((CategoryTheory.ConcreteCategory.hom (((CategoryTheory.GrothendieckTopology.uliftYoneda.{w, v, u} J).map f).hom.app X)) x).down = CategoryTheory.CategoryStruct.comp x.down f
• TopCat.subcanonical_grothendieckTopology 📋 Mathlib.Topology.Category.TopCat.GrothendieckTopology
  : TopCat.grothendieckTopology.Subcanonical
• AlgebraicGeometry.Scheme.subcanonical_zariskiTopology 📋 Mathlib.AlgebraicGeometry.Sites.BigZariski
  : AlgebraicGeometry.Scheme.zariskiTopology.Subcanonical
• AlgebraicGeometry.Scheme.instSubcanonicalFppfTopology 📋 Mathlib.AlgebraicGeometry.Sites.Fpqc
  : AlgebraicGeometry.Scheme.fppfTopology.Subcanonical
• AlgebraicGeometry.Scheme.instSubcanonicalFpqcTopology 📋 Mathlib.AlgebraicGeometry.Sites.Fpqc
  : AlgebraicGeometry.Scheme.fpqcTopology.Subcanonical
• CategoryTheory.GrothendieckTopology.subcanonical_of_full_of_faithful 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v', u_1} D] (F : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [F.Full] [F.Faithful] [F.IsContinuous J K] [K.Subcanonical] : J.Subcanonical
• CategoryTheory.GrothendieckTopology.preservesLimitsOfSize_yoneda 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : CategoryTheory.Limits.PreservesLimitsOfSize.{u_1, u_2, v, max u v, u, max u (v + 1)} J.yoneda
• CategoryTheory.GrothendieckTopology.uliftYonedaEquiv 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X : C} {F : CategoryTheory.Sheaf J (Type (max v v'))} : ((CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).obj X ⟶ F) ≃ F.obj.obj (Opposite.op X)
• CategoryTheory.GrothendieckTopology.yonedaEquiv 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X : C} {F : CategoryTheory.Sheaf J (Type v)} : (J.yoneda.obj X ⟶ F) ≃ F.obj.obj (Opposite.op X)
• CategoryTheory.GrothendieckTopology.preservesColimitsOfShape_yoneda_of_ofArrows_inj_mem 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {ι : Type u_1} [CategoryTheory.Limits.CoproductsOfShapeDisjoint C ι] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasStrictInitialObjects C] (hcov : ∀ {X : ι → C} {c : CategoryTheory.Limits.Cofan X} (x : CategoryTheory.Limits.IsColimit c), CategoryTheory.Sieve.ofArrows X c.inj ∈ J c.pt) (htriv : ∀ (Y : C) (a : CategoryTheory.Limits.IsInitial Y), ⊥ ∈ J Y) : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ι) J.yoneda
• CategoryTheory.GrothendieckTopology.hom_ext_uliftYoneda 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {P Q : CategoryTheory.Sheaf J (Type (max v v'))} {f g : P ⟶ Q} (h : ∀ (X : C) (p : (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).obj X ⟶ P), CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.comp p g) : f = g
• CategoryTheory.GrothendieckTopology.hom_ext_yoneda 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {P Q : CategoryTheory.Sheaf J (Type v)} {f g : P ⟶ Q} (h : ∀ (X : C) (p : J.yoneda.obj X ⟶ P), CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.comp p g) : f = g
• CategoryTheory.GrothendieckTopology.isColimitCofanMkYoneda 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {ι : Type u_1} (X : ι → C) {c : CategoryTheory.Limits.Cofan X} (H : CategoryTheory.Sieve.ofArrows X c.inj ∈ J c.pt) [∀ (i : ι), CategoryTheory.Mono (c.inj i)] (hempty : ∀ (Y : C) (a : CategoryTheory.Limits.IsInitial Y), ⊥ ∈ J Y) (hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), CategoryTheory.CategoryStruct.comp a (c.inj i) = CategoryTheory.CategoryStruct.comp b (c.inj j) → Nonempty (CategoryTheory.Limits.IsInitial Y)) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (J.yoneda.obj c.pt) fun i => J.yoneda.map (c.inj i))
• CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).op.comp CategoryTheory.coyoneda ≅ (CategoryTheory.evaluation Cᵒᵖ (Type (max v v'))).comp (((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Functor Cᵒᵖ (Type (max v v'))) (Type (max v v')) (Type (max (max v v') u))).obj CategoryTheory.uliftFunctor.{u, max v v'}).comp ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Sheaf J (Type (max v v'))) (CategoryTheory.Functor Cᵒᵖ (Type (max v v'))) (Type (max (max v v') u))).obj (CategoryTheory.sheafToPresheaf J (Type (max v v')))))
• CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : J.yoneda.op.comp CategoryTheory.coyoneda ≅ (CategoryTheory.evaluation Cᵒᵖ (Type v)).comp (((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Functor Cᵒᵖ (Type v)) (Type v) (Type (max v u))).obj CategoryTheory.uliftFunctor.{u, v}).comp ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Sheaf J (Type v)) (CategoryTheory.Functor Cᵒᵖ (Type v)) (Type (max v u))).obj (CategoryTheory.sheafToPresheaf J (Type v))))
• CategoryTheory.GrothendieckTopology.yonedaEquiv_yoneda_map 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X Y : C} (f : X ⟶ Y) : J.yonedaEquiv (J.yoneda.map f) = f
• CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_uliftYoneda_map 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X Y : C} (f : X ⟶ Y) : J.uliftYonedaEquiv ((CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).map f) = { down := f }
• CategoryTheory.GrothendieckTopology.yonedaEquiv_apply 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X : C} {F : CategoryTheory.Sheaf J (Type v)} (f : J.yoneda.obj X ⟶ F) : J.yonedaEquiv f = (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op X))) (CategoryTheory.CategoryStruct.id X)
• CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_app_apply 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X : C} {F : CategoryTheory.Sheaf J (Type v)} (x : F.obj.obj (Opposite.op X)) (Y : Cᵒᵖ) (f : Opposite.unop Y ⟶ X) : (CategoryTheory.ConcreteCategory.hom ((J.yonedaEquiv.symm x).hom.app Y)) f = (CategoryTheory.ConcreteCategory.hom (F.obj.map f.op)) x
• CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_apply 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X : C} {F : CategoryTheory.Sheaf J (Type (max v v'))} (f : (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).obj X ⟶ F) : J.uliftYonedaEquiv f = (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op X))) { down := CategoryTheory.CategoryStruct.id X }
• CategoryTheory.GrothendieckTopology.map_yonedaEquiv 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X Y : C} {F : CategoryTheory.Sheaf J (Type v)} (f : J.yoneda.obj X ⟶ F) (g : Y ⟶ X) : (CategoryTheory.ConcreteCategory.hom (F.obj.map g.op)) (J.yonedaEquiv f) = (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op Y))) g
• CategoryTheory.GrothendieckTopology.map_yonedaEquiv' 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X Y : Cᵒᵖ} {F : CategoryTheory.Sheaf J (Type v)} (f : J.yoneda.obj (Opposite.unop X) ⟶ F) (g : X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom (F.obj.map g)) (J.yonedaEquiv f) = (CategoryTheory.ConcreteCategory.hom (f.hom.app Y)) g.unop
• CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_app_apply 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X : C} {F : CategoryTheory.Sheaf J (Type (max v v'))} (x : F.obj.obj (Opposite.op X)) (Y : Cᵒᵖ) (f : Opposite.unop Y ⟶ X) : (CategoryTheory.ConcreteCategory.hom ((J.uliftYonedaEquiv.symm x).hom.app Y)) { down := f } = (CategoryTheory.ConcreteCategory.hom (F.obj.map f.op)) x
• CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X Y : C} {F : CategoryTheory.Sheaf J (Type (max v v'))} (f : (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).obj X ⟶ F) (g : Y ⟶ X) : (CategoryTheory.ConcreteCategory.hom (F.obj.map g.op)) (J.uliftYonedaEquiv f) = (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op Y))) { down := g }
• CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv' 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X Y : Cᵒᵖ} {F : CategoryTheory.Sheaf J (Type (max v v'))} (f : (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).obj (Opposite.unop X) ⟶ F) (g : X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom (F.obj.map g)) (J.uliftYonedaEquiv f) = (CategoryTheory.ConcreteCategory.hom (f.hom.app Y)) { down := g.unop }
• CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_naturality 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X Y : C} {F : CategoryTheory.Sheaf J (Type (max v v'))} (f : (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).obj X ⟶ F) (g : Y ⟶ X) : (CategoryTheory.ConcreteCategory.hom (F.obj.map g.op)) (J.uliftYonedaEquiv f) = J.uliftYonedaEquiv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).map g) f)
• CategoryTheory.GrothendieckTopology.yonedaEquiv_naturality 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X Y : C} {F : CategoryTheory.Sheaf J (Type v)} (f : J.yoneda.obj X ⟶ F) (g : Y ⟶ X) : (CategoryTheory.ConcreteCategory.hom (F.obj.map g.op)) (J.yonedaEquiv f) = J.yonedaEquiv (CategoryTheory.CategoryStruct.comp (J.yoneda.map g) f)
• CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_naturality' 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X Y : Cᵒᵖ} {F : CategoryTheory.Sheaf J (Type (max v v'))} (f : (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).obj (Opposite.unop X) ⟶ F) (g : X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom (F.obj.map g)) (J.uliftYonedaEquiv f) = J.uliftYonedaEquiv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).map g.unop) f)
• CategoryTheory.GrothendieckTopology.yonedaEquiv_naturality' 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X Y : Cᵒᵖ} {F : CategoryTheory.Sheaf J (Type v)} (f : J.yoneda.obj (Opposite.unop X) ⟶ F) (g : X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom (F.obj.map g)) (J.yonedaEquiv f) = J.yonedaEquiv (CategoryTheory.CategoryStruct.comp (J.yoneda.map g.unop) f)
• CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_comp 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X : C} {F G : CategoryTheory.Sheaf J (Type (max v v'))} (α : (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).obj X ⟶ F) (β : F ⟶ G) : J.uliftYonedaEquiv (CategoryTheory.CategoryStruct.comp α β) = (CategoryTheory.ConcreteCategory.hom (β.hom.app (Opposite.op X))) (J.uliftYonedaEquiv α)
• CategoryTheory.GrothendieckTopology.yonedaEquiv_comp 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X : C} {F G : CategoryTheory.Sheaf J (Type v)} (α : J.yoneda.obj X ⟶ F) (β : F ⟶ G) : J.yonedaEquiv (CategoryTheory.CategoryStruct.comp α β) = (CategoryTheory.ConcreteCategory.hom (β.hom.app (Opposite.op X))) (J.yonedaEquiv α)
• CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_naturality_left 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X X' : C} (f : X' ⟶ X) (F : CategoryTheory.Sheaf J (Type (max v v'))) (x : F.obj.obj (Opposite.op X)) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).map f) (J.uliftYonedaEquiv.symm x) = J.uliftYonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.obj.map f.op)) x)
• CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_naturality_left 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X X' : C} (f : X' ⟶ X) (F : CategoryTheory.Sheaf J (Type v)) (x : F.obj.obj (Opposite.op X)) : CategoryTheory.CategoryStruct.comp (J.yoneda.map f) (J.yonedaEquiv.symm x) = J.yonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.obj.map f.op)) x)
• CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_naturality_right 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] (X : C) {F F' : CategoryTheory.Sheaf J (Type (max v v'))} (f : F ⟶ F') (x : F.obj.obj (Opposite.op X)) : CategoryTheory.CategoryStruct.comp (J.uliftYonedaEquiv.symm x) f = J.uliftYonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op X))) x)
• CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_naturality_right 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] (X : C) {F F' : CategoryTheory.Sheaf J (Type v)} (f : F ⟶ F') (x : F.obj.obj (Opposite.op X)) : CategoryTheory.CategoryStruct.comp (J.yonedaEquiv.symm x) f = J.yonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op X))) x)
• CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_map 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X Y : Cᵒᵖ} (f : X ⟶ Y) {F : CategoryTheory.Sheaf J (Type (max v v'))} (t : F.obj.obj X) : J.uliftYonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.obj.map f)) t) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).map f.unop) (J.uliftYonedaEquiv.symm t)
• CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_map 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X Y : Cᵒᵖ} (f : X ⟶ Y) {F : CategoryTheory.Sheaf J (Type v)} (t : F.obj.obj X) : J.yonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.obj.map f)) t) = CategoryTheory.CategoryStruct.comp (J.yoneda.map f.unop) (J.yonedaEquiv.symm t)
• CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_app_app 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] (X : Cᵒᵖ) (F : CategoryTheory.Sheaf J (Type (max v v'))) : (J.uliftYonedaOpCompCoyoneda.app X).app F = (J.uliftYonedaEquiv.trans Equiv.ulift.symm).toIso
• CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] (X : Cᵒᵖ) (F : CategoryTheory.Sheaf J (Type (max v v'))) (s : ULift.{u, max v v'} (F.obj.obj X)) : (CategoryTheory.ConcreteCategory.hom ((J.uliftYonedaOpCompCoyoneda.inv.app X).app F)) s = J.uliftYonedaEquiv.symm s.down
• CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda_inv_app_app 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] (X : Cᵒᵖ) (X✝ : CategoryTheory.Sheaf J (Type v)) : (J.yonedaOpCompCoyoneda.inv.app X).app X✝ = CategoryTheory.CategoryStruct.comp ((CategoryTheory.largeCurriedYonedaLemma.inv.app X).app X✝.obj) (CategoryTheory.CategoryStruct.comp (TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp (J.yonedaCompSheafToPresheaf.hom.app (Opposite.unop X)) g) ((CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf.hom.app (Opposite.op (J.yoneda.obj (Opposite.unop X)))).app X✝))
• CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app_hom_apply_hom_app_hom_apply 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] (X : Cᵒᵖ) (X✝ : CategoryTheory.Sheaf J (Type (max v' v))) (a✝ : (((CategoryTheory.evaluation Cᵒᵖ (Type (max v v'))).comp (((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Functor Cᵒᵖ (Type (max v v'))) (Type (max v v')) (Type (max (max v v') u))).obj CategoryTheory.uliftFunctor.{u, max v v'}).comp ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Sheaf J (Type (max v v'))) (CategoryTheory.Functor Cᵒᵖ (Type (max v v'))) (Type (max (max v v') u))).obj (CategoryTheory.sheafToPresheaf J (Type (max v v')))))).obj X).obj X✝) (X✝¹ : Cᵒᵖ) (a✝¹ : (Opposite.unop (((CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).comp (CategoryTheory.sheafToPresheaf J (Type (max v v')))).op.obj X)).obj X✝¹) : (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.ConcreteCategory.hom ((J.uliftYonedaOpCompCoyoneda.inv.app X).app X✝)) a✝).hom.app X✝¹)) a✝¹ = ((((CategoryTheory.uliftYonedaOpCompCoyoneda.inv.app X).app X✝.obj).hom' a✝).app X✝¹).hom' (((J.uliftYonedaCompSheafToPresheaf.hom.app (Opposite.unop X)).app X✝¹).hom' a✝¹)
• CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda_hom_app_app_hom_apply_down 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] (X : Cᵒᵖ) (X✝ : CategoryTheory.Sheaf J (Type v)) (a✝ : ((J.yoneda.op.comp CategoryTheory.coyoneda).obj X).obj X✝) : ((CategoryTheory.ConcreteCategory.hom ((J.yonedaOpCompCoyoneda.hom.app X).app X✝)) a✝).down = CategoryTheory.yonedaEquiv ((CategoryTheory.CategoryStruct.comp ((CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf.inv.app (Opposite.op (J.yoneda.obj (Opposite.unop X)))).app X✝) (TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp (J.yonedaCompSheafToPresheaf.inv.app (Opposite.unop X)) g)).hom' a✝)
• CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_hom_app_app_hom_apply_down 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] (X : Cᵒᵖ) (X✝ : CategoryTheory.Sheaf J (Type (max v' v))) (a✝ : (((J.yoneda.op.comp (CategoryTheory.sheafCompose J CategoryTheory.uliftFunctor.{v', v}).op).comp CategoryTheory.coyoneda).obj X).obj X✝) : ((CategoryTheory.ConcreteCategory.hom ((J.uliftYonedaOpCompCoyoneda.hom.app X).app X✝)) a✝).down = CategoryTheory.uliftYonedaEquiv ((CategoryTheory.CategoryStruct.comp ((CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf.inv.app (Opposite.op ((CategoryTheory.sheafCompose J CategoryTheory.uliftFunctor.{v', v}).obj (J.yoneda.obj (Opposite.unop X))))).app X✝) (TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp (J.uliftYonedaCompSheafToPresheaf.inv.app (Opposite.unop X)) g)).hom' a✝)
• CategoryTheory.GrothendieckTopology.subcanonical_over 📋 Mathlib.CategoryTheory.Sites.SubcanonicalOver
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] (X : C) : (J.over X).Subcanonical
• AlgebraicGeometry.Scheme.instSubcanonicalProetaleTopology 📋 Mathlib.AlgebraicGeometry.Sites.Proetale
  : AlgebraicGeometry.Scheme.proetaleTopology.Subcanonical
• AlgebraicGeometry.Scheme.ProEt.instSubcanonicalTopology 📋 Mathlib.AlgebraicGeometry.Sites.Proetale
  (S : AlgebraicGeometry.Scheme) : (AlgebraicGeometry.Scheme.ProEt.topology S).Subcanonical
• CategoryTheory.coherentTopology.subcanonical 📋 Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Precoherent C] : (CategoryTheory.coherentTopology C).Subcanonical
• CategoryTheory.extensiveTopology.subcanonical 📋 Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.FinitaryPreExtensive C] : (CategoryTheory.extensiveTopology C).Subcanonical
• CategoryTheory.regularTopology.subcanonical 📋 Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preregular C] : (CategoryTheory.regularTopology C).Subcanonical
• CategoryTheory.Precoverage.ZeroHypercover.instIsLocalAtTargetIsomorphisms 📋 Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.toGrothendieck.Subcanonical] [CategoryTheory.Limits.HasPullbacks C] [J.IsStableUnderBaseChange] : (CategoryTheory.MorphismProperty.isomorphisms C).IsLocalAtTarget J
• CategoryTheory.Precoverage.ZeroHypercover.hom_ext 📋 Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.toGrothendieck.Subcanonical] {X Y : C} (𝒰 : J.ZeroHypercover X) {f g : X ⟶ Y} (h : ∀ (i : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (𝒰.f i) f = CategoryTheory.CategoryStruct.comp (𝒰.f i) g) : f = g
• CategoryTheory.GrothendieckTopology.OneHypercover.glueMorphisms 📋 Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] {S T : C} (E : J.OneHypercover S) (f : (i : E.I₀) → E.X i ⟶ T) (h : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryTheory.CategoryStruct.comp (E.p₁ k) (f i) = CategoryTheory.CategoryStruct.comp (E.p₂ k) (f j)) : S ⟶ T
• CategoryTheory.GrothendieckTopology.OneHypercover.f_glueMorphisms 📋 Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] {S T : C} (E : J.OneHypercover S) (f : (i : E.I₀) → E.X i ⟶ T) (h : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryTheory.CategoryStruct.comp (E.p₁ k) (f i) = CategoryTheory.CategoryStruct.comp (E.p₂ k) (f j)) (i : E.I₀) : CategoryTheory.CategoryStruct.comp (E.f i) (E.glueMorphisms f h) = f i
• CategoryTheory.GrothendieckTopology.OneHypercover.f_glueMorphisms_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] {S T : C} (E : J.OneHypercover S) (f : (i : E.I₀) → E.X i ⟶ T) (h : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryTheory.CategoryStruct.comp (E.p₁ k) (f i) = CategoryTheory.CategoryStruct.comp (E.p₂ k) (f j)) (i : E.I₀) {Z : C} (h✝ : T ⟶ Z) : CategoryTheory.CategoryStruct.comp (E.f i) (CategoryTheory.CategoryStruct.comp (E.glueMorphisms f h) h✝) = CategoryTheory.CategoryStruct.comp (f i) h✝
• CategoryTheory.Precoverage.ZeroHypercover.isPullback_of_forall_isPullback 📋 Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.toGrothendieck.Subcanonical] [CategoryTheory.Limits.HasPullbacks C] [J.IsStableUnderBaseChange] {P X Y Z : C} (fst : P ⟶ X) (snd : P ⟶ Y) (f : X ⟶ Z) (g : Y ⟶ Z) (𝒰 : J.ZeroHypercover X) (H : ∀ (i : 𝒰.I₀), CategoryTheory.IsPullback (CategoryTheory.Limits.pullback.snd fst (𝒰.f i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst fst (𝒰.f i)) snd) (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) : CategoryTheory.IsPullback fst snd f g
• CategoryTheory.Precoverage.ZeroHypercover.glueMorphisms 📋 Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.toGrothendieck.Subcanonical] {S T : C} (𝒰 : J.ZeroHypercover S) [𝒰.HasPullbacks] (f : (i : 𝒰.I₀) → 𝒰.X i ⟶ T) (hf : ∀ (i j : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f i) (𝒰.f j)) (f i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f i) (𝒰.f j)) (f j)) : S ⟶ T
• CategoryTheory.Precoverage.ZeroHypercover.f_glueMorphisms 📋 Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.toGrothendieck.Subcanonical] {S T : C} (𝒰 : J.ZeroHypercover S) [𝒰.HasPullbacks] (f : (i : 𝒰.I₀) → 𝒰.X i ⟶ T) (hf : ∀ (i j : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f i) (𝒰.f j)) (f i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f i) (𝒰.f j)) (f j)) (i : 𝒰.I₀) : CategoryTheory.CategoryStruct.comp (𝒰.f i) (𝒰.glueMorphisms f hf) = f i
• CategoryTheory.Precoverage.ZeroHypercover.f_glueMorphisms_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.toGrothendieck.Subcanonical] {S T : C} (𝒰 : J.ZeroHypercover S) [𝒰.HasPullbacks] (f : (i : 𝒰.I₀) → 𝒰.X i ⟶ T) (hf : ∀ (i j : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f i) (𝒰.f j)) (f i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f i) (𝒰.f j)) (f j)) (i : 𝒰.I₀) {Z : C} (h : T ⟶ Z) : CategoryTheory.CategoryStruct.comp (𝒰.f i) (CategoryTheory.CategoryStruct.comp (𝒰.glueMorphisms f hf) h) = CategoryTheory.CategoryStruct.comp (f i) h
• instPreservesLimitsOfShapeSheafTypeUliftYoneda 📋 Mathlib.CategoryTheory.Sites.PreservesLimits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] {K : Type u_1} [CategoryTheory.Category.{v_1, u_1} K] : CategoryTheory.Limits.PreservesLimitsOfShape K (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J)
• instPreservesLimitsOfShapeSheafTypeYoneda 📋 Mathlib.CategoryTheory.Sites.PreservesLimits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] {K : Type u_1} [CategoryTheory.Category.{v_1, u_1} K] : CategoryTheory.Limits.PreservesLimitsOfShape K J.yoneda
• instPreservesFiniteCoproductsSheafTypeUliftYonedaOfPreservesFiniteProductsOppositeObjFunctorIsSheaf 📋 Mathlib.CategoryTheory.Sites.PreservesLimits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] [∀ (X : CategoryTheory.Sheaf J (Type (max v v'))), CategoryTheory.Limits.PreservesFiniteProducts X.obj] : CategoryTheory.Limits.PreservesFiniteCoproducts (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J)
• instPreservesFiniteCoproductsSheafTypeYonedaOfPreservesFiniteProductsOppositeObjFunctorIsSheaf 📋 Mathlib.CategoryTheory.Sites.PreservesLimits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] [∀ (X : CategoryTheory.Sheaf J (Type v)), CategoryTheory.Limits.PreservesFiniteProducts X.obj] : CategoryTheory.Limits.PreservesFiniteCoproducts J.yoneda
• instPreservesColimitsOfShapeSheafTypeUliftYonedaOfPreservesLimitsOfShapeOppositeObjFunctorIsSheaf 📋 Mathlib.CategoryTheory.Sites.PreservesLimits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] {K : Type u_1} [CategoryTheory.Category.{v_1, u_1} K] [∀ (X : CategoryTheory.Sheaf J (Type (max v v'))), CategoryTheory.Limits.PreservesLimitsOfShape Kᵒᵖ X.obj] : CategoryTheory.Limits.PreservesColimitsOfShape K (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J)
• instPreservesColimitsOfShapeSheafTypeYonedaOfPreservesLimitsOfShapeOppositeObjFunctorIsSheaf 📋 Mathlib.CategoryTheory.Sites.PreservesLimits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] {K : Type u_1} [CategoryTheory.Category.{v_1, u_1} K] [∀ (X : CategoryTheory.Sheaf J (Type v)), CategoryTheory.Limits.PreservesLimitsOfShape Kᵒᵖ X.obj] : CategoryTheory.Limits.PreservesColimitsOfShape K J.yoneda
• instPreservesColimitSheafTypeUliftYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf 📋 Mathlib.CategoryTheory.Sites.PreservesLimits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] {K : Type u_1} [CategoryTheory.Category.{v_1, u_1} K] {F : CategoryTheory.Functor K C} [∀ (X : CategoryTheory.Sheaf J (Type (max v v'))), CategoryTheory.Limits.PreservesLimit F.op X.obj] : CategoryTheory.Limits.PreservesColimit F (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J)
• instPreservesColimitSheafTypeYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf 📋 Mathlib.CategoryTheory.Sites.PreservesLimits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] {K : Type u_1} [CategoryTheory.Category.{v_1, u_1} K] {F : CategoryTheory.Functor K C} [∀ (X : CategoryTheory.Sheaf J (Type v)), CategoryTheory.Limits.PreservesLimit F.op X.obj] : CategoryTheory.Limits.PreservesColimit F J.yoneda
• instPreservesColimitSheafTypeYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf_1 📋 Mathlib.CategoryTheory.Sites.PreservesLimits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] {K : Type u_1} [CategoryTheory.Category.{v_1, u_1} K] {F : CategoryTheory.Functor K C} [∀ (X : CategoryTheory.Sheaf J (Type v)), CategoryTheory.Limits.PreservesLimit F.op X.obj] : CategoryTheory.Limits.PreservesColimit F J.yoneda
• CategoryTheory.subcanonical_typesGrothendieckTopology 📋 Mathlib.CategoryTheory.Sites.Types
  : CategoryTheory.typesGrothendieckTopology.Subcanonical

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