Loogle!

Result

Found 45 declarations mentioning TopCat.Presheaf.stalkFunctor.

• TopCat.Presheaf.stalkFunctor 📋 Mathlib.Topology.Sheaves.Stalks
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (x : ↑X) : CategoryTheory.Functor (TopCat.Presheaf C X) C
• TopCat.Presheaf.stalkFunctor_obj 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (ℱ : TopCat.Presheaf C X) (x : ↑X) : (TopCat.Presheaf.stalkFunctor C x).obj ℱ = ℱ.stalk x
• TopCat.Presheaf.stalkFunctor_preserves_mono 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] (x : ↑X) : ((TopCat.Sheaf.forget C X).comp (TopCat.Presheaf.stalkFunctor C x)).PreservesMonomorphisms
• TopCat.Presheaf.stalkSpecializes_stalkFunctor_map 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {F G : TopCat.Presheaf C X} (f : F ⟶ G) {x y : ↑X} (h : x ⤳ y) : CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h) ((TopCat.Presheaf.stalkFunctor C x).map f) = CategoryTheory.CategoryStruct.comp ((TopCat.Presheaf.stalkFunctor C y).map f) (G.stalkSpecializes h)
• TopCat.Presheaf.stalkPushforward.id 📋 Mathlib.Topology.Sheaves.Stalks
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (ℱ : TopCat.Presheaf C X) (x : ↑X) : TopCat.Presheaf.stalkPushforward C (CategoryTheory.CategoryStruct.id X) ℱ x = (TopCat.Presheaf.stalkFunctor C x).map (TopCat.Presheaf.Pushforward.id ℱ).hom
• TopCat.Presheaf.stalkSpecializes_stalkFunctor_map_assoc 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {F G : TopCat.Presheaf C X} (f : F ⟶ G) {x y : ↑X} (h : x ⤳ y) {Z : C} (h✝ : (TopCat.Presheaf.stalkFunctor C x).obj G ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h) (CategoryTheory.CategoryStruct.comp ((TopCat.Presheaf.stalkFunctor C x).map f) h✝) = CategoryTheory.CategoryStruct.comp ((TopCat.Presheaf.stalkFunctor C y).map f) (CategoryTheory.CategoryStruct.comp (G.stalkSpecializes h) h✝)
• TopCat.Presheaf.stalkFunctor_map_germ 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {F G : TopCat.Presheaf C X} (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U) (f : F ⟶ G) : CategoryTheory.CategoryStruct.comp (F.germ U x hx) ((TopCat.Presheaf.stalkFunctor C x).map f) = CategoryTheory.CategoryStruct.comp (f.app (Opposite.op U)) (G.germ U x hx)
• TopCat.Presheaf.stalkFunctor_map_germ_assoc 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {F G : TopCat.Presheaf C X} (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U) (f : F ⟶ G) {Z : C} (h : (TopCat.Presheaf.stalkFunctor C x).obj G ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.germ U x hx) (CategoryTheory.CategoryStruct.comp ((TopCat.Presheaf.stalkFunctor C x).map f) h) = CategoryTheory.CategoryStruct.comp (f.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (G.germ U x hx) h)
• TopCat.Presheaf.stalkSpecializes_stalkFunctor_map_apply 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {F G : TopCat.Presheaf C X} (f : F ⟶ G) {x y : ↑X} (h : x ⤳ y) {F✝ : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F✝] (x✝ : carrier (F.stalk y)) : (CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C x).map f)) ((CategoryTheory.ConcreteCategory.hom (F.stalkSpecializes h)) x✝) = (CategoryTheory.ConcreteCategory.hom (G.stalkSpecializes h)) ((CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C y).map f)) x✝)
• TopCat.Presheaf.isIso_of_stalkFunctor_map_iso 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {F G : TopCat.Sheaf C X} (f : F ⟶ G) [∀ (x : ↑X), CategoryTheory.IsIso ((TopCat.Presheaf.stalkFunctor C x).map f.hom)] : CategoryTheory.IsIso f
• TopCat.Presheaf.mono_of_stalk_mono 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {F G : TopCat.Sheaf C X} (f : F ⟶ G) [∀ (x : ↑X), CategoryTheory.Mono ((TopCat.Presheaf.stalkFunctor C x).map f.hom)] : CategoryTheory.Mono f
• TopCat.Presheaf.stalk_mono_of_mono 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {F G : TopCat.Sheaf C X} (f : F ⟶ G) [CategoryTheory.Mono f] (x : ↑X) : CategoryTheory.Mono ((TopCat.Presheaf.stalkFunctor C x).map f.hom)
• TopCat.Presheaf.isIso_iff_stalkFunctor_map_iso 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {F G : TopCat.Sheaf C X} (f : F ⟶ G) : CategoryTheory.IsIso f ↔ ∀ (x : ↑X), CategoryTheory.IsIso ((TopCat.Presheaf.stalkFunctor C x).map f.hom)
• TopCat.Presheaf.mono_iff_stalk_mono 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {F G : TopCat.Sheaf C X} (f : F ⟶ G) : CategoryTheory.Mono f ↔ ∀ (x : ↑X), CategoryTheory.Mono ((TopCat.Presheaf.stalkFunctor C x).map f.hom)
• TopCat.Presheaf.stalkFunctor_map_injective_of_app_injective 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] {F G : TopCat.Presheaf C X} {f : F ⟶ G} (h : ∀ (U : TopologicalSpace.Opens ↑X), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op U)))) (x : ↑X) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C x).map f))
• TopCat.Presheaf.stalkFunctor_map_injective_of_isBasis 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] {B : Set (TopologicalSpace.Opens ↑X)} (hB : TopologicalSpace.Opens.IsBasis B) {F G : TopCat.Presheaf C X} {α : F ⟶ G} (hα : ∀ U ∈ B, Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op U)))) (x : ↑X) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C x).map α))
• TopCat.Presheaf.stalkFunctor_map_germ_apply' 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {FC : C → C → Type u_1} {CC : C → Type u_2} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {F G : TopCat.Presheaf C X} (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U) (f : F ⟶ G) (s : CC (F.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C x).map f)) ((CategoryTheory.ConcreteCategory.hom (F.germ U x hx)) s) = (CategoryTheory.ConcreteCategory.hom (G.germ U x hx)) ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op U))) s)
• TopCat.Presheaf.stalkFunctor_map_germ_apply 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {FC : C → C → Type u_1} {CC : C → Type u_2} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {F G : TopCat.Presheaf C X} (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U) (f : F ⟶ G) (s : CC (F.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C x).map f)) ((CategoryTheory.ConcreteCategory.hom (F.germ U x hx)) s) = (CategoryTheory.ConcreteCategory.hom (G.germ U x hx)) ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op U))) s)
• TopCat.Presheaf.app_isIso_of_stalkFunctor_map_iso 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {F G : TopCat.Sheaf C X} (f : F ⟶ G) (U : TopologicalSpace.Opens ↑X) [∀ (x : ↥U), CategoryTheory.IsIso ((TopCat.Presheaf.stalkFunctor C ↑x).map f.hom)] : CategoryTheory.IsIso (f.hom.app (Opposite.op U))
• TopCat.Presheaf.app_injective_iff_stalkFunctor_map_injective 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {F : TopCat.Sheaf C X} {G : TopCat.Presheaf C X} (f : F.obj ⟶ G) : (∀ (x : ↑X), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C x).map f))) ↔ ∀ (U : TopologicalSpace.Opens ↑X), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op U)))
• TopCat.Presheaf.app_injective_of_stalkFunctor_map_injective 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {F : TopCat.Sheaf C X} {G : TopCat.Presheaf C X} (f : F.obj ⟶ G) (U : TopologicalSpace.Opens ↑X) (h : ∀ x ∈ U, Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C x).map f))) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op U)))
• TopCat.Presheaf.app_bijective_of_stalkFunctor_map_bijective 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {F G : TopCat.Sheaf C X} (f : F ⟶ G) (U : TopologicalSpace.Opens ↑X) (h : ∀ x ∈ U, Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C x).map f.hom))) : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op U)))
• TopCat.Presheaf.app_surjective_of_stalkFunctor_map_bijective 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {F G : TopCat.Sheaf C X} (f : F ⟶ G) (U : TopologicalSpace.Opens ↑X) (h : ∀ x ∈ U, Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C x).map f.hom))) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op U)))
• TopCat.Presheaf.app_surjective_of_injective_of_locally_surjective 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {F G : TopCat.Sheaf C X} (f : F ⟶ G) (U : TopologicalSpace.Opens ↑X) (hinj : ∀ x ∈ U, Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C x).map f.hom))) (hsurj : ∀ (t : CC (G.obj.obj (Opposite.op U))), ∀ x ∈ U, ∃ V, ∃ (_ : x ∈ V), ∃ iVU s, (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op V))) s = (CategoryTheory.ConcreteCategory.hom (G.obj.map iVU.op)) t) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op U)))
• AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp 📋 Mathlib.AlgebraicGeometry.Spec
  {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑R) : CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.StructureSheaf.toPushforwardStalk f p) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toStalk (↑R) p) ((TopCat.Presheaf.stalkFunctor CommRingCat p).map (AlgebraicGeometry.Spec.sheafedSpaceMap f).hom.c)
• AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc 📋 Mathlib.AlgebraicGeometry.Spec
  {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑R) {Z : CommRingCat} (h : ((TopCat.Presheaf.pushforward CommRingCat (AlgebraicGeometry.Spec.topMap f)).obj (AlgebraicGeometry.Spec.structureSheaf ↑S).obj).stalk p ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toPushforwardStalk f p) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toStalk (↑R) p) (CategoryTheory.CategoryStruct.comp ((TopCat.Presheaf.stalkFunctor CommRingCat p).map (AlgebraicGeometry.Spec.sheafedSpaceMap f).hom.c) h)
• AlgebraicGeometry.Scheme.Hom.stalkFunctor_toImage_injective 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f] (x : ↥(AlgebraicGeometry.Scheme.Hom.image f)) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor CommRingCat x).map (AlgebraicGeometry.Scheme.Hom.toImage f).c))
• AlgebraicGeometry.Scheme.Modules.restrictStalkNatIso 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (x : ↥X) : (AlgebraicGeometry.Scheme.Modules.restrictFunctor f).comp ((AlgebraicGeometry.Scheme.Modules.toPresheaf X).comp (TopCat.Presheaf.stalkFunctor Ab x)) ≅ (AlgebraicGeometry.Scheme.Modules.toPresheaf Y).comp (TopCat.Presheaf.stalkFunctor Ab (f x))
• AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_inv_app 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {X Y : AlgebraicGeometry.Scheme} {U : X.Opens} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (x : ↥X) (M : Y.Modules) (hxU : x ∈ U) : CategoryTheory.CategoryStruct.comp (M.presheaf.germ ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj (Opposite.unop (Opposite.op U))) (f x) ⋯) ((AlgebraicGeometry.Scheme.Modules.restrictStalkNatIso f x).inv.app M) = ((AlgebraicGeometry.Scheme.Modules.restrictFunctor f).obj M).presheaf.germ U x hxU
• AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_hom_app 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {X Y : AlgebraicGeometry.Scheme} {U : X.Opens} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (x : ↥X) (M : Y.Modules) (hxU : x ∈ U) : CategoryTheory.CategoryStruct.comp (((AlgebraicGeometry.Scheme.Modules.restrictFunctor f).obj M).presheaf.germ U x hxU) ((AlgebraicGeometry.Scheme.Modules.restrictStalkNatIso f x).hom.app M) = M.presheaf.germ ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj (Opposite.unop (Opposite.op U))) (f x) ⋯
• instIsLeftAdjointPresheafStalkFunctor 📋 Mathlib.Topology.Sheaves.Skyscraper
  {X : TopCat} (p₀ : ↑X) {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] : (TopCat.Presheaf.stalkFunctor C p₀).IsLeftAdjoint
