Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Hom.germ_stalkMap

∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (x : ↥X) (hx : f x ∈ U),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.germ U (f x) hx) (AlgebraicGeometry.Scheme.Hom.stalkMap f x) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U)
      (X.presheaf.germ ((TopologicalSpace.Opens.map f.base).obj U) x hx)

Defined in

Mathlib.AlgebraicGeometry.Scheme

Cited by

10 results in Mathlib

Foundations

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