Loogle!

Result

Found 191 declarations mentioning CategoryTheory.Limits.HasProducts.

• CategoryTheory.Limits.HasProducts 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop
• CategoryTheory.Limits.hasProducts_shrink 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] : CategoryTheory.Limits.HasProducts C
• CategoryTheory.Limits.has_smallest_products_of_hasProducts 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] : CategoryTheory.Limits.HasProducts C
• CategoryTheory.Limits.hasProductsOfShape_of_hasProducts 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] (J : Type w) : CategoryTheory.Limits.HasProductsOfShape J C
• CategoryTheory.Limits.piConst 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] : CategoryTheory.Functor C (CategoryTheory.Functor Type wᵒᵖ C)
• CategoryTheory.Limits.piFunctor 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] : CategoryTheory.Functor C (CategoryTheory.Functor Type wᵒᵖ C)
• CategoryTheory.Limits.hasProducts_of_limit_fans 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (lf : {J : Type w} → (f : J → C) → CategoryTheory.Limits.Fan f) (lf_isLimit : {J : Type w} → (f : J → C) → CategoryTheory.Limits.IsLimit (lf f)) : CategoryTheory.Limits.HasProducts C
• CategoryTheory.Limits.piConst_obj_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] (X : C) (n : Type wᵒᵖ) : (CategoryTheory.Limits.piConst.obj X).obj n = ∏ᶜ fun x => X
• CategoryTheory.Limits.piFunctor_obj_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] (X : C) (α : Type wᵒᵖ) : (CategoryTheory.Limits.piFunctor.obj X).obj α = ∏ᶜ fun t => X
• CategoryTheory.Limits.piConstAdj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] (X : C) : (CategoryTheory.Limits.piConst.obj X).rightOp ⊣ CategoryTheory.yoneda.obj X
• CategoryTheory.Limits.piConst_obj_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] (X : C) {X✝ Y✝ : Type wᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.piConst.obj X).map f = CategoryTheory.Limits.Pi.map' ⇑(CategoryTheory.ConcreteCategory.hom f.unop) fun x => CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.piFunctor_obj_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] (X : C) {X✝ Y✝ : Type wᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.piFunctor.obj X).map f = CategoryTheory.Limits.Pi.map' ⇑(CategoryTheory.ConcreteCategory.hom f.unop) fun x => CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.piConst_map_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (n : Type wᵒᵖ) : (CategoryTheory.Limits.piConst.map f).app n = CategoryTheory.Limits.Pi.map fun x => f
• CategoryTheory.Limits.piFunctor_map_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (T : Type wᵒᵖ) : (CategoryTheory.Limits.piFunctor.map f).app T = CategoryTheory.Limits.Pi.map fun x => f
• CategoryTheory.Limits.hasFiniteProducts_of_hasProducts 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] : CategoryTheory.Limits.HasFiniteProducts C
• CategoryTheory.Limits.Types.instHasProductsType 📋 Mathlib.CategoryTheory.Limits.Types.Products
  : CategoryTheory.Limits.HasProducts (Type v)