• instIsLeftAdjointSheafCompPresheafForgetStalkFunctor 📋 Mathlib.Topology.Sheaves.Skyscraper
  {X : TopCat} (p₀ : ↑X) {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] : ((TopCat.Sheaf.forget C X).comp (TopCat.Presheaf.stalkFunctor C p₀)).IsLeftAdjoint
• skyscraperPresheafStalkAdjunction 📋 Mathlib.Topology.Sheaves.Skyscraper
  {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] : TopCat.Presheaf.stalkFunctor C p₀ ⊣ skyscraperPresheafFunctor p₀
• skyscraperSheafForgetAdjunction 📋 Mathlib.Topology.Sheaves.Skyscraper
  {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] : TopCat.Presheaf.stalkFunctor C p₀ ⊣ (skyscraperSheafFunctor p₀).comp (TopCat.Sheaf.forget C X)
• stalkSkyscraperSheafAdjunction 📋 Mathlib.Topology.Sheaves.Skyscraper
  {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] : (TopCat.Sheaf.forget C X).comp (TopCat.Presheaf.stalkFunctor C p₀) ⊣ skyscraperSheafFunctor p₀
• StalkSkyscraperPresheafAdjunctionAuxs.counit 📋 Mathlib.Topology.Sheaves.Skyscraper
  {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] : (skyscraperPresheafFunctor p₀).comp (TopCat.Presheaf.stalkFunctor C p₀) ⟶ CategoryTheory.Functor.id C
