AlgebraicGeometry.universallyClosed_eq

theorem AlgebraicGeometry.universallyClosed_eq : @AlgebraicGeometry.UniversallyClosed = (AlgebraicGeometry.MorphismProperty.topologically @IsClosedMap).universally

The theorem `AlgebraicGeometry.universallyClosed_eq` states that a morphism in algebraic geometry is universally closed if and only if it satisfies the property of being universally a topologically closed map. In other words, a morphism `f: X ⟶ Y` in the category of algebraic geometry schemes is universally closed if for every pullback of `f` over any map `f': X' ⟶ Y'`, the underlying topological map of the pullback is a closed map, meaning that the image of any closed set `U` in `X` under this map is a closed set in `Y`.

More concisely: A morphism in algebraic geometry is universally closed if and only if the topological map induced by each pullback is closed.