Post #1888488

@MartinEscardo @jonmsterling Thanks to both of you! In classical algebraic geometry, morphisms of schemes are called surjective if they are surjective on the underlying topological spaces. So for a map of spectra Spec(R) -> Spec(S) this means that prime ideals can be lifted along a ring homomorphism. A basic theorem is that morphisms induced by finite ring extensions are surjective (geometrically they correspond to some sort of finite coverings). I will try and see if localic surjectivity is a good replacement here.