Theorems · Theorem · algebraic geometry

AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality

∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) {V : TopologicalSpace.Opens ↑Y.toTopCat}
  (x : ↥((TopologicalSpace.Opens.map f.base).obj V)),
  CategoryTheory.CategoryStruct.comp (Y.evaluation ⟨(CategoryTheory.ConcreteCategory.hom f.base) ↑x, ⋯⟩)
      (AlgebraicGeometry.LocallyRingedSpace.residueFieldMap f ↑x) =
    CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op V)) (X.evaluation x)

Defined in

Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Cited by

4 results in Mathlib

Foundations

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