English
IsProper is a multiplicative morphism property: if f and g are IsProper, then their composition is IsProper.
Русский
IsProper является мультипликативным свойством морфизмов: если f и g являются IsProper, то их композиция IsProper.
LaTeX
$$$[IsProper(f)] \land [IsProper(g)] \Rightarrow IsProper(f ≫ g)$$$
Lean4
/-- If `f : X ⟶ Y` is universally closed and `Y` is affine,
then the map on global sections is integral. -/
theorem isIntegral_appTop_of_universallyClosed (f : X ⟶ Y) [UniversallyClosed f] [IsAffine Y] :
f.appTop.hom.IsIntegral :=
by
have : CompactSpace X := (quasiCompact_over_affine_iff f).mp inferInstance
have : UniversallyClosed (X.toSpecΓ ≫ Spec.map f.appTop) := by
rwa [← Scheme.toSpecΓ_naturality, MorphismProperty.cancel_right_of_respectsIso (P := @UniversallyClosed)]
have : UniversallyClosed X.toSpecΓ := .of_comp_of_isSeparated _ (Spec.map f.appTop)
rw [← IsIntegralHom.SpecMap_iff, IsIntegralHom.iff_universallyClosed_and_isAffineHom]
exact ⟨.of_comp_surjective X.toSpecΓ _, inferInstance⟩
