Structures · Geometry

AlgebraicGeometry.HasRingHomProperty

HasRingHomProperty P Q is a type class asserting that P is local at the target and the source, and for f : Spec B ⟶ Spec A, it is equivalent to the ring hom property Q. To make the proofs easier, we state it instead as 1. Q is local (See RingHom.PropertyIsLocal) 2. P f if and only if Q holds for every Γ(Y, U) ⟶ Γ(X, V) for all affine U, V. See HasRingHomProperty.iff_appLE.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Shape

2 explicit arguments · adds isLocal_ringHomProperty, eq_affineLocally'