Loogle!

Result

Found 105 declarations mentioning CategoryTheory.GrothendieckTopology.Point.fiber.

CategoryTheory.GrothendieckTopology.Point.fiber 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (self : J.Point) : CategoryTheory.Functor C (Type w)
CategoryTheory.GrothendieckTopology.Point.instPreservesFiniteLimitsFiber 📋 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.Limits.PreservesFiniteLimits Φ.fiber
CategoryTheory.GrothendieckTopology.Point.initiallySmall 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (self : J.Point) : CategoryTheory.InitiallySmall self.fiber.Elements
CategoryTheory.GrothendieckTopology.Point.isCofiltered 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (self : J.Point) : CategoryTheory.IsCofiltered self.fiber.Elements
CategoryTheory.GrothendieckTopology.Point.uniqueFiberObj 📋 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] (T : C) (hT : CategoryTheory.Limits.IsTerminal T) : Unique (Φ.fiber.obj T)
CategoryTheory.GrothendieckTopology.Point.isTerminalFiberObj 📋 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] (T : C) (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.Limits.IsTerminal (Φ.fiber.obj T)
CategoryTheory.GrothendieckTopology.Point.instIsSiftedOppositeElementsFiber 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) : CategoryTheory.IsSifted Φ.fiber.Elementsᵒᵖ
CategoryTheory.GrothendieckTopology.Point.instHasColimitsOfShapeOppositeElementsFiber 📋 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.HasColimitsOfShape Φ.fiber.Elementsᵒᵖ A
CategoryTheory.GrothendieckTopology.Point.subsingleton_fiber_obj 📋 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] {U T : C} (f : U ⟶ T) [CategoryTheory.Mono f] (hT : CategoryTheory.Limits.IsTerminal T) : Subsingleton (Φ.fiber.obj U)
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.instHasExactColimitsOfShapeOppositeElementsFiberOfLocallySmallOfAB5OfSizeOfHasFiniteLimits 📋 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.AB5OfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasFiniteLimits A] : CategoryTheory.HasExactColimitsOfShape Φ.fiber.Elementsᵒᵖ A
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.instPreservesColimitsOfShapeOppositeElementsFiberForget 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w'} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)] [CategoryTheory.LocallySmall.{w, v, u} C] : CategoryTheory.Limits.PreservesColimitsOfShape Φ.fiber.Elementsᵒᵖ (CategoryTheory.forget A)
CategoryTheory.GrothendieckTopology.Point.presheafFiberCocone 📋 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) : CategoryTheory.Limits.Cocone ((CategoryTheory.CategoryOfElements.π Φ.fiber).op.comp P)
CategoryTheory.GrothendieckTopology.Point.isColimitPresheafFiberCocone 📋 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) : CategoryTheory.Limits.IsColimit (Φ.presheafFiberCocone P)
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.fiber_map_injective_of_mono 📋 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] {U T : C} (f : U ⟶ T) [CategoryTheory.Mono f] : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f))
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.jointly_surjective 📋 Mathlib.CategoryTheory.Sites.Point.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (self : J.Point) {X : C} (R : CategoryTheory.Sieve X) (h : R ∈ J X) (x : self.fiber.obj X) : ∃ Y f, ∃ (_ : R.arrows f), ∃ y, (CategoryTheory.ConcreteCategory.hom (self.fiber.map f)) y = x
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_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.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.hom 📋 Mathlib.CategoryTheory.Sites.Point.Category
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {Φ₁ Φ₂ : J.Point} (self : Φ₁.Hom Φ₂) : Φ₂.fiber ⟶ Φ₁.fiber
CategoryTheory.GrothendieckTopology.Point.Hom.mk 📋 Mathlib.CategoryTheory.Sites.Point.Category
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {Φ₁ Φ₂ : J.Point} (hom : Φ₂.fiber ⟶ Φ₁.fiber) : Φ₁.Hom Φ₂
CategoryTheory.GrothendieckTopology.Point.Hom.ext 📋 Mathlib.CategoryTheory.Sites.Point.Category
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.GrothendieckTopology C} {Φ₁ Φ₂ : J.Point} {x y : Φ₁.Hom Φ₂} (hom : x.hom = y.hom) : x = y
CategoryTheory.GrothendieckTopology.Point.Hom.ext_iff 📋 Mathlib.CategoryTheory.Sites.Point.Category
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.GrothendieckTopology C} {Φ₁ Φ₂ : J.Point} {x y : Φ₁.Hom Φ₂} : x = y ↔ x.hom = y.hom
CategoryTheory.GrothendieckTopology.Point.id_hom 📋 Mathlib.CategoryTheory.Sites.Point.Category
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) : (CategoryTheory.CategoryStruct.id Φ).hom = CategoryTheory.CategoryStruct.id Φ.fiber
CategoryTheory.GrothendieckTopology.Point.hom_ext 📋 Mathlib.CategoryTheory.Sites.Point.Category
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {Φ₁ Φ₂ : J.Point} {f g : Φ₁ ⟶ Φ₂} (h : f.hom = g.hom) : f = g
CategoryTheory.GrothendieckTopology.Point.hom_ext_iff 📋 Mathlib.CategoryTheory.Sites.Point.Category
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {Φ₁ Φ₂ : J.Point} {f g : Φ₁ ⟶ Φ₂} : f = g ↔ f.hom = g.hom
CategoryTheory.GrothendieckTopology.Point.comp_hom 📋 Mathlib.CategoryTheory.Sites.Point.Category
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {Φ₁ Φ₂ Φ₃ : J.Point} (f : Φ₁ ⟶ Φ₂) (g : Φ₂ ⟶ Φ₃) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp g.hom f.hom
CategoryTheory.GrothendieckTopology.Point.comp_hom_assoc 📋 Mathlib.CategoryTheory.Sites.Point.Category
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {Φ₁ Φ₂ Φ₃ : J.Point} (f : Φ₁ ⟶ Φ₂) (g : Φ₂ ⟶ Φ₃) {Z : CategoryTheory.Functor C (Type w)} (h : Φ₁.fiber ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h = CategoryTheory.CategoryStruct.comp g.hom (CategoryTheory.CategoryStruct.comp f.hom h)
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.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.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.ObjectProperty.IsConservativeFamilyOfPoints.mk' 📋 Mathlib.CategoryTheory.Sites.Point.Conservative
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point} [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.HasSheafify J (Type w)] (hP : ∀ ⦃X : C⦄ (S : CategoryTheory.Sieve X), (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (CategoryTheory.ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) → S ∈ J X) : P.IsConservativeFamilyOfPoints
CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_ofArrows_mem 📋 Mathlib.CategoryTheory.Sites.Point.Conservative
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point} [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.HasSheafify J (Type w)] [J.WEqualsLocallyBijective (Type w)] (hP : P.IsConservativeFamilyOfPoints) {X : C} {ι : Type u_1} [Small.{w, u_1} ι] {U : ι → C} (f : (i : ι) → U i ⟶ X) : CategoryTheory.Sieve.ofArrows U f ∈ J X ↔ ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (CategoryTheory.ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_ofArrows_mem_of_small 📋 Mathlib.CategoryTheory.Sites.Point.Conservative
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point} [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.HasSheafify J (Type w)] [J.WEqualsLocallyBijective (Type w)] (hP : P.IsConservativeFamilyOfPoints) [CategoryTheory.ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P] {X : C} {ι : Type u_1} {U : ι → C} (f : (i : ι) → U i ⟶ X) : CategoryTheory.Sieve.ofArrows U f ∈ J X ↔ ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (CategoryTheory.ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
AlgebraicGeometry.Scheme.pointSmallEtale_fiber 📋 Mathlib.AlgebraicGeometry.Sites.EtalePoint
{S : AlgebraicGeometry.Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : AlgebraicGeometry.Spec (CommRingCat.of Ω) ⟶ S) : (AlgebraicGeometry.Scheme.pointSmallEtale s).fiber = (AlgebraicGeometry.Scheme.Etale.forget S).comp (CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.Over.mk s)))
AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage 📋 Mathlib.AlgebraicGeometry.Sites.EtalePoint
{S : AlgebraicGeometry.Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : AlgebraicGeometry.Spec (CommRingCat.of Ω) ⟶ S) {s₀ : ↥S} (hs₀ : s default = s₀) {X : S.Etale} (t : (AlgebraicGeometry.Scheme.pointSmallEtale s).fiber.obj X) : ↑(⇑X.hom ⁻¹' {s₀})
AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage_surjective 📋 Mathlib.AlgebraicGeometry.Sites.EtalePoint
{S : AlgebraicGeometry.Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : AlgebraicGeometry.Spec (CommRingCat.of Ω) ⟶ S) {s₀ : ↥S} (hs₀ : s default = s₀) (X : S.Etale) : Function.Surjective (AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage s hs₀)
AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage_coe 📋 Mathlib.AlgebraicGeometry.Sites.EtalePoint
{S : AlgebraicGeometry.Scheme} {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : AlgebraicGeometry.Spec (CommRingCat.of Ω) ⟶ S) {s₀ : ↥S} (hs₀ : s default = s₀) {X : S.Etale} (t : (AlgebraicGeometry.Scheme.pointSmallEtale s).fiber.obj X) : ↑(AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage s hs₀ t) = (CategoryTheory.Over.Hom.left t) default
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.comap 📋 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] : J.Point
CategoryTheory.GrothendieckTopology.Point.comap_fiber 📋 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] : (Φ.comap F hF).fiber = F.comp Φ.fiber
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.instPreservesColimitsOfShapeOppositeElementsFiberObjFunctorCurriedTensor 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.LocallySmall.{w, v, u} C] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorLeft X)] (M : A) : CategoryTheory.Limits.PreservesColimitsOfShape Φ.fiber.Elementsᵒᵖ ((CategoryTheory.MonoidalCategory.curriedTensor A).obj M)
CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfShapeOppositeElementsFiberObjFunctorFlipCurriedTensor 📋 Mathlib.CategoryTheory.Sites.Point.Monoidal
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.LocallySmall.{w, v, u} C] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorRight X)] (M : A) : CategoryTheory.Limits.PreservesColimitsOfShape Φ.fiber.Elementsᵒᵖ ((CategoryTheory.MonoidalCategory.curriedTensor A).flip.obj M)
CategoryTheory.GrothendieckTopology.Point.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.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.ofIsCofiltered_fiber 📋 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) : (CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered p hp).fiber = CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiber p
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.presheafFiberMapCocone 📋 Mathlib.CategoryTheory.Sites.Point.Map
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) : CategoryTheory.Limits.Cocone ((CategoryTheory.CategoryOfElements.π Φ.fiber).op.comp (F.op.comp P))
CategoryTheory.GrothendieckTopology.Point.isColimitPresheafFiberMapCocone 📋 Mathlib.CategoryTheory.Sites.Point.Map
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) : CategoryTheory.Limits.IsColimit (Φ.presheafFiberMapCocone F K P)
CategoryTheory.GrothendieckTopology.Point.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.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.map_aux 📋 Mathlib.CategoryTheory.Sites.Point.Map
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] ⦃X : D⦄ (R : CategoryTheory.Sieve X) (hR : R ∈ K X) ⦃u : Φ.fiber.Elements⦄ (f : ((CategoryTheory.CategoryOfElements.π Φ.fiber).comp F).obj u ⟶ X) : ∃ Y g, ∃ (_ : R.arrows g), ∃ v q a, CategoryTheory.CategoryStruct.comp a g = CategoryTheory.CategoryStruct.comp (F.map ↑q) f
CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_naturality_apply 📋 Mathlib.CategoryTheory.Sites.Point.Map
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] [CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [CategoryTheory.Category.{v'', u''} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P Q : CategoryTheory.Functor Dᵒᵖ A} (g : P ⟶ Q) (X : C) (x : Φ.fiber.obj X) {F✝ : A → A → Type uF} {carrier : A → Type w_1} {instFunLike : (X Y : A) → FunLike (F✝ X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory A F✝] (x✝ : carrier (P.obj (Opposite.op (F.obj X)))) : (CategoryTheory.ConcreteCategory.hom ((Φ.map F K).presheafFiber.map g)) ((CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiberMap F K P X x)) x✝) = (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiberMap F K Q X x)) ((CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op (F.obj X)))) x✝)
CategoryTheory.GrothendieckTopology.Point.over 📋 Mathlib.CategoryTheory.Sites.Point.Over
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.LocallySmall.{w, v, u} C] (Φ : J.Point) {X : C} (x : Φ.fiber.obj X) : (J.over X).Point
CategoryTheory.GrothendieckTopology.Point.over_fiber 📋 Mathlib.CategoryTheory.Sites.Point.Over
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.LocallySmall.{w, v, u} C] (Φ : J.Point) {X : C} (x : Φ.fiber.obj X) : (Φ.over x).fiber = CategoryTheory.FunctorToTypes.fromOverFunctor Φ.fiber x
CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.over 📋 Mathlib.CategoryTheory.Sites.Point.Over
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.LocallySmall.{w, v, u} C] {P : CategoryTheory.ObjectProperty J.Point} [CategoryTheory.ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P] [J.WEqualsLocallyBijective (Type w)] [CategoryTheory.HasSheafify J (Type w)] (hP : P.IsConservativeFamilyOfPoints) (X : C) [CategoryTheory.HasSheafify (J.over X) (Type w)] : (CategoryTheory.ObjectProperty.ofObj fun ψ => ψ.fst.obj.over ψ.snd).IsConservativeFamilyOfPoints
CategoryTheory.GrothendieckTopology.pointBot_fiber 📋 Mathlib.CategoryTheory.Sites.Point.Presheaf
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] (X : C) : (CategoryTheory.GrothendieckTopology.pointBot X).fiber = CategoryTheory.shrinkYoneda.{w, v, u}.flip.obj (Opposite.op X)
Opens.instSubsingletonObjOpensFiber 📋 Mathlib.Topology.Sheaves.Points
{X : Type u} [TopologicalSpace X] (U : TopologicalSpace.Opens X) (Φ : (Opens.grothendieckTopology X).Point) : Subsingleton (Φ.fiber.obj U)

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 ?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
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.
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