Theorems · Theorem · algebraic geometry

AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ

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

Defined in

Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Cited by

2 results in Mathlib

Foundations

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