We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 3df14c1 commit a67d97bCopy full SHA for a67d97b
Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean
@@ -32,8 +32,6 @@ variable {X Y : Scheme.{u}} (f : X ⟶ Y)
32
33
open CategoryTheory.MorphismProperty
34
35
-open AlgebraicGeometry.MorphismProperty (topologically)
36
-
37
/-- A morphism of schemes `f : X ⟶ Y` is universally closed if the base change `X ×[Y] Y' ⟶ Y'`
38
along any morphism `Y' ⟶ Y` is (topologically) a closed map.
39
-/
0 commit comments