SchemeTheory.germ_sheafStalkPullbackIso_hom
Taking a germ after restriction along a continuous map is the same as applying the canonical comparison to the original germ.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace SchemeTheory
variable {X Y : TopCat.{u}}Lean source · statement
theorem germ_sheafStalkPullbackIso_hom (f : X ⟶ Y)
(F : CategoryTheory.Sheaf (Opens.grothendieckTopology Y) (Type u))
(x : X) (U : Opens Y) (hx : f x ∈ U) :
TopCat.Presheaf.germ F.obj U (f x) hx ≫ (sheafStalkPullbackIso f F x).hom =
(((TopCat.Sheaf.pullbackPushforwardAdjunction (Type u) f).unit.app F).hom.app
(op U)) ≫
TopCat.Presheaf.germ ((TopCat.Sheaf.pullback (Type u) f).obj F).obj
((Opens.map f).obj U) x hx