Loogle!

Result

Found 81 declarations mentioning CategoryTheory.Functor.IsCocontinuous.

• CategoryTheory.isCocontinuous_id 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) : (CategoryTheory.Functor.id C).IsCocontinuous J J
• CategoryTheory.Functor.IsCocontinuous 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) : Prop
• CategoryTheory.instIsContinuousRightAdjointOfIsCocontinuous 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) {F : CategoryTheory.Functor C D} [F.IsCocontinuous J K] [F.IsLeftAdjoint] : F.rightAdjoint.IsContinuous K J
• CategoryTheory.Adjunction.isContinuous_of_isCocontinuous 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.IsCocontinuous J K] : G.IsContinuous K J
• CategoryTheory.Adjunction.isCocontinuous_iff_coverPreserving 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) : F.IsCocontinuous J K ↔ CategoryTheory.CoverPreserving K J G
• CategoryTheory.Functor.IsCocontinuous.of_iso 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {F G : CategoryTheory.Functor C D} (e : F ≅ G) [F.IsCocontinuous J K] : G.IsCocontinuous J K
• CategoryTheory.Functor.IsCocontinuous.iff_of_iso 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {F G : CategoryTheory.Functor C D} (e : F ≅ G) : F.IsCocontinuous J K ↔ G.IsCocontinuous J K
• CategoryTheory.isCocontinuous_comp 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [CategoryTheory.Category.{v_3, u_3} E] (G : CategoryTheory.Functor C D) (G' : CategoryTheory.Functor D E) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) {L : CategoryTheory.GrothendieckTopology E} [G.IsCocontinuous J K] [G'.IsCocontinuous K L] : (G.comp G').IsCocontinuous J L
• CategoryTheory.CoverPreserving.of_comp_of_isCocontinuous 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [CategoryTheory.Category.{v_3, u_3} E] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) {L : CategoryTheory.GrothendieckTopology E} {F : CategoryTheory.Functor C D} (G : CategoryTheory.Functor D E) (h : CategoryTheory.CoverPreserving J L (F.comp G)) [G.IsCocontinuous K L] [G.Full] [G.Faithful] : CategoryTheory.CoverPreserving J K F
• CategoryTheory.Functor.sheafPushforwardCocontinuous 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] : CategoryTheory.Functor (CategoryTheory.Sheaf J A) (CategoryTheory.Sheaf K A)
• CategoryTheory.Functor.cover_lift 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] {U : C} {S : CategoryTheory.Sieve (G.obj U)} (hS : S ∈ K (G.obj U)) : CategoryTheory.Sieve.functorPullback G S ∈ J U
• CategoryTheory.Functor.IsCocontinuous.cover_lift 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {D : Type u_2} {inst✝¹ : CategoryTheory.Category.{v_2, u_2} D} {G : CategoryTheory.Functor C D} {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [self : G.IsCocontinuous J K] {U : C} {S : CategoryTheory.Sieve (G.obj U)} : S ∈ K (G.obj U) → CategoryTheory.Sieve.functorPullback G S ∈ J U
• CategoryTheory.Functor.IsCocontinuous.mk 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} (cover_lift : ∀ {U : C} {S : CategoryTheory.Sieve (G.obj U)}, S ∈ K (G.obj U) → CategoryTheory.Sieve.functorPullback G S ∈ J U) : G.IsCocontinuous J K
• CategoryTheory.Functor.sheafAdjunctionCocontinuous 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsContinuous J K] : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K
• CategoryTheory.ran_isSheaf_of_isCocontinuous 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] (ℱ : CategoryTheory.Sheaf J A) : CategoryTheory.Presheaf.IsSheaf K (G.op.ran.obj ℱ.obj)
• CategoryTheory.RanIsSheafOfIsCocontinuous.isLimitMultifork 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F} (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} (S : K.Cover X) : CategoryTheory.Limits.IsLimit (S.multifork R)
• CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} (α : G.op.comp R ⟶ F) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) {Y : C} (f : G.obj Y ⟶ X) : s.pt ⟶ F.obj (Opposite.op Y)
• CategoryTheory.RanIsSheafOfIsCocontinuous.lift 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F} (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) : s.pt ⟶ R.obj (Opposite.op X)
• CategoryTheory.Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] : (G.sheafPushforwardCocontinuous A J K).comp (CategoryTheory.sheafToPresheaf K A) ≅ (CategoryTheory.sheafToPresheaf J A).comp G.op.ran
• CategoryTheory.RanIsSheafOfIsCocontinuous.fac 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F} (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) (i : S.Arrow) : CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.lift hF hR s) (R.map i.f.op) = s.ι i
• CategoryTheory.RanIsSheafOfIsCocontinuous.hom_ext 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F} (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} {S : K.Cover X} {W : A} {f g : W ⟶ R.obj (Opposite.op X)} (h : ∀ (i : S.Arrow), CategoryTheory.CategoryStruct.comp f (R.map i.f.op) = CategoryTheory.CategoryStruct.comp g (R.map i.f.op)) : f = g
• CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsContinuous J K] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify K A] : ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).comp (CategoryTheory.presheafToSheaf J A) ≅ (CategoryTheory.presheafToSheaf K A).comp (G.sheafPushforwardContinuous A J K)
• CategoryTheory.RanIsSheafOfIsCocontinuous.fac_assoc 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F} (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) (i : S.Arrow) {Z : A} (h : R.obj (Opposite.op i.Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.lift hF hR s) (CategoryTheory.CategoryStruct.comp (R.map i.f.op) h) = CategoryTheory.CategoryStruct.comp (s.ι i) h
• CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux_map' 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} (α : G.op.comp R ⟶ F) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) {Y Y' : C} (f : G.obj Y ⟶ X) (f' : G.obj Y' ⟶ X) {W : C} (a : W ⟶ Y) (b : W ⟶ Y') (w : CategoryTheory.CategoryStruct.comp (G.map a) f = CategoryTheory.CategoryStruct.comp (G.map b) f') : CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s f) (F.map a.op) = CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s f') (F.map b.op)
• CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux_map 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} (α : G.op.comp R ⟶ F) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) {Y : C} (f : G.obj Y ⟶ X) {W : C} (g : W ⟶ Y) (i : S.Arrow) (h : G.obj W ⟶ i.Y) (w : CategoryTheory.CategoryStruct.comp h i.f = CategoryTheory.CategoryStruct.comp (G.map g) f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s f) (F.map g.op) = CategoryTheory.CategoryStruct.comp (s.ι i) (CategoryTheory.CategoryStruct.comp (R.map h.op) (α.app (Opposite.op W)))
• CategoryTheory.RanIsSheafOfIsCocontinuous.fac' 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F} (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) (j : CategoryTheory.StructuredArrow (Opposite.op X) G.op) : CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.lift hF hR s) (CategoryTheory.CategoryStruct.comp (R.map j.hom) (α.app j.right)) = CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s j.hom.unop
• CategoryTheory.Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso_hom 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] : (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).hom = CategoryTheory.CategoryStruct.id ((G.sheafPushforwardCocontinuous A J K).comp (CategoryTheory.sheafToPresheaf K A))
• CategoryTheory.Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso_inv 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] : (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).inv = CategoryTheory.CategoryStruct.id ((G.sheafPushforwardCocontinuous A J K).comp (CategoryTheory.sheafToPresheaf K A))
• CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_hom 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsContinuous J K] (F : CategoryTheory.Sheaf J A) : ((G.sheafAdjunctionCocontinuous A J K).counit.app F).hom = (G.op.ranAdjunction A).counit.app F.obj
• CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_val 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsContinuous J K] (F : CategoryTheory.Sheaf J A) : ((G.sheafAdjunctionCocontinuous A J K).counit.app F).hom = (G.op.ranAdjunction A).counit.app F.obj
• CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_hom 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsContinuous J K] (F : CategoryTheory.Sheaf K A) : ((G.sheafAdjunctionCocontinuous A J K).unit.app F).hom = (G.op.ranAdjunction A).unit.app F.obj
• CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_val 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsContinuous J K] (F : CategoryTheory.Sheaf K A) : ((G.sheafAdjunctionCocontinuous A J K).unit.app F).hom = (G.op.ranAdjunction A).unit.app F.obj
• CategoryTheory.Functor.toSheafify_pullbackSheafificationCompatibility 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsContinuous J K] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify K A] (F : CategoryTheory.Functor Dᵒᵖ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J (G.op.comp F)) ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).hom = G.op.whiskerLeft (CategoryTheory.toSheafify K F)
• CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility_hom_app_hom 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsContinuous J K] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify K A] (F : CategoryTheory.Functor Dᵒᵖ A) : ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).hom = CategoryTheory.sheafifyLift J (G.op.whiskerLeft (CategoryTheory.toSheafify K F)) ⋯
• CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility_hom_app_val 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsContinuous J K] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify K A] (F : CategoryTheory.Functor Dᵒᵖ A) : ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).hom = CategoryTheory.sheafifyLift J (G.op.whiskerLeft (CategoryTheory.toSheafify K F)) ⋯
• CategoryTheory.Functor.sheafAdjunctionCocontinuous_homEquiv_apply_hom 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsContinuous J K] {F : CategoryTheory.Sheaf K A} {H : CategoryTheory.Sheaf J A} (f : (G.sheafPushforwardContinuous A J K).obj F ⟶ H) : (((G.sheafAdjunctionCocontinuous A J K).homEquiv F H) f).hom = ((G.op.ranAdjunction A).homEquiv F.obj H.obj) f.hom
• CategoryTheory.Functor.sheafAdjunctionCocontinuous_homEquiv_apply_val 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsContinuous J K] {F : CategoryTheory.Sheaf K A} {H : CategoryTheory.Sheaf J A} (f : (G.sheafPushforwardContinuous A J K).obj F ⟶ H) : (((G.sheafAdjunctionCocontinuous A J K).homEquiv F H) f).hom = ((G.op.ranAdjunction A).homEquiv F.obj H.obj) f.hom
• CategoryTheory.Functor.IsDenseSubsite.instIsCocontinuous 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) [CategoryTheory.Functor.IsDenseSubsite J K G] : G.IsCocontinuous J K
• CategoryTheory.Functor.instIsCocontinuousRestrictedTopology 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [G.LocallyCoverDense K] : G.IsCocontinuous (G.restrictedTopology K) K
• CategoryTheory.Presheaf.isLocallyInjective_whisker 📋 Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
  {C : Type u_1} {D : Type u_2} {A : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_3, u_3} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (H : CategoryTheory.Functor C D) {F G : CategoryTheory.Functor Dᵒᵖ A} (f : F ⟶ G) {FA : A → A → Type u_4} {CA : A → Type u_5} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [H.IsCocontinuous J K] [CategoryTheory.Presheaf.IsLocallyInjective K f] : CategoryTheory.Presheaf.IsLocallyInjective J (H.op.whiskerLeft f)
