affineLocally — Mathlib

English

An equivalent formulation states that a morphism is affine-locally P if and only if its restriction to every affine open is P.

Русский

Эквивалентная формулировка: морфизм является affineLocally P тогда и только тогда, когда его ограничение на каждое аффинное открытое имеет свойство P.

LaTeX

$$affineLocally P ≡ ∀ U ∈ X.affineOpens, P (f|_U).hom$$

Lean4

/-- 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`. -/
abbrev affineLocally : MorphismProperty Scheme.{u} :=
  targetAffineLocally (sourceAffineLocally P)

Похожие утверждения