• StalkSkyscraperPresheafAdjunctionAuxs.counit_app 📋 Mathlib.Topology.Sheaves.Skyscraper
  {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] (c : C) : (StalkSkyscraperPresheafAdjunctionAuxs.counit p₀).app c = (skyscraperPresheafStalkOfSpecializes p₀ c ⋯).hom
• StalkSkyscraperPresheafAdjunctionAuxs.unit 📋 Mathlib.Topology.Sheaves.Skyscraper
  {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] : CategoryTheory.Functor.id (TopCat.Presheaf C X) ⟶ (TopCat.Presheaf.stalkFunctor C p₀).comp (skyscraperPresheafFunctor p₀)
• StalkSkyscraperPresheafAdjunctionAuxs.unit_app 📋 Mathlib.Topology.Sheaves.Skyscraper
  {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] (x✝ : TopCat.Presheaf C X) : (StalkSkyscraperPresheafAdjunctionAuxs.unit p₀).app x✝ = StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf p₀ (CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.id (TopCat.Presheaf C X)).obj x✝).stalk p₀))
• TopCat.instAdditivePresheafStalkFunctor 📋 Mathlib.Topology.Sheaves.Abelian
  {X : TopCat} (p₀ : ↑X) {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasColimits C] : (TopCat.Presheaf.stalkFunctor C p₀).Additive
• TopCat.Sheaf.instPreservesFiniteLimitsCompPresheafForgetStalkFunctor 📋 Mathlib.Topology.Sheaves.Abelian
  {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasColimits C] [CategoryTheory.Limits.HasLimits C] {FC : C → C → Type u_1} {CC : C → Type u} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [CategoryTheory.Abelian C] {X : TopCat} (p₀ : ↑X) : CategoryTheory.Limits.PreservesFiniteLimits ((TopCat.Sheaf.forget C X).comp (TopCat.Presheaf.stalkFunctor C p₀))
• TopCat.Sheaf.isZero_iff_stalkFunctor_obj_isZero 📋 Mathlib.Topology.Sheaves.Abelian
  {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasColimits C] [CategoryTheory.Limits.HasLimits C] {FC : C → C → Type u_1} {CC : C → Type u} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [CategoryTheory.Abelian C] {X : TopCat} (F : TopCat.Sheaf C X) : CategoryTheory.Limits.IsZero F ↔ ∀ (x : ↑X), CategoryTheory.Limits.IsZero (((TopCat.Sheaf.forget C X).comp (TopCat.Presheaf.stalkFunctor C x)).obj F)
• TopCat.Sheaf.exact_iff_stalkFunctor_map_exact 📋 Mathlib.Topology.Sheaves.Abelian
  {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasColimits C] [CategoryTheory.Limits.HasLimits C] {FC : C → C → Type u_1} {CC : C → Type u} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [CategoryTheory.Abelian C] {X : TopCat} (S : CategoryTheory.ShortComplex (TopCat.Sheaf C X)) : S.Exact ↔ ∀ (x : ↑X), (S.map ((TopCat.Sheaf.forget C X).comp (TopCat.Presheaf.stalkFunctor C x))).Exact
• TopCat.Presheaf.locally_surjective_iff_surjective_on_stalks 📋 Mathlib.Topology.Sheaves.LocallySurjective
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {X : TopCat} {ℱ 𝒢 : TopCat.Presheaf C X} [CategoryTheory.Limits.HasColimits C] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] (T : ℱ ⟶ 𝒢) : TopCat.Presheaf.IsLocallySurjective T ↔ ∀ (x : ↑X), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C x).map T))
• TopCat.Presheaf.stalkFunctor_map_unit_toSheafify_isIso 📋 Mathlib.Topology.Sheaves.Sheafify
  {X : TopCat} (p₀ : ↑X) (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] [CategoryTheory.Limits.HasTerminal C] (𝓕 : TopCat.Presheaf C X) [CategoryTheory.HasWeakSheafify (Opens.grothendieckTopology ↑X) C] : CategoryTheory.IsIso ((TopCat.Presheaf.stalkFunctor C p₀).map (CategoryTheory.toSheafify (Opens.grothendieckTopology ↑X) 𝓕))

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c