pullback with closed embedding

Stream: new members

[Vasilii Nesterov]

I have three topological spaces (in fact, compact metric spaces) $A$, $B$, $C$, with a closed embedding $f : A \to C$ and a surjective continuous function $g : B \to C$. I want to take the pullback, obtaining a space $D$ with a continuous surjection $\phi : D \to A$ and a closed embedding $\psi : D \to B$.

I've never worked with category theory in Mathlib, and I'm seeking advice on how such constructions are typically done. Should I use docs#TopCat ? Or docs#Function.Pullback ? I don't understand how to work with the former, and I don't see much topological API for the latter.

[Kenny Lau]

@Vasilii Nesterov https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.html#TopCat.pullbackIsoProdSubtype

[Andrew Yang]

I would suggest you to use docs#Function.Pullback and add the missing API. The category theory library makes things much more opaque (both literally and figuratively) without much benefit. The benefit it adds is the access to a powerful category machinery which I don't think is useful to you.