Theorems · Theorem · algebraic geometry

AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.of_basicOpenCover

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

P for f if P holds for f restricted to basic sets of a spanning set of the 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