• CategoryTheory.Limits.has_limits_of_hasEqualizers_and_products 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v, u} C
• CategoryTheory.Limits.preservesLimits_of_preservesEqualizers_and_products 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasProducts C] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] [∀ (J : Type w), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) G] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, w, v, v₂, u, u₂} G
• CategoryTheory.Limits.createsLimitsOfSizeOfCreatesEqualizersAndProducts 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasEqualizers D] [CategoryTheory.Limits.HasProducts D] (G : CategoryTheory.Functor C D) [G.ReflectsIsomorphisms] [CategoryTheory.CreatesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] [(J : Type w) → CategoryTheory.CreatesLimitsOfShape (CategoryTheory.Discrete J) G] : CategoryTheory.CreatesLimitsOfSize.{w, w, v, v₂, u, u₂} G
• CategoryTheory.Limits.hasCoproducts_of_opposite 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasProducts Cᵒᵖ] : CategoryTheory.Limits.HasCoproducts C
• CategoryTheory.Limits.hasCoproducts_opposite 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasProducts C] : CategoryTheory.Limits.HasCoproducts Cᵒᵖ
• CategoryTheory.Limits.hasProducts_of_opposite 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasCoproducts Cᵒᵖ] : CategoryTheory.Limits.HasProducts C
• CategoryTheory.Limits.hasProducts_opposite 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasCoproducts C] : CategoryTheory.Limits.HasProducts Cᵒᵖ
• CategoryTheory.Limits.hasProducts_of_finite_and_cofiltered 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w, w, v, u} C] : CategoryTheory.Limits.HasProducts C
• CategoryTheory.Limits.hasCountableProducts_of_hasProducts 📋 Mathlib.CategoryTheory.Limits.Shapes.Countable
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasProducts C] : CategoryTheory.Limits.HasCountableProducts C
• CategoryTheory.AB4Star 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] : Prop
• CategoryTheory.AB4StarOfSize 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] : Prop
• CategoryTheory.AB4StarOfSize_shrink 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] [CategoryTheory.AB4StarOfSize.{max w w', v, u} C] : CategoryTheory.AB4StarOfSize.{w, v, u} C
• CategoryTheory.instAB4StarOfSize 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] [CategoryTheory.AB4StarOfSize.{w, v, u} C] : CategoryTheory.AB4StarOfSize.{0, v, u} C
• CategoryTheory.instCountableAB4StarOfAB4StarOfSize 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] [CategoryTheory.AB4StarOfSize.{0, v, u} C] : CategoryTheory.CountableAB4Star C
• CategoryTheory.AB4StarOfSize.mk 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] (ofShape : ∀ (α : Type w), CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete α) C) : CategoryTheory.AB4StarOfSize.{w, v, u} C
• CategoryTheory.AB4StarOfSize.ofShape 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Limits.HasProducts C} [self : CategoryTheory.AB4StarOfSize.{w, v, u} C] (α : Type w) : CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete α) C
• CategoryTheory.Limits.hasProductsOfShape_of_small 📋 Mathlib.CategoryTheory.Limits.EssentiallySmall
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (β : Type w₂) [Small.{w₁, w₂} β] [CategoryTheory.Limits.HasProducts C] : CategoryTheory.Limits.HasProductsOfShape β C
• CategoryTheory.has_weakly_initial_of_weakly_initial_set_and_hasProducts 📋 Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {ι : Type w} {B : ι → C} (hB : ∀ (A : C), ∃ i, Nonempty (B i ⟶ A)) : ∃ T, ∀ (X : C), Nonempty (T ⟶ X)
• CategoryTheory.Presheaf.firstObj 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {U : C} (R : CategoryTheory.Presieve U) (P : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Limits.HasProducts A] : A
• CategoryTheory.Presheaf.IsSheaf' 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasPullbacks C] (P : CategoryTheory.Functor Cᵒᵖ A) : Prop
• CategoryTheory.Presheaf.secondObj 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {U : C} (R : CategoryTheory.Presieve U) (P : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasPullbacks C] : A
• CategoryTheory.Presheaf.isSheaf_iff_isSheaf' 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A' : Type u₂} [CategoryTheory.Category.{max v₁ u₁, u₂} A'] (J : CategoryTheory.GrothendieckTopology C) (P' : CategoryTheory.Functor Cᵒᵖ A') [CategoryTheory.Limits.HasProducts A'] [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.Presheaf.IsSheaf J P' ↔ CategoryTheory.Presheaf.IsSheaf' J P'
• CategoryTheory.Presheaf.forkMap 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {U : C} (R : CategoryTheory.Presieve U) (P : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Limits.HasProducts A] : P.obj (Opposite.op U) ⟶ CategoryTheory.Presheaf.firstObj R P
• CategoryTheory.Presheaf.firstMap 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {U : C} (R : CategoryTheory.Presieve U) (P : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.Presheaf.firstObj R P ⟶ CategoryTheory.Presheaf.secondObj R P
• CategoryTheory.Presheaf.secondMap 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {U : C} (R : CategoryTheory.Presieve U) (P : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.Presheaf.firstObj R P ⟶ CategoryTheory.Presheaf.secondObj R P
• CategoryTheory.Presheaf.w 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {U : C} (R : CategoryTheory.Presieve U) (P : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.forkMap R P) (CategoryTheory.Presheaf.firstMap R P) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.forkMap R P) (CategoryTheory.Presheaf.secondMap R P)
• CategoryTheory.Presheaf.isSheafForIsSheafFor' 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasPullbacks C] (P : CategoryTheory.Functor Cᵒᵖ A) (s : CategoryTheory.Functor A (Type (max v₁ u₁))) [∀ (J : Type (max v₁ u₁)), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) s] (U : C) (R : CategoryTheory.Presieve U) : CategoryTheory.Limits.IsLimit (s.mapCone (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Presheaf.forkMap R P) ⋯)) ≃ CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Equalizer.forkMap (P.comp s) R) ⋯)
• CategoryTheory.Over.ConstructProducts.over_products_of_widePullbacks 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasWidePullbacks C] {B : C} : CategoryTheory.Limits.HasProducts (CategoryTheory.Over B)
• CategoryTheory.GrothendieckTopology.Point.skyscraperSheaf 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] (M : A) : CategoryTheory.Sheaf J A
• CategoryTheory.GrothendieckTopology.Point.skyscraperPresheaf 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] (M : A) : CategoryTheory.Functor Cᵒᵖ A
• CategoryTheory.GrothendieckTopology.Point.isSheaf_skyscraperPresheaf 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] (M : A) : CategoryTheory.Presheaf.IsSheaf J (Φ.skyscraperPresheaf M)
• CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafFunctor 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] : CategoryTheory.Functor A (CategoryTheory.Functor Cᵒᵖ A)
• CategoryTheory.GrothendieckTopology.Point.skyscraperSheafFunctor 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] : CategoryTheory.Functor A (CategoryTheory.Sheaf J A)
• CategoryTheory.GrothendieckTopology.Point.W_isInvertedBy_presheafFiber 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] : J.W.IsInvertedBy Φ.presheafFiber
• CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafAdjunction 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] : Φ.presheafFiber ⊣ Φ.skyscraperPresheafFunctor
• CategoryTheory.GrothendieckTopology.Point.instIsLeftAdjointSheafSheafFiber 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] : Φ.sheafFiber.IsLeftAdjoint
• CategoryTheory.GrothendieckTopology.Point.instIsRightAdjointSheafSkyscraperSheafFunctor 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] : Φ.skyscraperSheafFunctor.IsRightAdjoint
• CategoryTheory.GrothendieckTopology.Point.instPreservesFiniteColimitsSheafSheafFiber 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] : CategoryTheory.Limits.PreservesFiniteColimits Φ.sheafFiber
• CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] : Φ.sheafFiber ⊣ Φ.skyscraperSheafFunctor
• CategoryTheory.GrothendieckTopology.Point.skyscraperSheafFunctor_obj_obj 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] (M : A) : (Φ.skyscraperSheafFunctor.obj M).obj = Φ.skyscraperPresheaf M
• CategoryTheory.GrothendieckTopology.Point.instLiftingFunctorOppositeSheafPresheafToSheafWPresheafFiberSheafFiber 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.HasWeakSheafify J A] : CategoryTheory.Localization.Lifting (CategoryTheory.presheafToSheaf J A) J.W Φ.presheafFiber Φ.sheafFiber
• CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafFunctor_obj_obj 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] (k : A) (j : Cᵒᵖ) : (Φ.skyscraperPresheafFunctor.obj k).obj j = ∏ᶜ fun t => k
• CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] {P : CategoryTheory.Functor Cᵒᵖ A} {M : A} [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] : (Φ.presheafFiber.obj P ⟶ M) ≃ (P ⟶ Φ.skyscraperPresheaf M)
• CategoryTheory.GrothendieckTopology.Point.presheafToSheafCompSheafFiber 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.HasWeakSheafify J A] : (CategoryTheory.presheafToSheaf J A).comp Φ.sheafFiber ≅ Φ.presheafFiber
• CategoryTheory.GrothendieckTopology.Point.presheafToSheafCompSheafFiberIso 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.HasWeakSheafify J A] : (CategoryTheory.presheafToSheaf J A).comp Φ.sheafFiber ≅ Φ.presheafFiber
• CategoryTheory.GrothendieckTopology.Point.instIsIsoMapFunctorOppositePresheafFiberToSheafify 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (P : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.HasWeakSheafify J A] : CategoryTheory.IsIso (Φ.presheafFiber.map (CategoryTheory.toSheafify J P))
• CategoryTheory.GrothendieckTopology.Point.skyscraperSheafFunctor_map_hom 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] {X✝ Y✝ : A} (f : X✝ ⟶ Y✝) : (Φ.skyscraperSheafFunctor.map f).hom = Φ.skyscraperPresheafFunctor.map f
• CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafFunctor_obj_map 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] (k : A) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : (Φ.skyscraperPresheafFunctor.obj k).map f = CategoryTheory.Limits.Pi.map' ⇑(CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f.unop)) fun x => CategoryTheory.CategoryStruct.id k
• CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_app_π 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] {P : CategoryTheory.Functor Cᵒᵖ A} {M : A} [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (f : Φ.presheafFiber.obj P ⟶ M) (X : C) (x : Φ.fiber.obj X) : CategoryTheory.CategoryStruct.comp ((Φ.skyscraperPresheafHomEquiv f).app (Opposite.op X)) (CategoryTheory.Limits.Pi.π (fun x => M) x) = CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P) f
• CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_apply_app 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] {P : CategoryTheory.Functor Cᵒᵖ A} {M : A} [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (f : Φ.presheafFiber.obj P ⟶ M) (X : Cᵒᵖ) : (Φ.skyscraperPresheafHomEquiv f).app X = CategoryTheory.Limits.Pi.lift fun x => CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber (Opposite.unop X) x P) f
• CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_symm_apply 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] {P : CategoryTheory.Functor Cᵒᵖ A} {M : A} [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (g : P ⟶ Φ.skyscraperPresheaf M) : Φ.skyscraperPresheafHomEquiv.symm g = Φ.presheafFiberDesc (fun X x => CategoryTheory.CategoryStruct.comp (g.app (Opposite.op X)) (CategoryTheory.Limits.Pi.π (fun t => M) x)) ⋯
• CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_app_π_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] {P : CategoryTheory.Functor Cᵒᵖ A} {M : A} [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (f : Φ.presheafFiber.obj P ⟶ M) (X : C) (x : Φ.fiber.obj X) {Z : A} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp ((Φ.skyscraperPresheafHomEquiv f).app (Opposite.op X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun x => M) x) h) = CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P) (CategoryTheory.CategoryStruct.comp f h)
• CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_skyscraperPresheafHomEquiv_symm 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] {P : CategoryTheory.Functor Cᵒᵖ A} {M : A} [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (g : P ⟶ Φ.skyscraperPresheaf M) (X : C) (x : Φ.fiber.obj X) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P) (Φ.skyscraperPresheafHomEquiv.symm g) = CategoryTheory.CategoryStruct.comp (g.app (Opposite.op X)) (CategoryTheory.Limits.Pi.π (fun t => M) x)
• CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_skyscraperPresheafHomEquiv_symm_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] {P : CategoryTheory.Functor Cᵒᵖ A} {M : A} [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (g : P ⟶ Φ.skyscraperPresheaf M) (X : C) (x : Φ.fiber.obj X) {Z : A} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P) (CategoryTheory.CategoryStruct.comp (Φ.skyscraperPresheafHomEquiv.symm g) h) = CategoryTheory.CategoryStruct.comp (g.app (Opposite.op X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun t => M) x) h)
• CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafFunctor_map_app 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] {X✝ Y✝ : A} (f : X✝ ⟶ Y✝) (j : Cᵒᵖ) : (Φ.skyscraperPresheafFunctor.map f).app j = CategoryTheory.Limits.Pi.map fun x => f
• CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_right 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] {P : CategoryTheory.Functor Cᵒᵖ A} {M N : A} [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (f : Φ.presheafFiber.obj P ⟶ M) (g : M ⟶ N) : Φ.skyscraperPresheafHomEquiv (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (Φ.skyscraperPresheafHomEquiv f) (Φ.skyscraperPresheafFunctor.map g)
• CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafAdjunction_homEquiv_apply 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {P : CategoryTheory.Functor Cᵒᵖ A} {M : A} (f : Φ.presheafFiber.obj P ⟶ M) : (Φ.skyscraperPresheafAdjunction.homEquiv P M) f = Φ.skyscraperPresheafHomEquiv f
• CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_left 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] {P Q : CategoryTheory.Functor Cᵒᵖ A} {M : A} [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (f : P ⟶ Q) (g : Φ.presheafFiber.obj Q ⟶ M) : Φ.skyscraperPresheafHomEquiv (CategoryTheory.CategoryStruct.comp (Φ.presheafFiber.map f) g) = CategoryTheory.CategoryStruct.comp f (Φ.skyscraperPresheafHomEquiv g)
• CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_right_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] {P : CategoryTheory.Functor Cᵒᵖ A} {M N : A} [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (f : Φ.presheafFiber.obj P ⟶ M) (g : M ⟶ N) {Z : CategoryTheory.Functor Cᵒᵖ A} (h : Φ.skyscraperPresheaf N ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.skyscraperPresheafHomEquiv (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (Φ.skyscraperPresheafHomEquiv f) (CategoryTheory.CategoryStruct.comp (Φ.skyscraperPresheafFunctor.map g) h)
• CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_left_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] {P Q : CategoryTheory.Functor Cᵒᵖ A} {M : A} [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (f : P ⟶ Q) (g : Φ.presheafFiber.obj Q ⟶ M) {Z : CategoryTheory.Functor Cᵒᵖ A} (h : Φ.skyscraperPresheaf M ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.skyscraperPresheafHomEquiv (CategoryTheory.CategoryStruct.comp (Φ.presheafFiber.map f) g)) h = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (Φ.skyscraperPresheafHomEquiv g) h)
• CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafAdjunction_homEquiv_symm_apply 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {P : CategoryTheory.Functor Cᵒᵖ A} {M : A} (f : P ⟶ Φ.skyscraperPresheaf M) : (Φ.skyscraperPresheafAdjunction.homEquiv P M).symm f = Φ.skyscraperPresheafHomEquiv.symm f
• CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_left_symm 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] {P Q : CategoryTheory.Functor Cᵒᵖ A} {M : A} [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (f : P ⟶ Q) (g : Q ⟶ Φ.skyscraperPresheaf M) : Φ.skyscraperPresheafHomEquiv.symm (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (Φ.presheafFiber.map f) (Φ.skyscraperPresheafHomEquiv.symm g)
• CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_left_symm_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] {P Q : CategoryTheory.Functor Cᵒᵖ A} {M : A} [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (f : P ⟶ Q) (g : Q ⟶ Φ.skyscraperPresheaf M) {Z : A} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.skyscraperPresheafHomEquiv.symm (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (Φ.presheafFiber.map f) (CategoryTheory.CategoryStruct.comp (Φ.skyscraperPresheafHomEquiv.symm g) h)
• CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction_homEquiv_apply_hom 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {F : CategoryTheory.Sheaf J A} {M : A} (f : Φ.presheafFiber.obj F.obj ⟶ M) : ((Φ.skyscraperSheafAdjunction.homEquiv F M) f).hom = Φ.skyscraperPresheafHomEquiv f
• CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction_homEquiv_apply_val 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {F : CategoryTheory.Sheaf J A} {M : A} (f : Φ.presheafFiber.obj F.obj ⟶ M) : ((Φ.skyscraperSheafAdjunction.homEquiv F M) f).hom = Φ.skyscraperPresheafHomEquiv f
• CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction_homEquiv_symm_apply 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {F : CategoryTheory.Sheaf J A} {M : A} (f : F ⟶ Φ.skyscraperSheaf M) : (Φ.skyscraperSheafAdjunction.homEquiv F M).symm f = Φ.skyscraperPresheafHomEquiv.symm f.hom
• CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectEpimorphisms 📋 Mathlib.CategoryTheory.Sites.Point.Conservative
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)] [hJ : J.HasSheafCompose (CategoryTheory.forget A)] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.Limits.HasProducts A] : CategoryTheory.JointlyReflectEpimorphisms fun Φ => Φ.obj.sheafFiber
• CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.W_iff 📋 Mathlib.CategoryTheory.Sites.Point.Conservative
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)] [hJ : J.HasSheafCompose (CategoryTheory.forget A)] {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.Limits.HasProducts A] : J.W f ↔ ∀ (Φ : P.FullSubcategory), CategoryTheory.IsIso (Φ.obj.presheafFiber.map f)
• CategoryTheory.Grpd.has_pi 📋 Mathlib.CategoryTheory.Groupoid.Grpd.Basic
  : CategoryTheory.Limits.HasProducts CategoryTheory.Grpd
