isAffineHom_of_forall_exists_isAffineOpen

English

If for every point in Y there exists an affine open neighborhood whose preimage is affine, then f is affine.

Русский

Если для каждой точки в Y существует афинное окрестности с афинным прообразом, то f аффинна.

LaTeX

$$$\\forall x: Y, \\exists U, x \\in U \\land IsAffineOpen U \\land IsAffineOpen (f^{-1}\\!U) \\Rightarrow IsAffineHom f$$$

Lean4

theorem isAffineHom_of_forall_exists_isAffineOpen
    (H : ∀ x : Y, ∃ U : Y.Opens, x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)) : IsAffineHom f :=
  by
  choose U hxU hU hfU using H
  rw [HasAffineProperty.iff_of_iSup_eq_top (P := @IsAffineHom) fun i ↦ ⟨U i, hU i⟩]
  · exact hfU
  · exact top_le_iff.mp (fun x _ ↦ by simpa using ⟨x, hxU x⟩)

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