English
A morphism f is integral if and only if it is universally closed and affine as a morphism.
Русский
Отображение f интегрально тогда и только тогда, когда оно универсально замкнуто и аффинно.
LaTeX
$$IsIntegralHom f \iff (UniversallyClosed f \land IsAffineHom f)$$
Lean4
theorem iff_universallyClosed_and_isAffineHom {X Y : Scheme.{u}} {f : X ⟶ Y} :
IsIntegralHom f ↔ UniversallyClosed f ∧ IsAffineHom f :=
by
refine ⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩
clear * -
wlog hY : ∃ R, Y = Spec R
· rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsIntegralHom) Y.affineCover]
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @UniversallyClosed) Y.affineCover] at H₁
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsAffineHom) Y.affineCover] at H₂
exact fun _ ↦ this inferInstance inferInstance ⟨_, rfl⟩
obtain ⟨R, rfl⟩ := hY
wlog hX : ∃ S, X = Spec S
· have inst : IsAffine X := isAffine_of_isAffineHom f
rw [← cancel_left_of_respectsIso (P := @IsIntegralHom) X.isoSpec.inv]
exact this _ inferInstance inferInstance ⟨_, rfl⟩
obtain ⟨S, rfl⟩ := hX
obtain ⟨φ, rfl⟩ : ∃ φ, Spec.map φ = f := ⟨_, Spec.map_preimage _⟩
rw [SpecMap_iff]
apply PrimeSpectrum.isIntegral_of_isClosedMap_comap_mapRingHom
algebraize [φ.1, Polynomial.mapRingHom φ.1]
haveI : IsScalarTower R (Polynomial R) (Polynomial S) := .of_algebraMap_eq' (Polynomial.mapRingHom_comp_C _).symm
refine
H₁.out (Spec.map (CommRingCat.ofHom Polynomial.C)) (Spec.map (CommRingCat.ofHom Polynomial.C)) (Spec.map _)
(isPullback_Spec_map_isPushout _ _ _ _
(CommRingCat.isPushout_of_isPushout R S (Polynomial R) (Polynomial S))).flip