• CategoryTheory.Limits.IsIPC 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasProducts C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, u_3, v_1, u_1} C] : Prop
• CategoryTheory.Limits.IsIPC.isIPCOfShape 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {inst✝¹ : CategoryTheory.Limits.HasProducts C} {inst✝² : CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, u_3, v_1, u_1} C} [self : CategoryTheory.Limits.IsIPC C] (ι : Type w) : CategoryTheory.Limits.IsIPCOfShape.{w, w, v_1, u_1} ι C
• CategoryTheory.Limits.IsIPC.mk 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasProducts C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, u_3, v_1, u_1} C] (isIPCOfShape : ∀ (ι : Type w), CategoryTheory.Limits.IsIPCOfShape.{w, w, v_1, u_1} ι C := by infer_instance) : CategoryTheory.Limits.IsIPC C
• CategoryTheory.Limits.instIsIPCOfShapeOfIsIPCOfSmall 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasProducts C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v_1, u_1} C] [CategoryTheory.Limits.IsIPC C] (ι : Type u_3) [Small.{w, u_3} ι] [CategoryTheory.Limits.HasProductsOfShape ι C] : CategoryTheory.Limits.IsIPCOfShape.{w, u_3, v_1, u_1} ι C
• CategoryTheory.Limits.instIsIPCFunctor 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C] [CategoryTheory.Limits.IsIPC C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] : CategoryTheory.Limits.IsIPC (CategoryTheory.Functor D C)
• CategoryTheory.Limits.FormalCoproduct.evalOp 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Limits.HasProducts A] : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Functor (CategoryTheory.Limits.FormalCoproduct C)ᵒᵖ A)
• CategoryTheory.Limits.FormalCoproduct.instPreservesLimitOppositeDiscreteFunctorCompOpObjFunctorEvalOp 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Limits.HasProducts A] (J : Type w) (f : J → CategoryTheory.Limits.FormalCoproduct C) (F : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor (Opposite.op ∘ f)) ((CategoryTheory.Limits.FormalCoproduct.evalOp C A).obj F)
• CategoryTheory.Limits.FormalCoproduct.evalOp_obj_obj 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Limits.HasProducts A] (F : CategoryTheory.Functor Cᵒᵖ A) (X : (CategoryTheory.Limits.FormalCoproduct C)ᵒᵖ) : ((CategoryTheory.Limits.FormalCoproduct.evalOp C A).obj F).obj X = ∏ᶜ fun i => F.obj (Opposite.op ((Opposite.unop X).obj i))
• CategoryTheory.Limits.FormalCoproduct.isLimitEvalMapConeCofanOp 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Limits.HasProducts A] (J : Type w) (f : J → CategoryTheory.Limits.FormalCoproduct C) (F : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.Limits.IsLimit (((CategoryTheory.Limits.FormalCoproduct.evalOp C A).obj F).mapCone (CategoryTheory.Limits.FormalCoproduct.cofan J f).op)
• CategoryTheory.Limits.FormalCoproduct.evalOpCompInlIsoId 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Limits.HasProducts A] : (CategoryTheory.Limits.FormalCoproduct.evalOp C A).comp ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ (CategoryTheory.Limits.FormalCoproduct C)ᵒᵖ A).obj (CategoryTheory.Limits.FormalCoproduct.incl C).op) ≅ CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ A)
• CategoryTheory.Limits.FormalCoproduct.evalOp_obj_map 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Limits.HasProducts A] (F : CategoryTheory.Functor Cᵒᵖ A) {X✝ Y✝ : (CategoryTheory.Limits.FormalCoproduct C)ᵒᵖ} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Limits.FormalCoproduct.evalOp C A).obj F).map f = CategoryTheory.Limits.Pi.lift fun i => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun i => F.obj (Opposite.op ((Opposite.unop X✝).obj i))) (f.unop.f i)) (F.map (f.unop.φ i).op)
• CategoryTheory.Limits.FormalCoproduct.evalOpCompInlIsoId_hom_app_app 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Limits.HasProducts A] (X : CategoryTheory.Functor Cᵒᵖ A) (X✝ : Cᵒᵖ) : ((CategoryTheory.Limits.FormalCoproduct.evalOpCompInlIsoId C A).hom.app X).app X✝ = CategoryTheory.Limits.Pi.π (fun i => X.obj X✝) PUnit.unit
• CategoryTheory.Limits.FormalCoproduct.evalOpCompInlIsoId_inv_app_app 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Limits.HasProducts A] (X : CategoryTheory.Functor Cᵒᵖ A) (X✝ : Cᵒᵖ) : ((CategoryTheory.Limits.FormalCoproduct.evalOpCompInlIsoId C A).inv.app X).app X✝ = CategoryTheory.Limits.Pi.lift fun x => CategoryTheory.CategoryStruct.id (X.obj X✝)
• CategoryTheory.Limits.FormalCoproduct.evalOp_map_app 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Limits.HasProducts A] {X✝ Y✝ : CategoryTheory.Functor Cᵒᵖ A} (α : X✝ ⟶ Y✝) (f : (CategoryTheory.Limits.FormalCoproduct C)ᵒᵖ) : ((CategoryTheory.Limits.FormalCoproduct.evalOp C A).map α).app f = CategoryTheory.Limits.Pi.map fun i => α.app (Opposite.op ((Opposite.unop f).obj i))
• CategoryTheory.Limits.FormalCoproduct.powerBifunctor 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] : CategoryTheory.Functor Type tᵒᵖ (CategoryTheory.Functor (CategoryTheory.Limits.FormalCoproduct C) (CategoryTheory.Limits.FormalCoproduct C))
• CategoryTheory.Limits.FormalCoproduct.powerBifunctor_obj 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] (α : Type tᵒᵖ) : CategoryTheory.Limits.FormalCoproduct.powerBifunctor.obj α = CategoryTheory.Limits.FormalCoproduct.powerFunctor (Opposite.unop α)
• CategoryTheory.Limits.FormalCoproduct.powerBifunctor_map_app 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X✝ Y✝ : Type tᵒᵖ} (f : X✝ ⟶ Y✝) (x✝ : CategoryTheory.Limits.FormalCoproduct C) : (CategoryTheory.Limits.FormalCoproduct.powerBifunctor.map f).app x✝ = x✝.mapPower ⇑(CategoryTheory.ConcreteCategory.hom f.unop)
• CategoryTheory.instIsThin 📋 Mathlib.CategoryTheory.Limits.SmallComplete
  {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasProducts C] : Quiver.IsThin C
• CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheaf 📋 Mathlib.CategoryTheory.Sites.LocalSite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] : CategoryTheory.Functor A (CategoryTheory.Sheaf J A)
• CategoryTheory.GrothendieckTopology.IsLocalSite.instFaithfulSheafConstantSheafOfHasColimitsOfSizeOfHasProducts 📋 Mathlib.CategoryTheory.Sites.LocalSite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.IsLocalSite] (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{v, v, v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.HasWeakSheafify J A] : (CategoryTheory.constantSheaf J A).Faithful
• CategoryTheory.GrothendieckTopology.IsLocalSite.instFullSheafConstantSheafOfHasColimitsOfSizeOfHasProducts 📋 Mathlib.CategoryTheory.Sites.LocalSite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.IsLocalSite] (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{v, v, v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.HasWeakSheafify J A] : (CategoryTheory.constantSheaf J A).Full
• CategoryTheory.GrothendieckTopology.IsLocalSite.faithful_constantSheaf 📋 Mathlib.CategoryTheory.Sites.LocalSite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.HasWeakSheafify J A] : (CategoryTheory.constantSheaf J A).Faithful
• CategoryTheory.GrothendieckTopology.IsLocalSite.full_constantSheaf 📋 Mathlib.CategoryTheory.Sites.LocalSite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.HasWeakSheafify J A] : (CategoryTheory.constantSheaf J A).Full
• CategoryTheory.GrothendieckTopology.IsLocalSite.fullyFaithfulConstantSheaf 📋 Mathlib.CategoryTheory.Sites.LocalSite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.HasWeakSheafify J A] : (CategoryTheory.constantSheaf J A).FullyFaithful
• CategoryTheory.GrothendieckTopology.IsLocalSite.fullyFaithfulCoconstantSheaf 📋 Mathlib.CategoryTheory.Sites.LocalSite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.HasWeakSheafify J A] : (CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheaf J A).FullyFaithful
• CategoryTheory.GrothendieckTopology.IsLocalSite.instFaithfulSheafCoconstantSheaf 📋 Mathlib.CategoryTheory.Sites.LocalSite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.HasWeakSheafify J A] : (CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheaf J A).Faithful
• CategoryTheory.GrothendieckTopology.IsLocalSite.instFullSheafCoconstantSheaf 📋 Mathlib.CategoryTheory.Sites.LocalSite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.HasWeakSheafify J A] : (CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheaf J A).Full
• CategoryTheory.GrothendieckTopology.IsLocalSite.instIsRightAdjointSheafCoconstantSheaf 📋 Mathlib.CategoryTheory.Sites.LocalSite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.HasWeakSheafify J A] : (CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheaf J A).IsRightAdjoint
• CategoryTheory.GrothendieckTopology.IsLocalSite.instIsLeftAdjointSheafΓOfHasColimitsOfSizeOfHasProducts 📋 Mathlib.CategoryTheory.Sites.LocalSite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.IsLocalSite] (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{v, v, v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.HasWeakSheafify J A] : (CategoryTheory.Sheaf.Γ J A).IsLeftAdjoint
• CategoryTheory.GrothendieckTopology.IsLocalSite.Γ_isLeftAdjoint 📋 Mathlib.CategoryTheory.Sites.LocalSite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.HasWeakSheafify J A] : (CategoryTheory.Sheaf.Γ J A).IsLeftAdjoint
• CategoryTheory.GrothendieckTopology.IsLocalSite.ΓCoconstantSheafAdj 📋 Mathlib.CategoryTheory.Sites.LocalSite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.HasWeakSheafify J A] : CategoryTheory.Sheaf.Γ J A ⊣ CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheaf J A
• CategoryTheory.GrothendieckTopology.IsLocalSite.constantΓCoconstantTriple 📋 Mathlib.CategoryTheory.Sites.LocalSite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.HasWeakSheafify J A] : CategoryTheory.Adjunction.Triple (CategoryTheory.constantSheaf J A) (CategoryTheory.Sheaf.Γ J A) (CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheaf J A)
• CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheafΓNatIsoId 📋 Mathlib.CategoryTheory.Sites.LocalSite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.HasWeakSheafify J A] : (CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheaf J A).comp (CategoryTheory.Sheaf.Γ J A) ≅ CategoryTheory.Functor.id A
• CategoryTheory.GrothendieckTopology.Point.skyscraperSheafFunctorCompSheafPushforwardContinuous 📋 Mathlib.CategoryTheory.Sites.Point.Comap
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} (Φ : K.Point) (F : CategoryTheory.Functor C D) [CategoryTheory.RepresentablyFlat F] {J : CategoryTheory.GrothendieckTopology C} (hF : CategoryTheory.CoverPreserving J K F) [CategoryTheory.InitiallySmall (F.comp Φ.fiber).Elements] (A : Type u_3) [CategoryTheory.Category.{v, u_3} A] [CategoryTheory.Limits.HasProducts A] [F.IsContinuous J K] : Φ.skyscraperSheafFunctor.comp (F.sheafPushforwardContinuous A J K) ≅ (Φ.comap F hF).skyscraperSheafFunctor
• CategoryTheory.GrothendieckTopology.Point.sheafFiberComapIso 📋 Mathlib.CategoryTheory.Sites.Point.Comap
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} (Φ : K.Point) (F : CategoryTheory.Functor C D) [CategoryTheory.RepresentablyFlat F] {J : CategoryTheory.GrothendieckTopology C} (hF : CategoryTheory.CoverPreserving J K F) [CategoryTheory.InitiallySmall (F.comp Φ.fiber).Elements] (A : Type u_3) [CategoryTheory.Category.{v, u_3} A] [CategoryTheory.Limits.HasProducts A] [F.IsContinuous J K] [(F.sheafPushforwardContinuous A J K).IsRightAdjoint] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u_3} A] : (Φ.comap F hF).sheafFiber ≅ (F.sheafPullback A J K).comp Φ.sheafFiber
• CategoryTheory.GrothendieckTopology.Point.sheafFiberComapIso_hom_app 📋 Mathlib.CategoryTheory.Sites.Point.Comap
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} (Φ : K.Point) (F : CategoryTheory.Functor C D) [CategoryTheory.RepresentablyFlat F] {J : CategoryTheory.GrothendieckTopology C} (hF : CategoryTheory.CoverPreserving J K F) [CategoryTheory.InitiallySmall (F.comp Φ.fiber).Elements] (A : Type u_3) [CategoryTheory.Category.{v, u_3} A] [CategoryTheory.Limits.HasProducts A] [F.IsContinuous J K] [(F.sheafPushforwardContinuous A J K).IsRightAdjoint] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u_3} A] (X : CategoryTheory.Sheaf J A) : (Φ.sheafFiberComapIso F hF A).hom.app X = CategoryTheory.CategoryStruct.comp ((Φ.comap F hF).sheafFiber.map ((F.sheafAdjunctionContinuous A J K).unit.app X)) (CategoryTheory.CategoryStruct.comp ((Φ.comap F hF).sheafFiber.map ((F.sheafPushforwardContinuous A J K).map (Φ.skyscraperSheafAdjunction.unit.app ((F.sheafPullback A J K).obj X)))) (CategoryTheory.CategoryStruct.comp ((Φ.comap F hF).sheafFiber.map ((Φ.skyscraperSheafFunctorCompSheafPushforwardContinuous F hF A).hom.app (Φ.sheafFiber.obj ((F.sheafPullback A J K).obj X)))) ((Φ.comap F hF).skyscraperSheafAdjunction.counit.app (Φ.sheafFiber.obj ((F.sheafPullback A J K).obj X)))))
• CategoryTheory.GrothendieckTopology.Point.sheafFiberComapIso_inv_app 📋 Mathlib.CategoryTheory.Sites.Point.Comap
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} (Φ : K.Point) (F : CategoryTheory.Functor C D) [CategoryTheory.RepresentablyFlat F] {J : CategoryTheory.GrothendieckTopology C} (hF : CategoryTheory.CoverPreserving J K F) [CategoryTheory.InitiallySmall (F.comp Φ.fiber).Elements] (A : Type u_3) [CategoryTheory.Category.{v, u_3} A] [CategoryTheory.Limits.HasProducts A] [F.IsContinuous J K] [(F.sheafPushforwardContinuous A J K).IsRightAdjoint] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u_3} A] (X : CategoryTheory.Sheaf J A) : (Φ.sheafFiberComapIso F hF A).inv.app X = CategoryTheory.CategoryStruct.comp (Φ.sheafFiber.map ((F.sheafPullback A J K).map ((Φ.comap F hF).skyscraperSheafAdjunction.unit.app X))) (CategoryTheory.CategoryStruct.comp (Φ.sheafFiber.map ((F.sheafPullback A J K).map ((Φ.skyscraperSheafFunctorCompSheafPushforwardContinuous F hF A).inv.app ((Φ.comap F hF).sheafFiber.obj X)))) (CategoryTheory.CategoryStruct.comp (Φ.sheafFiber.map ((F.sheafAdjunctionContinuous A J K).counit.app (Φ.skyscraperSheafFunctor.obj ((Φ.comap F hF).sheafFiber.obj X)))) (Φ.skyscraperSheafAdjunction.counit.app ((Φ.comap F hF).sheafFiber.obj X))))
• CategoryTheory.GrothendieckTopology.Point.instMonoidalSheafSheafFiber 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorRight X)] [J.W.IsMonoidal] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.Limits.HasProducts A] : Φ.sheafFiber.Monoidal
• CategoryTheory.GrothendieckTopology.Point.instIsMonoidalFunctorOppositeHomPresheafToSheafCompSheafFiberIso 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorRight X)] [J.W.IsMonoidal] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.Limits.HasProducts A] : CategoryTheory.NatTrans.IsMonoidal (Φ.presheafToSheafCompSheafFiberIso A).hom
• CategoryTheory.instIsMonoidalFunctorOppositeWOfHasSheafComposeForgetOfHasEnoughPoints 📋 Mathlib.CategoryTheory.Sites.Point.IsMonoidalW
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {J : CategoryTheory.GrothendieckTopology C} (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasProducts A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [CategoryTheory.HasWeakSheafify J A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorRight X)] [J.HasSheafCompose (CategoryTheory.forget A)] [J.HasEnoughPoints] : J.W.IsMonoidal
• CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.isMonoidal_W 📋 Mathlib.CategoryTheory.Sites.Point.IsMonoidalW
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasProducts A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [CategoryTheory.HasWeakSheafify J A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorRight X)] [J.HasSheafCompose (CategoryTheory.forget A)] : J.W.IsMonoidal
• CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor 📋 Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] (E : CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C)) : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.CosimplicialObject A)
• CategoryTheory.cechComplexFunctor 📋 Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Preadditive A] {ι : Type w} (U : ι → C) : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CochainComplex A ℕ)
• CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor 📋 Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] (E : CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C)) [CategoryTheory.Preadditive A] : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CochainComplex A ℕ)
• CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_obj_obj 📋 Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] (E : CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C)) (X : CategoryTheory.Functor Cᵒᵖ A) (X✝ : SimplexCategory) : ((CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor E).obj X).obj X✝ = ∏ᶜ fun i => X.obj (Opposite.op ((E.obj (Opposite.op X✝)).obj i))
• CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_X 📋 Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] (E : CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C)) [CategoryTheory.Preadditive A] (X : CategoryTheory.Functor Cᵒᵖ A) (n : ℕ) : ((CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor E).obj X).X n = ∏ᶜ fun i => X.obj (Opposite.op ((E.obj (Opposite.op { len := n })).obj i))
• CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_d 📋 Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] (E : CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C)) [CategoryTheory.Preadditive A] (X : CategoryTheory.Functor Cᵒᵖ A) (i j : ℕ) : ((CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor E).obj X).d i j = CochainComplex.of.d (fun n => ∏ᶜ fun i => X.obj (Opposite.op ((E.obj (Opposite.op { len := n })).obj i))) (AlgebraicTopology.AlternatingCofaceMapComplex.objD ((CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor E).obj X)) i j
• CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_map_f 📋 Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] (E : CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C)) [CategoryTheory.Preadditive A] {X✝ Y✝ : CategoryTheory.Functor Cᵒᵖ A} (f : X✝ ⟶ Y✝) (n : ℕ) : ((CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor E).map f).f n = CategoryTheory.Limits.Pi.map fun i => f.app (Opposite.op ((E.obj (Opposite.op { len := n })).obj i))
• CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_map_app 📋 Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] (E : CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C)) {X✝ Y✝ : CategoryTheory.Functor Cᵒᵖ A} (f : X✝ ⟶ Y✝) (X : SimplexCategory) : ((CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor E).map f).app X = CategoryTheory.Limits.Pi.map fun i => f.app (Opposite.op ((E.obj (Opposite.op X)).obj i))
• CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_obj_map 📋 Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] (E : CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C)) (X : CategoryTheory.Functor Cᵒᵖ A) {X✝ Y✝ : SimplexCategory} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor E).obj X).map f = CategoryTheory.Limits.Pi.lift fun i => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun i => X.obj (Opposite.op ((E.obj (Opposite.op X✝)).obj i))) ((E.map f.op).f i)) (X.map ((E.map f.op).φ i).op)
• ωCPO.instHasProducts 📋 Mathlib.Order.Category.OmegaCompletePartialOrder
  : CategoryTheory.Limits.HasProducts ωCPO
