[ScriptRaccoon]

The category LRS of locally ringed spaces (over a commutative ring) has 8 unknown properties left, as of writing. In this PR, all of them will be decided. The proofs come (more or less) from #403.

• The monomorphisms and regular epimorphisms of LRS are described (the other types of special morphisms already had descriptions).
• LRS has an extremal cogenerator (which also settles 3 related properties).
• LRS is well-powered (this is reduced to a lemma showing that the category of local commutative rings is well-copowered).
• From these results and completeness, we also deduce that LRS is cototal (which automatically implies that LRS is cocomplete, but we keep this assignment, of course).
• LRS does not have filtered-colimit-stable monomorphisms.
• LRS does not have a regular subobject classifier (and neither does Sch). The proof differs from the one in the mentioned PR, as it is more closely aligned with the recorded proof that CAlg(R) does not have a regular quotient object classifier.

As a result, LRS has no unknown properties left 🎉, and the number of unknown (category, property)-pairs decreases from 42 to 33.

Other adjustments for locally ringed spaces and schemes:

• Two redundant assignments in LRS have been removed (not cartesian closed, not concretizable). The latter has only become redundant because we now know that there is a cogenerator.
• The content page about the embedding Top → LRS has been removed. Most of the properties proven there were redundant, and the only two remaining ones (no cartesian filtered colimits, no effective cocongruences) are now proven directly on the page for LRS. The embedding is still used, but only its essential properties are established.
• The descriptions of special objects in LRS (initial object, coproduct, terminal object, product) have been expanded; the same has been done for Sch.
• The notation of objects and morphisms has been unified and made more precise: $X$ denotes a locally ringed space (or a scheme), $|X|$ its underlying topological space, and $\mathcal{O}_X$ its structure sheaf. For a morphism $f : X \to Y$, the underlying continuous map is denoted $|f| : |X| \to |Y|$. In particular, locally ringed spaces are no longer written as tuples, and their morphisms are no longer confused with their underlying continuous maps.
• Monomorphisms of schemes have been described.

The category of schemes still has several unknown properties. They will be addressed in a separate PR.

[ScriptRaccoon]

FYI @dschepler The content page about the embedding Top → LRS has been removed. Most of the properties proven there were redundant, and the only two remaining ones (no cartesian filtered colimits, no effective cocongruences) are now proven directly on the page for LRS. The embedding is still used, but only its essential properties are established.