Theorems · Theorem · algebraic geometry

AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.to_basicOpen

∀ {P : AlgebraicGeometry.AffineTargetMorphismProperty} [self : P.IsLocal] {X Y : AlgebraicGeometry.Scheme}
  [inst : AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) (r : ↑(Y.presheaf.obj (Opposite.op ⊤))),
  P f → P (f ∣_ Y.basicOpen r)

P is stable under restriction to a basic open set of global sections.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.AffineTargetMorphismProperty.IsLocalAlgebraicGeometry.IsAffine