English
The class of universally closed morphisms equals the intersection (infimum) of the class of morphisms whose underlying map is topologically specializing and the class of quasi-compact morphisms.
Русский
Класс универсально замкнутых морфизмов равен пересечению (meet) класса морфизмов с топологически специализирующимся отображением и класса квази-замкнутых морфизмов.
LaTeX
$$$@\AlgebraicGeometry.UniversallyClosed = (topologically @SpecializingMap).universally \; \infimum\; @AlgebraicGeometry.QuasiCompact.$$$
Lean4
theorem universallyClosed_eq_universallySpecializing :
@UniversallyClosed = (topologically @SpecializingMap).universally ⊓ @QuasiCompact :=
by
rw [← universally_eq_iff (P := @QuasiCompact).mpr inferInstance, ← universally_inf]
apply le_antisymm
· rw [← universally_eq_iff (P := @UniversallyClosed).mpr inferInstance]
exact universally_mono fun X Y f H ↦ ⟨f.isClosedMap.specializingMap, inferInstance⟩
· rw [universallyClosed_eq]
exact universally_mono fun X Y f ⟨h₁, h₂⟩ ↦ (isClosedMap_iff_specializingMap _).mpr h₁
