fix(algebraic_geometry/morphisms/universally_closed): Fix docstring. (#…

…17135)
leanprover-community · Oct 26, 2022 · a8ae1b3 · a8ae1b3
1 parent 179dcde
commit a8ae1b3
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/algebraic_geometry/morphisms/universally_closed.lean b/src/algebraic_geometry/morphisms/universally_closed.lean
@@ -31,8 +31,8 @@ open category_theory.morphism_property
 open algebraic_geometry.morphism_property (topologically)
 
 /--
-A morphism of schemes `f : X ⟶ Y` is locally of finite type if for each affine `U ⊆ Y` and
-`V ⊆ f ⁻¹' U`, The induced map `Γ(Y, U) ⟶ Γ(X, V)` is of finite type.
+A morphism of schemes `f : X ⟶ Y` is universally closed if the base change `X ×[Y] Y' ⟶ Y'`
+along any morphism `Y' ⟶ Y` is (topologically) a closed map.
 -/
 @[mk_iff]
 class universally_closed (f : X ⟶ Y) : Prop :=