Theorems · Theorem · algebraic geometry

AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_apply

∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑Y.toTopCat) (x : ↑X.toTopCat)
  (hx : (CategoryTheory.ConcreteCategory.hom f.base) x ∈ U) (y : ↑(Y.presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x))
      ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.germ U ((CategoryTheory.ConcreteCategory.hom f.base) x) hx))
        y) =
    (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ ((TopologicalSpace.Opens.map f.base).obj U) x hx))
      ((CategoryTheory.ConcreteCategory.hom (f.c.app (Opposite.op U))) y)

Defined in

Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Cited by

2 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound