hasAffineProperty — Mathlib

English

On morphisms with affine target, a closed immersion is equivalent to the source being affine and the map on global sections being surjective.

Русский

Для морфизмов с аффинной целью замкнутое вложение эквивалентно тому, что источник аффинен и отображение на глобальные секции сюръективно.

LaTeX

$$$IsClosedImmersion(f) \\iff (IsAffine(X) \\land Surjective(f.appTop))$$$

Lean4

/-- On morphisms with affine target, being a closed immersion is precisely having affine source
and being surjective on global sections. -/
instance hasAffineProperty :
    HasAffineProperty @IsClosedImmersion (fun X _ f ↦ IsAffine X ∧ Function.Surjective (f.appTop)) :=
  by
  convert HasAffineProperty.of_isZariskiLocalAtTarget @IsClosedImmersion
  refine ⟨fun ⟨h₁, h₂⟩ ↦ of_surjective_of_isAffine _ h₂, by apply isAffine_surjective_of_isAffine⟩

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