Structures · Geometry

AlgebraicGeometry.HasAffineProperty

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

Shape

2 explicit arguments · adds isLocal_affineProperty, eq_targetAffineLocally'