instance AlgebraicGeometry.universallyOpen_Spec_field {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec (CommRingCat.of k)) : UniversallyOpen f

If k is a field, any morphism X ⟶ Spec k is universally open.