• TopCat.Presheaf.IsSheafEqualizerProducts 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) : Prop
• TopCat.Presheaf.SheafConditionEqualizerProducts.piInters 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : C
• TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : C
• TopCat.Presheaf.isSheaf_iff_isSheafEqualizerProducts 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) : F.IsSheaf ↔ F.IsSheafEqualizerProducts
• TopCat.Presheaf.SheafConditionEqualizerProducts.diagram 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C
• TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens F U ⟶ TopCat.Presheaf.SheafConditionEqualizerProducts.piInters F U
• TopCat.Presheaf.SheafConditionEqualizerProducts.rightRes 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens F U ⟶ TopCat.Presheaf.SheafConditionEqualizerProducts.piInters F U
• TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.isoOfIso 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} {F : TopCat.Presheaf C X} {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) {G : TopCat.Presheaf C X} (α : F ≅ G) : TopCat.Presheaf.SheafConditionEqualizerProducts.piInters F U ≅ TopCat.Presheaf.SheafConditionEqualizerProducts.piInters G U
• TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.isoOfIso 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} {F : TopCat.Presheaf C X} {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) {G : TopCat.Presheaf C X} (α : F ≅ G) : TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens F U ≅ TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens G U
• TopCat.Presheaf.SheafConditionEqualizerProducts.fork 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.Limits.Fork (TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes F U) (TopCat.Presheaf.SheafConditionEqualizerProducts.rightRes F U)
• TopCat.Presheaf.SheafConditionEqualizerProducts.diagram.isoOfIso 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} {F : TopCat.Presheaf C X} {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) {G : TopCat.Presheaf C X} (α : F ≅ G) : TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U ≅ TopCat.Presheaf.SheafConditionEqualizerProducts.diagram G U
• TopCat.Presheaf.SheafConditionEqualizerProducts.res 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : F.obj (Opposite.op (iSup U)) ⟶ TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens F U
• TopCat.Presheaf.SheafConditionEqualizerProducts.fork_ι 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : (TopCat.Presheaf.SheafConditionEqualizerProducts.fork F U).ι = TopCat.Presheaf.SheafConditionEqualizerProducts.res F U
• TopCat.Presheaf.SheafConditionEqualizerProducts.fork_pt 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : (TopCat.Presheaf.SheafConditionEqualizerProducts.fork F U).pt = F.obj (Opposite.op (iSup U))
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)) : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_pt 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)) : (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj F U c).pt = c.pt
• TopCat.Presheaf.SheafConditionEqualizerProducts.fork.isoOfIso 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} {F : TopCat.Presheaf C X} {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) {G : TopCat.Presheaf C X} (α : F ≅ G) : TopCat.Presheaf.SheafConditionEqualizerProducts.fork F U ≅ (CategoryTheory.Limits.Cone.postcompose (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram.isoOfIso U α).inv).obj (TopCat.Presheaf.SheafConditionEqualizerProducts.fork G U)
• TopCat.Presheaf.SheafConditionEqualizerProducts.fork_π_app_walkingParallelPair_zero 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : (TopCat.Presheaf.SheafConditionEqualizerProducts.fork F U).π.app CategoryTheory.Limits.WalkingParallelPair.zero = TopCat.Presheaf.SheafConditionEqualizerProducts.res F U
• TopCat.Presheaf.SheafConditionEqualizerProducts.w 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.SheafConditionEqualizerProducts.res F U) (TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes F U) = CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.SheafConditionEqualizerProducts.res F U) (TopCat.Presheaf.SheafConditionEqualizerProducts.rightRes F U)
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_pt 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) : (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj F U c).pt = c.pt
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F) ≌ CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.Functor (CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) (CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U))
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.Functor (CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)) (CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F))
• TopCat.Presheaf.SheafConditionPairwiseIntersections.isLimitMapConeOfIsLimitSheafConditionFork 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (P : CategoryTheory.Limits.IsLimit (TopCat.Presheaf.SheafConditionEqualizerProducts.fork F U)) : CategoryTheory.Limits.IsLimit (CategoryTheory.Functor.mapCone F (CategoryTheory.Pairwise.cocone U).op)
• TopCat.Presheaf.SheafConditionPairwiseIntersections.isLimitSheafConditionForkOfIsLimitMapCone 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (Q : CategoryTheory.Limits.IsLimit (CategoryTheory.Functor.mapCone F (CategoryTheory.Pairwise.cocone U).op)) : CategoryTheory.Limits.IsLimit (TopCat.Presheaf.SheafConditionEqualizerProducts.fork F U)
• TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.hom_ext 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) {X✝ : C} {f f' : X✝ ⟶ TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens F U} (w : ∀ (j : CategoryTheory.Discrete ι), CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun i => F.obj (Opposite.op (U i))) j) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun i => F.obj (Opposite.op (U i))) j)) : f = f'
• TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.hom_ext_iff 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} {F : TopCat.Presheaf C X} {ι : Type v'} {U : ι → TopologicalSpace.Opens ↑X} {X✝ : C} {f f' : X✝ ⟶ TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens F U} : f = f' ↔ ∀ (j : CategoryTheory.Discrete ι), CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun i => F.obj (Opposite.op (U i))) j) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun i => F.obj (Opposite.op (U i))) j)
• TopCat.Presheaf.SheafConditionEqualizerProducts.fork_π_app_walkingParallelPair_one 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : (TopCat.Presheaf.SheafConditionEqualizerProducts.fork F U).π.app CategoryTheory.Limits.WalkingParallelPair.one = CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.SheafConditionEqualizerProducts.res F U) (TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes F U)
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U).comp (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U) ≅ CategoryTheory.Functor.id (CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U))
• TopCat.Presheaf.SheafConditionEqualizerProducts.res_π 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (i : ι) : CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.SheafConditionEqualizerProducts.res F U) (CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun i => F.obj (Opposite.op (U i))) { as := i }) = F.map (TopologicalSpace.Opens.leSupr U i).op
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_pt 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)) : ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U).obj c).pt = c.pt
• TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.hom_ext 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) {X✝ : C} {f f' : X✝ ⟶ TopCat.Presheaf.SheafConditionEqualizerProducts.piInters F U} (w : ∀ (j : CategoryTheory.Discrete (ι × ι)), CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun p => F.obj (Opposite.op (U p.1 ⊓ U p.2))) j) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun p => F.obj (Opposite.op (U p.1 ⊓ U p.2))) j)) : f = f'
• TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.hom_ext_iff 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} {F : TopCat.Presheaf C X} {ι : Type v'} {U : ι → TopologicalSpace.Opens ↑X} {X✝ : C} {f f' : X✝ ⟶ TopCat.Presheaf.SheafConditionEqualizerProducts.piInters F U} : f = f' ↔ ∀ (j : CategoryTheory.Discrete (ι × ι)), CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun p => F.obj (Opposite.op (U p.1 ⊓ U p.2))) j) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun p => F.obj (Opposite.op (U p.1 ⊓ U p.2))) j)
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_map_hom 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) {c c' : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)} (f : c ⟶ c') : ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U).map f).hom = f.hom
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_pt 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) : ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U).obj c).pt = c.pt
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_functor 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv F U).functor = TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_inverse 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv F U).inverse = TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_counitIso 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv F U).counitIso = TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso F U
• TopCat.Presheaf.SheafConditionEqualizerProducts.w_apply 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) {F✝ : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F✝] (x : carrier (F.obj (Opposite.op (iSup U)))) : (CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes F U)) ((CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.SheafConditionEqualizerProducts.res F U)) x) = (CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.SheafConditionEqualizerProducts.rightRes F U)) ((CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.SheafConditionEqualizerProducts.res F U)) x)
• TopCat.Presheaf.SheafConditionEqualizerProducts.res_π_apply 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (i : ι) {F✝ : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F✝] (x : carrier (F.obj (Opposite.op (iSup U)))) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun i => F.obj (Opposite.op (U i))) { as := i })) ((CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.SheafConditionEqualizerProducts.res F U)) x) = (CategoryTheory.ConcreteCategory.hom (F.map (TopologicalSpace.Opens.leSupr U i).op)) x
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_π_app 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)) (x : (CategoryTheory.Pairwise ι)ᵒᵖ) : ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U).obj c).π.app x = CategoryTheory.Pairwise.rec (fun a => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c) (CategoryTheory.Limits.Pi.π (fun i => F.obj (Opposite.op (U i))) a)) (fun a a_1 => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c) (CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes F U) (CategoryTheory.Limits.Pi.π (fun p => F.obj (Opposite.op (U p.1 ⊓ U p.2))) (a, a_1)))) (Opposite.unop x)
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_inv_app_hom 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (X✝ : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)) : ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso F U).inv.app X✝).hom = CategoryTheory.CategoryStruct.id X✝.pt
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_map_hom 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) {c c' : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)} (f : c ⟶ c') : ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U).map f).hom = f.hom
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_π_app 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)) (x : (CategoryTheory.Pairwise ι)ᵒᵖ) : (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj F U c).π.app x = Opposite.rec (fun x => CategoryTheory.Pairwise.casesOn x (fun i => CategoryTheory.CategoryStruct.comp (c.π.app CategoryTheory.Limits.WalkingParallelPair.zero) (CategoryTheory.Limits.Pi.π (fun i => F.obj (Opposite.op (U i))) i)) fun i j => CategoryTheory.CategoryStruct.comp (c.π.app CategoryTheory.Limits.WalkingParallelPair.one) (CategoryTheory.Limits.Pi.π (fun p => F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j))) x
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.Functor.id (CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) ≅ (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U).comp (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U)
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_π_app 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) (Z : CategoryTheory.Limits.WalkingParallelPair) : (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj F U c).π.app Z = CategoryTheory.Limits.WalkingParallelPair.casesOn Z (CategoryTheory.Limits.Pi.lift fun i => c.π.app (Opposite.op (CategoryTheory.Pairwise.single i))) (CategoryTheory.Limits.Pi.lift fun b => c.π.app (Opposite.op (CategoryTheory.Pairwise.pair b.1 b.2)))
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_hom_app_hom 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (X✝ : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)) : ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso F U).hom.app X✝).hom = CategoryTheory.CategoryStruct.id X✝.pt
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_unitIso 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv F U).unitIso = TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso F U
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_π_app 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) (Z : CategoryTheory.Limits.WalkingParallelPair) : ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U).obj c).π.app Z = CategoryTheory.Limits.WalkingParallelPair.rec (CategoryTheory.Limits.Pi.lift fun i => c.π.app (Opposite.op (CategoryTheory.Pairwise.single i))) (CategoryTheory.Limits.Pi.lift fun b => c.π.app (Opposite.op (CategoryTheory.Pairwise.pair b.1 b.2))) Z
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) : (CategoryTheory.Functor.id (CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F))).obj c ≅ ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U).comp (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U)).obj c
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_hom_hom 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) : (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp F U c).hom.hom = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F))).obj c).pt
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_hom_app_hom 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (X✝ : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) : ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso F U).hom.app X✝).hom = CategoryTheory.CategoryStruct.id X✝.pt
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_inv_app_hom 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (X✝ : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) : ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso F U).inv.app X✝).hom = CategoryTheory.CategoryStruct.id X✝.pt
• TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_inv_hom 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) : (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp F U c).inv.hom = CategoryTheory.CategoryStruct.id (((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U).comp (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U)).obj c).pt

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