Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.algebraMap_germ_eq_germToFunctionField

∀ (X : AlgebraicGeometry.Scheme) [inst : IrreducibleSpace ↥X] {U : X.Opens} [inst_1 : Nonempty ↥↑U] {x : ↥X}
  (hx : x ∈ U) (f : ↑(X.presheaf.obj (Opposite.op U))),
  (algebraMap ↑(X.presheaf.stalk x) ↑X.functionField)
      ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx)) f) =
    (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField U)) f

Defined in

Mathlib.AlgebraicGeometry.FunctionField

Cited by

1 results in Mathlib

Foundations

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

Assumes

IrreducibleSpaceNonempty