Andrew Yang

Not really. Not every topological space (or ring) is catenary.

I think yes?

There are two notations introduced. - `x ∣_ₕ e` for `F.map e.op x` - `x ∣_ₗ V ⟪e⟫` for `F.map (hom_of_le e).op x` Are you referring to both of them?...

bors merge

Ah I forgot about that. We will probably need a custom tactic instead but this is definitely worth a try.

bors cancel Let me experiment with that a bit.

Thanks! maintainer merge

Please resolve the merge conflict. Thanks!

> It fails at `hensel` file that I didn’t touch. You should still try to fix it or else it won't come up on the queue, and the PR is...

bors merge