English
Isomorphisms of schemes have the affine property: X is affine and theTop map is an isomorphism.
Русский
Изоморфизмы схем обладают афинным свойством: X аффинна, а отображение на верхнем уровне является изоморфизмом.
LaTeX
$$HasAffineProperty (isomorphisms Scheme) (fun X _ f _ => IsAffine X ∧ IsIso (f.appTop))$$
Lean4
instance : HasAffineProperty (isomorphisms Scheme) fun X _ f _ ↦ IsAffine X ∧ IsIso (f.appTop) :=
by
convert HasAffineProperty.of_isZariskiLocalAtTarget (isomorphisms Scheme) with X Y f hY
exact
⟨fun ⟨_, _⟩ ↦
(arrow_mk_iso_iff (isomorphisms _) (arrowIsoSpecΓOfIsAffine f)).mpr
(inferInstanceAs (IsIso (Spec.map (f.appTop)))),
fun (_ : IsIso f) ↦ ⟨.of_isIso f, inferInstance⟩⟩
