sourceAffineLocally — Mathlib

English

Abbrev: affineLocally assigns a morphism property to scheme morphisms by checking affine opens on source and target.

Русский

Сокращение: affineLocally задает свойство морфизмов схем через проверку на аффинных открытых.

LaTeX

$$affineLocally : MorphismProperty Scheme$$

Lean4

/-- For `P` a property of ring homomorphisms, `sourceAffineLocally P` holds for `f : X ⟶ Y`
whenever `P` holds for the restriction of `f` on every affine open subset of `X`. -/
def sourceAffineLocally : AffineTargetMorphismProperty := fun X _ f _ => ∀ U : X.affineOpens, P (f.appLE ⊤ U le_top).hom

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