Theorems · Theorem · algebraic geometry

AlgebraicGeometry.exists_isUnit_germ_eq

∀ (X : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsIntegral X] (f : ↑X.functionField),
  f ≠ 0 →
    ∃ U ∈ X.affineOpens,
      ∃ f', ∃ (x : Nonempty ↥↑U), (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField U)) f' = f ∧ IsUnit f'

For f an element of the function field of X, there exists some open set U ⊆ X such that f is a unit in Γ(X, U).

Defined in

Mathlib.AlgebraicGeometry.FunctionField

Cited by

0 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsIntegral