Hyperplane is closed or dense

Stream: Is there code for X?

[Anatole Dedecker]

Do we know that a hyperplane is either closed or dense? @Jireh Loreaux you may know about this

[Anatole Dedecker]

(I think the hardest part would be choosing a definition for "hyperplane": using docs#is_coatom makes it trivial, but I'm going to need that for the kernel of a linear map. Do we know that submodules containing a fixed submodule are exactly preimages of submodules of the quotient? EDIT: yes, this is docs#submodule.comap_mkq.rel_iso)

[Jireh Loreaux]

Sorry. I was gone for the weekend. If we have it already then I don't know about it. Possibly related: I have an open PR (#16663) about the behavior of atoms and coatoms with respect to Galois insertions and coinsertions.