English
Integral morphisms are universally closed: they map closed sets to closed sets after any base change.
Русский
Интегральные отображения универсально замкнуты: отображают замкнутые множества в замкнутые после любого изменения базы.
LaTeX
$$UniversallyClosed IsIntegralHom$$
Lean4
instance (priority := 100) {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegralHom f] : UniversallyClosed f :=
by
revert X Y f ‹IsIntegralHom f›
rw [universallyClosed_eq, ← IsStableUnderBaseChange.universally_eq (P := @IsIntegralHom)]
apply universally_mono
intro X Y f
wlog hY : ∃ R, Y = Spec R
· rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsIntegralHom) Y.affineCover,
IsZariskiLocalAtTarget.iff_of_openCover (P := topologically _) Y.affineCover]
exact fun a i ↦ this _ ⟨_, rfl⟩ (a i)
obtain ⟨R, rfl⟩ := hY
wlog hX : ∃ S, X = Spec S
· intro H
have inst : IsAffine X := isAffine_of_isAffineHom f
rw [← cancel_left_of_respectsIso (P := topologically _) X.isoSpec.inv]
rw [← cancel_left_of_respectsIso (P := @IsIntegralHom) X.isoSpec.inv] at H
exact this _ _ ⟨_, rfl⟩ H
obtain ⟨S, rfl⟩ := hX
obtain ⟨φ, rfl⟩ := Spec.map_surjective f
rw [SpecMap_iff]
exact PrimeSpectrum.isClosedMap_comap_of_isIntegral _
