Theorems · Inductive type · algebraic geometry

AlgebraicGeometry.HasAffineProperty

CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme →
  outParam AlgebraicGeometry.AffineTargetMorphismProperty → Prop

HasAffineProperty P Q is a type class asserting that P is local at the target, and over affine schemes, it is equivalent to Q : AffineTargetMorphismProperty. To make the proofs easier, we state it instead as 1. Q is local at the target 2. P f if and only if ∀ U, Q (f ∣_ U) ranging over all affine opens of the target of f. See HasAffineProperty.iff.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Basic

Cited by

30 results in Mathlib

Foundations

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