Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.ordHom_of_isUnit

∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsIntegral X]
  [inst_1 : AlgebraicGeometry.IsLocallyNoetherian X] {U : X.Opens} [inst_2 : Nonempty ↥↑U]
  {f : ↑(X.presheaf.obj (Opposite.op U))},
  IsUnit f →
    ∀ {x : ↥X} (hx : Order.coheight x = 1),
      x ∈ U →
        (AlgebraicGeometry.Scheme.ordHom x hx) ((CategoryTheory.ConcreteCategory.hom (X.germToFunctionField U)) f) = 1

Defined in

Mathlib.AlgebraicGeometry.OrderOfVanishing

Cited by

1 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsIntegralAlgebraicGeometry.IsLocallyNoetherianNonempty