Loogle!
Result
Found 112 declarations mentioning CategoryTheory.GrothendieckTopology.Point.presheafFiber.
- CategoryTheory.GrothendieckTopology.Point.presheafFiber 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) A - CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfSizeFunctorOppositePresheafFiber 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] : CategoryTheory.Limits.PreservesColimitsOfSize.{w, w, max u v', v', max (max (max u u') v) v', u'} Φ.presheafFiber - CategoryTheory.GrothendieckTopology.Point.instPreservesFiniteLimitsFunctorOppositePresheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.HasFiniteLimits A] [CategoryTheory.AB5OfSize.{w, w, v', u'} A] : CategoryTheory.Limits.PreservesFiniteLimits Φ.presheafFiber - CategoryTheory.GrothendieckTopology.Point.shrinkYonedaCompPresheafFiberIso 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) [CategoryTheory.LocallySmall.{w, v, u} C] : CategoryTheory.shrinkYoneda.{w, v, u}.comp Φ.presheafFiber ≅ Φ.fiber - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (X : C) (x : Φ.fiber.obj X) (P : CategoryTheory.Functor Cᵒᵖ A) : P.obj (Opposite.op X) ⟶ Φ.presheafFiber.obj P - CategoryTheory.GrothendieckTopology.Point.W_isInvertedBy_presheafFiber' 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w'} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)] [CategoryTheory.LocallySmall.{w, v, u} C] [J.WEqualsLocallyBijective A] [(CategoryTheory.forget A).ReflectsIsomorphisms] : J.W.IsInvertedBy Φ.presheafFiber - CategoryTheory.GrothendieckTopology.Point.sheafToPresheafCompPresheafFiberIso 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] : (CategoryTheory.sheafToPresheaf J A).comp Φ.presheafFiber ≅ Φ.sheafFiber - CategoryTheory.GrothendieckTopology.Point.presheafFiberCocone_pt 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (P : CategoryTheory.Functor Cᵒᵖ A) : (Φ.presheafFiberCocone P).pt = Φ.presheafFiber.obj P - CategoryTheory.GrothendieckTopology.Point.toPresheafFiberNatTrans 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (X : C) (x : Φ.fiber.obj X) : (CategoryTheory.evaluation Cᵒᵖ A).obj (Opposite.op X) ⟶ Φ.presheafFiber - CategoryTheory.GrothendieckTopology.Point.toPresheafFiberNatTrans_app 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (X : C) (x : Φ.fiber.obj X) (P : CategoryTheory.Functor Cᵒᵖ A) : (Φ.toPresheafFiberNatTrans X x).app P = Φ.toPresheafFiber X x P - CategoryTheory.GrothendieckTopology.Point.presheafFiberCompIso 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] {B : Type u''} [CategoryTheory.Category.{v'', u''} B] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} B] (F : CategoryTheory.Functor A B) [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F] : ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).comp Φ.presheafFiber ≅ Φ.presheafFiber.comp F - CategoryTheory.GrothendieckTopology.Point.presheafFiber_hom_ext 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {P : CategoryTheory.Functor Cᵒᵖ A} {T : A} {f g : Φ.presheafFiber.obj P ⟶ T} (h : ∀ (X : C) (x : Φ.fiber.obj X), CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P) f = CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P) g) : f = g - CategoryTheory.GrothendieckTopology.Point.presheafFiber_hom_ext_iff 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {Φ : J.Point} {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {P : CategoryTheory.Functor Cᵒᵖ A} {T : A} {f g : Φ.presheafFiber.obj P ⟶ T} : f = g ↔ ∀ (X : C) (x : Φ.fiber.obj X), CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P) f = CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P) g - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_naturality 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {P Q : CategoryTheory.Functor Cᵒᵖ A} (g : P ⟶ Q) (X : C) (x : Φ.fiber.obj X) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P) (Φ.presheafFiber.map g) = CategoryTheory.CategoryStruct.comp (g.app (Opposite.op X)) (Φ.toPresheafFiber X x Q) - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_w 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {X Y : C} (f : X ⟶ Y) (x : Φ.fiber.obj X) (P : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.CategoryStruct.comp (P.map f.op) (Φ.toPresheafFiber X x P) = Φ.toPresheafFiber Y ((CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f)) x) P - CategoryTheory.GrothendieckTopology.Point.presheafFiberDesc 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {P : CategoryTheory.Functor Cᵒᵖ A} {T : A} (φ : (X : C) → Φ.fiber.obj X → (P.obj (Opposite.op X) ⟶ T)) (hφ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : Φ.fiber.obj X), CategoryTheory.CategoryStruct.comp (P.map f.op) (φ X x) = φ Y ((CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f)) x) := by cat_disch) : Φ.presheafFiber.obj P ⟶ T - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_jointly_surjective 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w'} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] {P : CategoryTheory.Functor Cᵒᵖ A} [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)] [CategoryTheory.LocallySmall.{w, v, u} C] (p : CategoryTheory.ToType (Φ.presheafFiber.obj P)) : ∃ X x z, (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z = p - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_naturality_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {P Q : CategoryTheory.Functor Cᵒᵖ A} (g : P ⟶ Q) (X : C) (x : Φ.fiber.obj X) {Z : A} (h : Φ.presheafFiber.obj Q ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P) (CategoryTheory.CategoryStruct.comp (Φ.presheafFiber.map g) h) = CategoryTheory.CategoryStruct.comp (g.app (Opposite.op X)) (CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x Q) h) - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberDesc 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {P : CategoryTheory.Functor Cᵒᵖ A} {T : A} (φ : (X : C) → Φ.fiber.obj X → (P.obj (Opposite.op X) ⟶ T)) (hφ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : Φ.fiber.obj X), CategoryTheory.CategoryStruct.comp (P.map f.op) (φ X x) = φ Y ((CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f)) x) := by cat_disch) (X : C) (x : Φ.fiber.obj X) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P) (Φ.presheafFiberDesc φ hφ) = φ X x - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_w_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {X Y : C} (f : X ⟶ Y) (x : Φ.fiber.obj X) (P : CategoryTheory.Functor Cᵒᵖ A) {Z : A} (h : Φ.presheafFiber.obj P ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.map f.op) (CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P) h) = CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber Y ((CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f)) x) P) h - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberDesc_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {P : CategoryTheory.Functor Cᵒᵖ A} {T : A} (φ : (X : C) → Φ.fiber.obj X → (P.obj (Opposite.op X) ⟶ T)) (hφ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : Φ.fiber.obj X), CategoryTheory.CategoryStruct.comp (P.map f.op) (φ X x) = φ Y ((CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f)) x) := by cat_disch) (X : C) (x : Φ.fiber.obj X) {Z : A} (h : T ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P) (CategoryTheory.CategoryStruct.comp (Φ.presheafFiberDesc φ hφ) h) = CategoryTheory.CategoryStruct.comp (φ X x) h - CategoryTheory.GrothendieckTopology.Point.presheafFiberCocone_ι_app 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (P : CategoryTheory.Functor Cᵒᵖ A) (x : Φ.fiber.Elementsᵒᵖ) : (Φ.presheafFiberCocone P).ι.app x = Φ.toPresheafFiber (Opposite.unop x).fst (Opposite.unop x).snd P - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_map_injective 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w'} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] {P Q : CategoryTheory.Functor Cᵒᵖ A} [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)] [CategoryTheory.LocallySmall.{w, v, u} C] (f : P ⟶ Q) [CategoryTheory.Presheaf.IsLocallyInjective J f] : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (Φ.presheafFiber.map f)) - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_map_surjective 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w'} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] {P Q : CategoryTheory.Functor Cᵒᵖ A} [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)] [CategoryTheory.LocallySmall.{w, v, u} C] (f : P ⟶ Q) [CategoryTheory.Presheaf.IsLocallySurjective J f] : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Φ.presheafFiber.map f)) - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_map_bijective 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w'} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] {P Q : CategoryTheory.Functor Cᵒᵖ A} [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)] [CategoryTheory.LocallySmall.{w, v, u} C] (f : P ⟶ Q) [CategoryTheory.Presheaf.IsLocallyInjective J f] [CategoryTheory.Presheaf.IsLocallySurjective J f] : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom (Φ.presheafFiber.map f)) - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_jointly_surjective₂ 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w'} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] {P : CategoryTheory.Functor Cᵒᵖ A} [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)] [CategoryTheory.LocallySmall.{w, v, u} C] (p₁ p₂ : CategoryTheory.ToType (Φ.presheafFiber.obj P)) : ∃ X x z₁ z₂, (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z₁ = p₁ ∧ (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z₂ = p₂ - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberCompIso_hom_app 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] {B : Type u''} [CategoryTheory.Category.{v'', u''} B] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} B] (F : CategoryTheory.Functor A B) [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F] (X : C) (x : Φ.fiber.obj X) (P : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (P.comp F)) ((Φ.presheafFiberCompIso F).hom.app P) = F.map (Φ.toPresheafFiber X x P) - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_w_apply 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {X Y : C} (f : X ⟶ Y) (x : Φ.fiber.obj X) (P : CategoryTheory.Functor Cᵒᵖ A) {F : A → A → Type uF} {carrier : A → Type w_1} {instFunLike : (X Y : A) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory A F] (x✝ : carrier (P.obj (Opposite.op Y))) : (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x P)) ((CategoryTheory.ConcreteCategory.hom (P.map f.op)) x✝) = (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber Y ((CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f)) x) P)) x✝ - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberCompIso_hom_app_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] {B : Type u''} [CategoryTheory.Category.{v'', u''} B] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} B] (F : CategoryTheory.Functor A B) [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F] (X : C) (x : Φ.fiber.obj X) (P : CategoryTheory.Functor Cᵒᵖ A) {Z : B} (h : F.obj (Φ.presheafFiber.obj P) ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (P.comp F)) (CategoryTheory.CategoryStruct.comp ((Φ.presheafFiberCompIso F).hom.app P) h) = CategoryTheory.CategoryStruct.comp (F.map (Φ.toPresheafFiber X x P)) h - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_naturality_apply 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {P Q : CategoryTheory.Functor Cᵒᵖ A} (g : P ⟶ Q) (X : C) (x : Φ.fiber.obj X) {F : A → A → Type uF} {carrier : A → Type w_1} {instFunLike : (X Y : A) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory A F] (x✝ : carrier (P.obj (Opposite.op X))) : (CategoryTheory.ConcreteCategory.hom (Φ.presheafFiber.map g)) ((CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x P)) x✝) = (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x Q)) ((CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op X))) x✝) - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_eq_iff' 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w'} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] {P : CategoryTheory.Functor Cᵒᵖ A} [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)] [CategoryTheory.LocallySmall.{w, v, u} C] (X : C) (x : Φ.fiber.obj X) (z₁ z₂ : CategoryTheory.ToType (P.obj (Opposite.op X))) : (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z₁ = (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z₂ ↔ ∃ Y f y, (CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f)) y = x ∧ (CategoryTheory.ConcreteCategory.hom (P.map f.op)) z₁ = (CategoryTheory.ConcreteCategory.hom (P.map f.op)) z₂ - CategoryTheory.GrothendieckTopology.Point.shrinkYonedaCompPresheafFiberIso_inv_app_toPresheafFiber 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) [CategoryTheory.LocallySmall.{w, v, u} C] {X : C} (x : Φ.fiber.obj X) : (CategoryTheory.ConcreteCategory.hom (Φ.shrinkYonedaCompPresheafFiberIso.inv.app X)) x = (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x (CategoryTheory.shrinkYoneda.{w, v, u}.obj X))) (CategoryTheory.shrinkYonedaObjObjEquiv.symm (CategoryTheory.CategoryStruct.id X)) - CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso_hom_app 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] {B : Type u''} [CategoryTheory.Category.{v'', u''} B] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} B] (F : CategoryTheory.Functor A B) [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F] [J.HasSheafCompose F] (X : CategoryTheory.Sheaf J A) : (Φ.sheafFiberCompIso F).hom.app X = CategoryTheory.CategoryStruct.comp ((Φ.presheafFiberCompIso F).hom.app X.obj) (CategoryTheory.CategoryStruct.id (F.obj (Φ.presheafFiber.obj X.obj))) - CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso_inv_app 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] {B : Type u''} [CategoryTheory.Category.{v'', u''} B] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} B] (F : CategoryTheory.Functor A B) [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F] [J.HasSheafCompose F] (X : CategoryTheory.Sheaf J A) : (Φ.sheafFiberCompIso F).inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (F.obj (Φ.presheafFiber.obj X.obj))) ((Φ.presheafFiberCompIso F).inv.app X.obj) - CategoryTheory.GrothendieckTopology.Point.presheafFiber_map_shrinkYoneda_map_shrinkYonedaCompPresheafFiberIso_inv_app 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) [CategoryTheory.LocallySmall.{w, v, u} C] {X Y : C} (f : X ⟶ Y) (x : Φ.fiber.obj X) : (CategoryTheory.ConcreteCategory.hom (Φ.presheafFiber.map (CategoryTheory.shrinkYoneda.{w, v, u}.map f))) ((CategoryTheory.ConcreteCategory.hom (Φ.shrinkYonedaCompPresheafFiberIso.inv.app X)) x) = (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x (CategoryTheory.shrinkYoneda.{w, v, u}.obj Y))) (CategoryTheory.shrinkYonedaObjObjEquiv.symm f) - CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber 📋 Mathlib.CategoryTheory.Sites.Point.Category
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {Φ₁ Φ₂ : J.Point} (f : Φ₁ ⟶ Φ₂) : Φ₂.presheafFiber ⟶ Φ₁.presheafFiber - CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber_id 📋 Mathlib.CategoryTheory.Sites.Point.Category
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (Φ : J.Point) : CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber (CategoryTheory.CategoryStruct.id Φ) = CategoryTheory.CategoryStruct.id Φ.presheafFiber - CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber_comp 📋 Mathlib.CategoryTheory.Sites.Point.Category
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {Φ₁ Φ₂ Φ₃ : J.Point} (f : Φ₁ ⟶ Φ₂) (g : Φ₂ ⟶ Φ₃) : CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber g) (CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber f) - CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber_app 📋 Mathlib.CategoryTheory.Sites.Point.Category
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {Φ₁ Φ₂ : J.Point} (f : Φ₁ ⟶ Φ₂) (P : CategoryTheory.Functor Cᵒᵖ A) : (CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber f).app P = Φ₂.presheafFiberDesc (fun X x => Φ₁.toPresheafFiber X ((CategoryTheory.ConcreteCategory.hom (f.hom.app X)) x) P) ⋯ - CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber_comp_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Category
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {Φ₁ Φ₂ Φ₃ : J.Point} (f : Φ₁ ⟶ Φ₂) (g : Φ₂ ⟶ Φ₃) {Z : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) A} (h : Φ₁.presheafFiber ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber f) h) - 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.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.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.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.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.W_iff 📋 Mathlib.CategoryTheory.Sites.Point.Conservative
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)] [hJ : J.HasSheafCompose (CategoryTheory.forget A)] {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.Limits.HasProducts A] : J.W f ↔ ∀ (Φ : P.FullSubcategory), CategoryTheory.IsIso (Φ.obj.presheafFiber.map f) - CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_isLocallySurjective 📋 Mathlib.CategoryTheory.Sites.Point.Conservative
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)] [J.WEqualsLocallyBijective (Type w)] [CategoryTheory.HasSheafify J (Type w)] {X Y : CategoryTheory.Functor Cᵒᵖ A} (f : X ⟶ Y) (hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Φ.obj.presheafFiber.map f))) : CategoryTheory.Presheaf.IsLocallySurjective J f - CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso 📋 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] (P : CategoryTheory.Functor Cᵒᵖ A) : (CategoryTheory.GrothendieckTopology.IsLocalSite.point J).presheafFiber.obj P ≅ P.obj (Opposite.op (⊤_ C)) - CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberNatIso 📋 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.GrothendieckTopology.IsLocalSite.point J).presheafFiber ≅ (CategoryTheory.evaluation Cᵒᵖ A).obj (Opposite.op (⊤_ C)) - CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso_naturality 📋 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] {P P' : CategoryTheory.Functor Cᵒᵖ A} (F : P ⟶ P') : CategoryTheory.CategoryStruct.comp ((CategoryTheory.GrothendieckTopology.IsLocalSite.point J).presheafFiber.map F) (CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso J P').hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso J P).hom (F.app (Opposite.op (⊤_ C))) - CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso_naturality_assoc 📋 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] {P P' : CategoryTheory.Functor Cᵒᵖ A} (F : P ⟶ P') {Z : A} (h : P'.obj (Opposite.op (⊤_ C)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.GrothendieckTopology.IsLocalSite.point J).presheafFiber.map F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso J P').hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso J P).hom (CategoryTheory.CategoryStruct.comp (F.app (Opposite.op (⊤_ C))) h) - CategoryTheory.GrothendieckTopology.IsLocalSite.toPresheafFiber_pointPresheafFiberIso_hom 📋 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] {P : CategoryTheory.Functor Cᵒᵖ A} (X : C) (x : (CategoryTheory.GrothendieckTopology.IsLocalSite.point J).fiber.obj X) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.GrothendieckTopology.IsLocalSite.point J).toPresheafFiber X x P) (CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso J P).hom = P.map (CategoryTheory.shrinkCoyonedaObjObjEquiv x).op - CategoryTheory.GrothendieckTopology.IsLocalSite.toPresheafFiber_pointPresheafFiberIso_hom_assoc 📋 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] {P : CategoryTheory.Functor Cᵒᵖ A} (X : C) (x : (CategoryTheory.GrothendieckTopology.IsLocalSite.point J).fiber.obj X) {Z : A} (h : P.obj (Opposite.op (⊤_ C)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.GrothendieckTopology.IsLocalSite.point J).toPresheafFiber X x P) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso J P).hom h) = CategoryTheory.CategoryStruct.comp (P.map (CategoryTheory.shrinkCoyonedaObjObjEquiv x).op) h - CategoryTheory.GrothendieckTopology.Point.instOplaxMonoidalFunctorOppositePresheafFiber 📋 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] : Φ.presheafFiber.OplaxMonoidal - CategoryTheory.GrothendieckTopology.Point.instMonoidalFunctorOppositePresheafFiber 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorRight X)] : Φ.presheafFiber.Monoidal - CategoryTheory.GrothendieckTopology.Point.instIsIsoηFunctorOppositePresheafFiber 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] : CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.η Φ.presheafFiber) - CategoryTheory.GrothendieckTopology.Point.instIsIsoδFunctorOppositePresheafFiber 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorRight X)] (P₁ P₂ : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.δ Φ.presheafFiber P₁ P₂) - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_ε 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorRight X)] (X : C) (x : Φ.fiber.obj X) : CategoryTheory.Functor.LaxMonoidal.ε Φ.presheafFiber = Φ.toPresheafFiber X x (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor Cᵒᵖ A)) - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_η 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (X : C) (x : Φ.fiber.obj X) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor Cᵒᵖ A))) (CategoryTheory.Functor.OplaxMonoidal.η Φ.presheafFiber) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_η_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (X : C) (x : Φ.fiber.obj X) {Z : A} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor Cᵒᵖ A))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η Φ.presheafFiber) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)) h - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_δ 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (X : C) (x : Φ.fiber.obj X) (G₁ G₂ : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (CategoryTheory.MonoidalCategoryStruct.tensorObj G₁ G₂)) (CategoryTheory.Functor.OplaxMonoidal.δ Φ.presheafFiber G₁ G₂) = CategoryTheory.MonoidalCategoryStruct.tensorHom (Φ.toPresheafFiber X x G₁) (Φ.toPresheafFiber X x G₂) - CategoryTheory.GrothendieckTopology.Point.instIsMonoidalFunctorOppositeHomPresheafToSheafCompSheafFiberIso 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorRight X)] [J.W.IsMonoidal] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.Limits.HasProducts A] : CategoryTheory.NatTrans.IsMonoidal (Φ.presheafToSheafCompSheafFiberIso A).hom - CategoryTheory.GrothendieckTopology.Point.tensorHom_comp_toPresheafFiber_μ 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorRight X)] (X : C) (x : Φ.fiber.obj X) (G₁ G₂ : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (Φ.toPresheafFiber X x G₁) (Φ.toPresheafFiber X x G₂)) (CategoryTheory.Functor.LaxMonoidal.μ Φ.presheafFiber G₁ G₂) = Φ.toPresheafFiber X x (CategoryTheory.MonoidalCategoryStruct.tensorObj G₁ G₂) - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_δ_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (X : C) (x : Φ.fiber.obj X) (G₁ G₂ : CategoryTheory.Functor Cᵒᵖ A) {Z : A} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (Φ.presheafFiber.obj G₁) (Φ.presheafFiber.obj G₂) ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (CategoryTheory.MonoidalCategoryStruct.tensorObj G₁ G₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ Φ.presheafFiber G₁ G₂) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (Φ.toPresheafFiber X x G₁) (Φ.toPresheafFiber X x G₂)) h - CategoryTheory.GrothendieckTopology.Point.tensorHom_comp_toPresheafFiber_μ_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorRight X)] (X : C) (x : Φ.fiber.obj X) (G₁ G₂ : CategoryTheory.Functor Cᵒᵖ A) {Z : A} (h : Φ.presheafFiber.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj G₁ G₂) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (Φ.toPresheafFiber X x G₁) (Φ.toPresheafFiber X x G₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ Φ.presheafFiber G₁ G₂) h) = CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (CategoryTheory.MonoidalCategoryStruct.tensorObj G₁ G₂)) h - CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered 📋 Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {N : Type u'} [CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C) [CategoryTheory.InitiallySmall N] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.IsCofiltered N] (hp : ∀ ⦃X : C⦄, ∀ R ∈ J X, ∀ ⦃U : N⦄ (f : p.obj U ⟶ X), ∃ Y g, ∃ (_ : R.arrows g), ∃ V q a, CategoryTheory.CategoryStruct.comp a g = CategoryTheory.CategoryStruct.comp (p.map q) f) {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (U : N) (P : CategoryTheory.Functor Cᵒᵖ A) : P.obj (Opposite.op (p.obj U)) ⟶ (CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered p hp).presheafFiber.obj P - CategoryTheory.GrothendieckTopology.Point.presheafFiberOfIsCofilteredCocone_pt 📋 Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {N : Type u'} [CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C) [CategoryTheory.InitiallySmall N] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.IsCofiltered N] (hp : ∀ ⦃X : C⦄, ∀ R ∈ J X, ∀ ⦃U : N⦄ (f : p.obj U ⟶ X), ∃ Y g, ∃ (_ : R.arrows g), ∃ V q a, CategoryTheory.CategoryStruct.comp a g = CategoryTheory.CategoryStruct.comp (p.map q) f) {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Cᵒᵖ A) : (CategoryTheory.GrothendieckTopology.Point.presheafFiberOfIsCofilteredCocone p hp P).pt = (CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered p hp).presheafFiber.obj P - CategoryTheory.GrothendieckTopology.Point.presheafFiberOfIsCofilteredCocone_ι_app 📋 Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {N : Type u'} [CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C) [CategoryTheory.InitiallySmall N] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.IsCofiltered N] (hp : ∀ ⦃X : C⦄, ∀ R ∈ J X, ∀ ⦃U : N⦄ (f : p.obj U ⟶ X), ∃ Y g, ∃ (_ : R.arrows g), ∃ V q a, CategoryTheory.CategoryStruct.comp a g = CategoryTheory.CategoryStruct.comp (p.map q) f) {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Cᵒᵖ A) (U : Nᵒᵖ) : (CategoryTheory.GrothendieckTopology.Point.presheafFiberOfIsCofilteredCocone p hp P).ι.app U = CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered p hp (Opposite.unop U) P - CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered_w 📋 Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {N : Type u'} [CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C) [CategoryTheory.InitiallySmall N] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.IsCofiltered N] (hp : ∀ ⦃X : C⦄, ∀ R ∈ J X, ∀ ⦃U : N⦄ (f : p.obj U ⟶ X), ∃ Y g, ∃ (_ : R.arrows g), ∃ V q a, CategoryTheory.CategoryStruct.comp a g = CategoryTheory.CategoryStruct.comp (p.map q) f) {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {V U : N} (f : V ⟶ U) (P : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.CategoryStruct.comp (P.map (p.map f).op) (CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered p hp V P) = CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered p hp U P - CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered_w_assoc 📋 Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {N : Type u'} [CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C) [CategoryTheory.InitiallySmall N] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.IsCofiltered N] (hp : ∀ ⦃X : C⦄, ∀ R ∈ J X, ∀ ⦃U : N⦄ (f : p.obj U ⟶ X), ∃ Y g, ∃ (_ : R.arrows g), ∃ V q a, CategoryTheory.CategoryStruct.comp a g = CategoryTheory.CategoryStruct.comp (p.map q) f) {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {V U : N} (f : V ⟶ U) (P : CategoryTheory.Functor Cᵒᵖ A) {Z : A} (h : (CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered p hp).presheafFiber.obj P ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.map (p.map f).op) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered p hp V P) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered p hp U P) h - CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered_naturality 📋 Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {N : Type u'} [CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C) [CategoryTheory.InitiallySmall N] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.IsCofiltered N] (hp : ∀ ⦃X : C⦄, ∀ R ∈ J X, ∀ ⦃U : N⦄ (f : p.obj U ⟶ X), ∃ Y g, ∃ (_ : R.arrows g), ∃ V q a, CategoryTheory.CategoryStruct.comp a g = CategoryTheory.CategoryStruct.comp (p.map q) f) {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P Q : CategoryTheory.Functor Cᵒᵖ A} (g : P ⟶ Q) (U : N) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered p hp U P) ((CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered p hp).presheafFiber.map g) = CategoryTheory.CategoryStruct.comp (g.app (Opposite.op (p.obj U))) (CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered p hp U Q) - CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered_naturality_assoc 📋 Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {N : Type u'} [CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C) [CategoryTheory.InitiallySmall N] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.IsCofiltered N] (hp : ∀ ⦃X : C⦄, ∀ R ∈ J X, ∀ ⦃U : N⦄ (f : p.obj U ⟶ X), ∃ Y g, ∃ (_ : R.arrows g), ∃ V q a, CategoryTheory.CategoryStruct.comp a g = CategoryTheory.CategoryStruct.comp (p.map q) f) {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P Q : CategoryTheory.Functor Cᵒᵖ A} (g : P ⟶ Q) (U : N) {Z : A} (h : (CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered p hp).presheafFiber.obj Q ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered p hp U P) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered p hp).presheafFiber.map g) h) = CategoryTheory.CategoryStruct.comp (g.app (Opposite.op (p.obj U))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered p hp U Q) h) - CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap 📋 Mathlib.CategoryTheory.Sites.Point.Map
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) (X : C) (x : Φ.fiber.obj X) : P.obj (Opposite.op (F.obj X)) ⟶ (Φ.map F K).presheafFiber.obj P - CategoryTheory.GrothendieckTopology.Point.presheafFiberMapObjIso 📋 Mathlib.CategoryTheory.Sites.Point.Map
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) : (Φ.map F K).presheafFiber.obj P ≅ Φ.presheafFiber.obj (F.op.comp P) - CategoryTheory.GrothendieckTopology.Point.presheafFiberMapCocone_pt 📋 Mathlib.CategoryTheory.Sites.Point.Map
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) : (Φ.presheafFiberMapCocone F K P).pt = (Φ.map F K).presheafFiber.obj P - CategoryTheory.GrothendieckTopology.Point.presheafFiberMapIso 📋 Mathlib.CategoryTheory.Sites.Point.Map
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] (A : Type u'') [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] : (Φ.map F K).presheafFiber ≅ ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj F.op).comp Φ.presheafFiber - CategoryTheory.GrothendieckTopology.Point.presheafFiberMap_hom_ext 📋 Mathlib.CategoryTheory.Sites.Point.Map
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P : CategoryTheory.Functor Dᵒᵖ A} {T : A} {f g : (Φ.map F K).presheafFiber.obj P ⟶ T} (h : ∀ (X : C) (x : Φ.fiber.obj X), CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) f = CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) g) : f = g - CategoryTheory.GrothendieckTopology.Point.presheafFiberMap_hom_ext_iff 📋 Mathlib.CategoryTheory.Sites.Point.Map
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} {Φ : J.Point} {F : CategoryTheory.Functor C D} {K : CategoryTheory.GrothendieckTopology D} [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P : CategoryTheory.Functor Dᵒᵖ A} {T : A} {f g : (Φ.map F K).presheafFiber.obj P ⟶ T} : f = g ↔ ∀ (X : C) (x : Φ.fiber.obj X), CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) f = CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) g - CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_presheafFiberMapObjIso_hom 📋 Mathlib.CategoryTheory.Sites.Point.Map
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) (X : C) (x : Φ.fiber.obj X) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) (Φ.presheafFiberMapObjIso F K P).hom = Φ.toPresheafFiber X x (F.op.comp P) - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberMapObjIso_inv 📋 Mathlib.CategoryTheory.Sites.Point.Map
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) (X : C) (x : Φ.fiber.obj X) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (F.op.comp P)) (Φ.presheafFiberMapObjIso F K P).inv = Φ.toPresheafFiberMap F K P X x - CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_w 📋 Mathlib.CategoryTheory.Sites.Point.Map
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {X Y : C} (f : X ⟶ Y) (x : Φ.fiber.obj X) (P : CategoryTheory.Functor Dᵒᵖ A) : CategoryTheory.CategoryStruct.comp (P.map (F.map f).op) (Φ.toPresheafFiberMap F K P X x) = Φ.toPresheafFiberMap F K P Y ((CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f)) x) - CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_naturality 📋 Mathlib.CategoryTheory.Sites.Point.Map
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P Q : CategoryTheory.Functor Dᵒᵖ A} (g : P ⟶ Q) (X : C) (x : Φ.fiber.obj X) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) ((Φ.map F K).presheafFiber.map g) = CategoryTheory.CategoryStruct.comp (g.app (Opposite.op (F.obj X))) (Φ.toPresheafFiberMap F K Q X x) - CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_presheafFiberMapObjIso_hom_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Map
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) (X : C) (x : Φ.fiber.obj X) {Z : A} (h : Φ.presheafFiber.obj (F.op.comp P) ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) (CategoryTheory.CategoryStruct.comp (Φ.presheafFiberMapObjIso F K P).hom h) = CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (F.op.comp P)) h - CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_naturality_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Map
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P Q : CategoryTheory.Functor Dᵒᵖ A} (g : P ⟶ Q) (X : C) (x : Φ.fiber.obj X) {Z : A} (h : (Φ.map F K).presheafFiber.obj Q ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) (CategoryTheory.CategoryStruct.comp ((Φ.map F K).presheafFiber.map g) h) = CategoryTheory.CategoryStruct.comp (g.app (Opposite.op (F.obj X))) (CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K Q X x) h) - CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_w_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Map
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {X Y : C} (f : X ⟶ Y) (x : Φ.fiber.obj X) (P : CategoryTheory.Functor Dᵒᵖ A) {Z : A} (h : (Φ.map F K).presheafFiber.obj P ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.map (F.map f).op) (CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) h) = CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P Y ((CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f)) x)) h - CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberMapObjIso_inv_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Map
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) (X : C) (x : Φ.fiber.obj X) {Z : A} (h : (Φ.map F K).presheafFiber.obj P ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (F.op.comp P)) (CategoryTheory.CategoryStruct.comp (Φ.presheafFiberMapObjIso F K P).inv h) = CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) h - CategoryTheory.GrothendieckTopology.Point.presheafFiberMapCocone_ι_app 📋 Mathlib.CategoryTheory.Sites.Point.Map
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) (x : Φ.fiber.Elementsᵒᵖ) : (Φ.presheafFiberMapCocone F K P).ι.app x = Φ.toPresheafFiberMap F K P (Opposite.unop x).fst (Opposite.unop x).snd - CategoryTheory.GrothendieckTopology.Point.presheafFiberMapIso_hom_app 📋 Mathlib.CategoryTheory.Sites.Point.Map
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] (A : Type u'') [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (X : CategoryTheory.Functor Dᵒᵖ A) : (Φ.presheafFiberMapIso F K A).hom.app X = (Φ.presheafFiberMapObjIso F K X).hom - CategoryTheory.GrothendieckTopology.Point.presheafFiberMapIso_inv_app 📋 Mathlib.CategoryTheory.Sites.Point.Map
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] (A : Type u'') [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (X : CategoryTheory.Functor Dᵒᵖ A) : (Φ.presheafFiberMapIso F K A).inv.app X = (Φ.presheafFiberMapObjIso F K X).inv - CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_naturality_apply 📋 Mathlib.CategoryTheory.Sites.Point.Map
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P Q : CategoryTheory.Functor Dᵒᵖ A} (g : P ⟶ Q) (X : C) (x : Φ.fiber.obj X) {F✝ : A → A → Type uF} {carrier : A → Type w_1} {instFunLike : (X Y : A) → FunLike (F✝ X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory A F✝] (x✝ : carrier (P.obj (Opposite.op (F.obj X)))) : (CategoryTheory.ConcreteCategory.hom ((Φ.map F K).presheafFiber.map g)) ((CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiberMap F K P X x)) x✝) = (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiberMap F K Q X x)) ((CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op (F.obj X)))) x✝) - CategoryTheory.GrothendieckTopology.pointBotPresheafFiberIso 📋 Mathlib.CategoryTheory.Sites.Point.Presheaf
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] (X : C) (A : Type u_1) [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, u_2, u_1} A] : (CategoryTheory.GrothendieckTopology.pointBot X).presheafFiber ≅ (CategoryTheory.evaluation Cᵒᵖ A).obj (Opposite.op X) - CategoryTheory.GrothendieckTopology.instIsIsoFunctorOppositeToPresheafFiberNatTransPointBotCoeEquivHomUnopOpObjTypeShrinkYonedaSymmShrinkYonedaObjObjEquivId 📋 Mathlib.CategoryTheory.Sites.Point.Presheaf
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] (X : C) (A : Type u_1) [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, u_2, u_1} A] : CategoryTheory.IsIso ((CategoryTheory.GrothendieckTopology.pointBot X).toPresheafFiberNatTrans X (CategoryTheory.shrinkYonedaObjObjEquiv.symm (CategoryTheory.CategoryStruct.id X))) - CategoryTheory.GrothendieckTopology.pointBotPresheafFiberIso_inv 📋 Mathlib.CategoryTheory.Sites.Point.Presheaf
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] (X : C) (A : Type u_1) [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, u_2, u_1} A] : (CategoryTheory.GrothendieckTopology.pointBotPresheafFiberIso X A).inv = (CategoryTheory.GrothendieckTopology.pointBot X).toPresheafFiberNatTrans X (CategoryTheory.shrinkYonedaObjObjEquiv.symm (CategoryTheory.CategoryStruct.id X))
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using the Loogle command from the command palette. You can also try the
#loogle command from LeanSearchClient,
the CLI version, the Loogle
VS Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"somewhere in their lemma name.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 ?aIf 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 ?bBy 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 findtsum_lt_tsumeven though the hypothesisf i < g iis not the last.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