Theorems · Definition · algebraic geometry

AlgebraicGeometry.affineLocally

({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) →
  CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme

For P a property of ring homomorphisms, affineLocally P holds for f : X ⟶ Y if for each affine open U = Spec A ⊆ Y and V = Spec B ⊆ f ⁻¹' U, the ring hom A ⟶ B satisfies P. Also see affineLocally_iff_affineOpens_le.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Cited by

13 results in Mathlib

Foundations

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