• CategoryTheory.Presheaf.isLocallySurjective_whisker 📋 Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
  {C : Type u_1} {D : Type u_2} {A : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_3, u_3} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (H : CategoryTheory.Functor C D) {F G : CategoryTheory.Functor Dᵒᵖ A} (f : F ⟶ G) {FA : A → A → Type u_4} {CA : A → Type u_5} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [H.IsCocontinuous J K] [CategoryTheory.Presheaf.IsLocallySurjective K f] : CategoryTheory.Presheaf.IsLocallySurjective J (H.op.whiskerLeft f)
• CategoryTheory.Presheaf.isLocallyInjective_whisker_iff 📋 Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
  {C : Type u_1} {D : Type u_2} {A : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_3, u_3} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (H : CategoryTheory.Functor C D) {F G : CategoryTheory.Functor Dᵒᵖ A} (f : F ⟶ G) {FA : A → A → Type u_4} {CA : A → Type u_5} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] (hH : CategoryTheory.CoverPreserving J K H) [H.IsCocontinuous J K] [H.IsCoverDense K] : CategoryTheory.Presheaf.IsLocallyInjective J (H.op.whiskerLeft f) ↔ CategoryTheory.Presheaf.IsLocallyInjective K f
• CategoryTheory.Presheaf.isLocallySurjective_whisker_iff 📋 Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
  {C : Type u_1} {D : Type u_2} {A : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_3, u_3} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (H : CategoryTheory.Functor C D) {F G : CategoryTheory.Functor Dᵒᵖ A} (f : F ⟶ G) {FA : A → A → Type u_4} {CA : A → Type u_5} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] (hH : CategoryTheory.CoverPreserving J K H) [H.IsCocontinuous J K] [H.IsCoverDense K] : CategoryTheory.Presheaf.IsLocallySurjective J (H.op.whiskerLeft f) ↔ CategoryTheory.Presheaf.IsLocallySurjective K f
• CategoryTheory.Equivalence.isDenseSubsite_functor_of_isCocontinuous 📋 Mathlib.CategoryTheory.Sites.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) [e.functor.IsCocontinuous J K] [e.inverse.IsCocontinuous K J] : CategoryTheory.Functor.IsDenseSubsite J K e.functor
• CategoryTheory.Equivalence.isDenseSubsite_inverse_of_isCocontinuous 📋 Mathlib.CategoryTheory.Sites.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) [e.functor.IsCocontinuous J K] [e.inverse.IsCocontinuous K J] : CategoryTheory.Functor.IsDenseSubsite K J e.inverse
• CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.transport 📋 Mathlib.CategoryTheory.Sites.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor D C) {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] [G.IsCoverDense J] [G.Full] [G.IsContinuous K J] [(G.sheafPushforwardContinuous A K J).EssSurj] [G.IsCocontinuous K J] {FA : A → A → Type u_1} {CA : A → Type u_2} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [K.WEqualsLocallyBijective A] (hG : CategoryTheory.CoverPreserving K J G) : J.WEqualsLocallyBijective A
• CategoryTheory.GrothendieckTopology.instIsCocontinuousOverForgetOver 📋 Mathlib.CategoryTheory.Sites.Over
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (X : C) : (CategoryTheory.Over.forget X).IsCocontinuous (J.over X) J
• CategoryTheory.GrothendieckTopology.instIsCocontinuousOverMapOver 📋 Mathlib.CategoryTheory.Sites.Over
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {X Y : C} (f : X ⟶ Y) : (CategoryTheory.Over.map f).IsCocontinuous (J.over X) (J.over Y)
• CategoryTheory.instIsCocontinuousOverLeftIteratedSliceBackwardOver 📋 Mathlib.CategoryTheory.Sites.Over
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} (f : CategoryTheory.Over X) : f.iteratedSliceBackward.IsCocontinuous (J.over f.left) ((J.over X).over f)
• CategoryTheory.instIsCocontinuousOverLeftIteratedSliceForwardOver 📋 Mathlib.CategoryTheory.Sites.Over
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} (f : CategoryTheory.Over X) : f.iteratedSliceForward.IsCocontinuous ((J.over X).over f) (J.over f.left)
• CategoryTheory.GrothendieckTopology.instIsCocontinuousOverObjPostOver 📋 Mathlib.CategoryTheory.Sites.Over
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (K : CategoryTheory.GrothendieckTopology D) (F : CategoryTheory.Functor C D) (X : C) [F.IsCocontinuous J K] : (CategoryTheory.Over.post F).IsCocontinuous (J.over X) (K.over (F.obj X))
• SheafOfModules.isLeftAdjoint_pushforward_of_isIso 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) [F.IsCocontinuous J K] [CategoryTheory.IsIso φ] [F.IsLeftAdjoint] : (SheafOfModules.pushforward φ).IsLeftAdjoint
• SheafOfModules.isQuasicoherent_pushforward_of_isLeftAdjoint 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} {S : CategoryTheory.Sheaf K RingCat} [∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : D), CategoryTheory.HasSheafify (K.over X) AddCommGrpCat] (G : CategoryTheory.Functor D C) [G.IsContinuous K J] [G.IsCocontinuous K J] (φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R) (η : (SheafOfModules.pushforward φ).obj (SheafOfModules.unit R) ≅ SheafOfModules.unit S) [G.IsLeftAdjoint] [CategoryTheory.IsIso φ] [∀ (X : D), (CategoryTheory.Over.post G).IsContinuous (K.over X) (J.over (G.obj X))] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasPullbacks D] {M : SheafOfModules R} [M.IsQuasicoherent] : ((SheafOfModules.pushforward φ).obj M).IsQuasicoherent
• SheafOfModules.isQuasicoherent_pushforward 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} {S : CategoryTheory.Sheaf K RingCat} [∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : D), CategoryTheory.HasSheafify (K.over X) AddCommGrpCat] (G : CategoryTheory.Functor D C) [G.IsContinuous K J] [G.IsCocontinuous K J] (φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R) (η : (SheafOfModules.pushforward φ).obj (SheafOfModules.unit R) ≅ SheafOfModules.unit S) [∀ (X : D), (CategoryTheory.Over.post G).IsContinuous (K.over X) (J.over (G.obj X))] (h : ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y), CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} (SheafOfModules.pushforward (((CategoryTheory.Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))) {M : SheafOfModules R} [M.IsQuasicoherent] : ((SheafOfModules.pushforward φ).obj M).IsQuasicoherent
• SheafOfModules.QuasicoherentData.pushforward 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} {S : CategoryTheory.Sheaf K RingCat} [∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : D), CategoryTheory.HasSheafify (K.over X) AddCommGrpCat] (G : CategoryTheory.Functor D C) [G.IsContinuous K J] [G.IsCocontinuous K J] (φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R) (η : (SheafOfModules.pushforward φ).obj (SheafOfModules.unit R) ≅ SheafOfModules.unit S) [∀ (X : D), (CategoryTheory.Over.post G).IsContinuous (K.over X) (J.over (G.obj X))] (h : ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y), CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} (SheafOfModules.pushforward (((CategoryTheory.Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))) {M : SheafOfModules R} (P : M.QuasicoherentData) : ((SheafOfModules.pushforward φ).obj M).QuasicoherentData
• SheafOfModules.QuasicoherentData.pushforward_I 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} {S : CategoryTheory.Sheaf K RingCat} [∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : D), CategoryTheory.HasSheafify (K.over X) AddCommGrpCat] (G : CategoryTheory.Functor D C) [G.IsContinuous K J] [G.IsCocontinuous K J] (φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R) (η : (SheafOfModules.pushforward φ).obj (SheafOfModules.unit R) ≅ SheafOfModules.unit S) [∀ (X : D), (CategoryTheory.Over.post G).IsContinuous (K.over X) (J.over (G.obj X))] (h : ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y), CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} (SheafOfModules.pushforward (((CategoryTheory.Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))) {M : SheafOfModules R} (P : M.QuasicoherentData) : (SheafOfModules.QuasicoherentData.pushforward G φ η h P).I = ((X : D) × (i : P.I) × (G.obj X ⟶ P.X i))
• SheafOfModules.QuasicoherentData.pushforward_X 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} {S : CategoryTheory.Sheaf K RingCat} [∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : D), CategoryTheory.HasSheafify (K.over X) AddCommGrpCat] (G : CategoryTheory.Functor D C) [G.IsContinuous K J] [G.IsCocontinuous K J] (φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R) (η : (SheafOfModules.pushforward φ).obj (SheafOfModules.unit R) ≅ SheafOfModules.unit S) [∀ (X : D), (CategoryTheory.Over.post G).IsContinuous (K.over X) (J.over (G.obj X))] (h : ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y), CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} (SheafOfModules.pushforward (((CategoryTheory.Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))) {M : SheafOfModules R} (P : M.QuasicoherentData) (i : (X : D) × (i : P.I) × (G.obj X ⟶ P.X i)) : (SheafOfModules.QuasicoherentData.pushforward G φ η h P).X i = i.fst
• AlgebraicGeometry.Scheme.Hom.instIsCocontinuousOpensOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat 📋 Mathlib.AlgebraicGeometry.OpenImmersion
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] : (AlgebraicGeometry.Scheme.Hom.opensFunctor f).IsCocontinuous (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥Y)
• CategoryTheory.GrothendieckTopology.Point.map 📋 Mathlib.CategoryTheory.Sites.Point.Map
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] : K.Point
• CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap 📋 Mathlib.CategoryTheory.Sites.Point.Map
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) (X : C) (x : Φ.fiber.obj X) : P.obj (Opposite.op (F.obj X)) ⟶ (Φ.map F K).presheafFiber.obj P
• CategoryTheory.GrothendieckTopology.Point.presheafFiberMapObjIso 📋 Mathlib.CategoryTheory.Sites.Point.Map
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) : (Φ.map F K).presheafFiber.obj P ≅ Φ.presheafFiber.obj (F.op.comp P)
• CategoryTheory.GrothendieckTopology.Point.presheafFiberMapCocone 📋 Mathlib.CategoryTheory.Sites.Point.Map
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) : CategoryTheory.Limits.Cocone ((CategoryTheory.CategoryOfElements.π Φ.fiber).op.comp (F.op.comp P))
• CategoryTheory.GrothendieckTopology.Point.isColimitPresheafFiberMapCocone 📋 Mathlib.CategoryTheory.Sites.Point.Map
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) : CategoryTheory.Limits.IsColimit (Φ.presheafFiberMapCocone F K P)
• CategoryTheory.GrothendieckTopology.Point.sheafFiberMapIso 📋 Mathlib.CategoryTheory.Sites.Point.Map
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] (A : Type u'') [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] [F.IsContinuous J K] : (Φ.map F K).sheafFiber ≅ (F.sheafPushforwardContinuous A J K).comp Φ.sheafFiber
• CategoryTheory.GrothendieckTopology.Point.presheafFiberMapCocone_pt 📋 Mathlib.CategoryTheory.Sites.Point.Map
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) : (Φ.presheafFiberMapCocone F K P).pt = (Φ.map F K).presheafFiber.obj P
• CategoryTheory.GrothendieckTopology.Point.presheafFiberMapIso 📋 Mathlib.CategoryTheory.Sites.Point.Map
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] (A : Type u'') [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] : (Φ.map F K).presheafFiber ≅ ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj F.op).comp Φ.presheafFiber
• CategoryTheory.GrothendieckTopology.Point.presheafFiberMap_hom_ext 📋 Mathlib.CategoryTheory.Sites.Point.Map
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P : CategoryTheory.Functor Dᵒᵖ A} {T : A} {f g : (Φ.map F K).presheafFiber.obj P ⟶ T} (h : ∀ (X : C) (x : Φ.fiber.obj X), CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) f = CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) g) : f = g
• CategoryTheory.GrothendieckTopology.Point.presheafFiberMap_hom_ext_iff 📋 Mathlib.CategoryTheory.Sites.Point.Map
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} {Φ : J.Point} {F : CategoryTheory.Functor C D} {K : CategoryTheory.GrothendieckTopology D} [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P : CategoryTheory.Functor Dᵒᵖ A} {T : A} {f g : (Φ.map F K).presheafFiber.obj P ⟶ T} : f = g ↔ ∀ (X : C) (x : Φ.fiber.obj X), CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) f = CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) g
• CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_presheafFiberMapObjIso_hom 📋 Mathlib.CategoryTheory.Sites.Point.Map
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) (X : C) (x : Φ.fiber.obj X) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) (Φ.presheafFiberMapObjIso F K P).hom = Φ.toPresheafFiber X x (F.op.comp P)
• CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberMapObjIso_inv 📋 Mathlib.CategoryTheory.Sites.Point.Map
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) (X : C) (x : Φ.fiber.obj X) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (F.op.comp P)) (Φ.presheafFiberMapObjIso F K P).inv = Φ.toPresheafFiberMap F K P X x
• CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_w 📋 Mathlib.CategoryTheory.Sites.Point.Map
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {X Y : C} (f : X ⟶ Y) (x : Φ.fiber.obj X) (P : CategoryTheory.Functor Dᵒᵖ A) : CategoryTheory.CategoryStruct.comp (P.map (F.map f).op) (Φ.toPresheafFiberMap F K P X x) = Φ.toPresheafFiberMap F K P Y ((CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f)) x)
• CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_naturality 📋 Mathlib.CategoryTheory.Sites.Point.Map
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P Q : CategoryTheory.Functor Dᵒᵖ A} (g : P ⟶ Q) (X : C) (x : Φ.fiber.obj X) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) ((Φ.map F K).presheafFiber.map g) = CategoryTheory.CategoryStruct.comp (g.app (Opposite.op (F.obj X))) (Φ.toPresheafFiberMap F K Q X x)
• CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_presheafFiberMapObjIso_hom_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Map
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) (X : C) (x : Φ.fiber.obj X) {Z : A} (h : Φ.presheafFiber.obj (F.op.comp P) ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) (CategoryTheory.CategoryStruct.comp (Φ.presheafFiberMapObjIso F K P).hom h) = CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (F.op.comp P)) h
• CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_naturality_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Map
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P Q : CategoryTheory.Functor Dᵒᵖ A} (g : P ⟶ Q) (X : C) (x : Φ.fiber.obj X) {Z : A} (h : (Φ.map F K).presheafFiber.obj Q ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) (CategoryTheory.CategoryStruct.comp ((Φ.map F K).presheafFiber.map g) h) = CategoryTheory.CategoryStruct.comp (g.app (Opposite.op (F.obj X))) (CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K Q X x) h)
• CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_w_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Map
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {X Y : C} (f : X ⟶ Y) (x : Φ.fiber.obj X) (P : CategoryTheory.Functor Dᵒᵖ A) {Z : A} (h : (Φ.map F K).presheafFiber.obj P ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.map (F.map f).op) (CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) h) = CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P Y ((CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f)) x)) h
• CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberMapObjIso_inv_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Map
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) (X : C) (x : Φ.fiber.obj X) {Z : A} (h : (Φ.map F K).presheafFiber.obj P ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (F.op.comp P)) (CategoryTheory.CategoryStruct.comp (Φ.presheafFiberMapObjIso F K P).inv h) = CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) h
• CategoryTheory.GrothendieckTopology.Point.presheafFiberMapCocone_ι_app 📋 Mathlib.CategoryTheory.Sites.Point.Map
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) (x : Φ.fiber.Elementsᵒᵖ) : (Φ.presheafFiberMapCocone F K P).ι.app x = Φ.toPresheafFiberMap F K P (Opposite.unop x).fst (Opposite.unop x).snd
• CategoryTheory.GrothendieckTopology.Point.presheafFiberMapIso_hom_app 📋 Mathlib.CategoryTheory.Sites.Point.Map
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] (A : Type u'') [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (X : CategoryTheory.Functor Dᵒᵖ A) : (Φ.presheafFiberMapIso F K A).hom.app X = (Φ.presheafFiberMapObjIso F K X).hom
• CategoryTheory.GrothendieckTopology.Point.presheafFiberMapIso_inv_app 📋 Mathlib.CategoryTheory.Sites.Point.Map
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] (A : Type u'') [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (X : CategoryTheory.Functor Dᵒᵖ A) : (Φ.presheafFiberMapIso F K A).inv.app X = (Φ.presheafFiberMapObjIso F K X).inv
• CategoryTheory.GrothendieckTopology.Point.map_aux 📋 Mathlib.CategoryTheory.Sites.Point.Map
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] ⦃X : D⦄ (R : CategoryTheory.Sieve X) (hR : R ∈ K X) ⦃u : Φ.fiber.Elements⦄ (f : ((CategoryTheory.CategoryOfElements.π Φ.fiber).comp F).obj u ⟶ X) : ∃ Y g, ∃ (_ : R.arrows g), ∃ v q a, CategoryTheory.CategoryStruct.comp a g = CategoryTheory.CategoryStruct.comp (F.map ↑q) f
• CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_naturality_apply 📋 Mathlib.CategoryTheory.Sites.Point.Map
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P Q : CategoryTheory.Functor Dᵒᵖ A} (g : P ⟶ Q) (X : C) (x : Φ.fiber.obj X) {F✝ : A → A → Type uF} {carrier : A → Type w_1} {instFunLike : (X Y : A) → FunLike (F✝ X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory A F✝] (x✝ : carrier (P.obj (Opposite.op (F.obj X)))) : (CategoryTheory.ConcreteCategory.hom ((Φ.map F K).presheafFiber.map g)) ((CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiberMap F K P X x)) x✝) = (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiberMap F K Q X x)) ((CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op (F.obj X)))) x✝)

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