Adjunction space, a.k.a. attaching space

Stream: Is there code for X?

[Michael Rothgang]

Given two topological spaces $X$ and $Y$ and a map $f\colon A\to Y$ from a subspace $A\subset X$ to $Y$, one can form the adjunction, commonly denoted $X\cup_f Y$, as the quotient of the disjoint union $X\sqcup Y$ by the equivalence relation generated by all pairs $a \sim f(a)$.

Does mathlib have this? (It has the disjoint union and the quotient topology, so defining this wouldn't be hard. I wasn't planning to do so now, but if it exists, I would probably use it.)

[Adam Topaz]

Again, this is an example of a colimit (in this case, a pushout).

[Michael Rothgang]

I see - I should learn how to think far more categorically!

[Adam Topaz]

the general setup is this: you have three spaces $A$, $X$ and $Y$, and you look at two maps $f : A \to X$ and $g : A \to Y$. Then take the quotient of the disjoint union of $X$ and $Y$ identifying the images of $a : A$ in the copy of $X$ and $Y$.

[Adam Topaz]

your adjunction space is the special case where $f$ is the inclusion of $A$ into $X$ and $g$ is the composition of your $f$ with this inclusion.

[Michael Rothgang]

Thanks; makes perfect sense!
Is there some custom notation for the pushout (or colimits in general)? How would I write this down (or where can I look to see one example myself)?

[Adam Topaz]

import Mathlib

open CategoryTheory Limits

noncomputable
example (A X Y : TopCat) (f : A ⟶ X) (g : A ⟶ Y) : TopCat := pushout f g

[Michael Rothgang]

Wow, so short! Thanks a lot!

[Adam Topaz]

note that it's noncomputable, unfortunately. If you want something more concrete, you will likely have to make things more explicit.

[Michael Rothgang]

I certainly don't need to generate code. I'll see if I need to use anything more concrete...

[Dagur Asgeirsson]

This file claims to be about pullbacks and pushouts in TopCat. It develops some API for explicit pullback, but there is barely anything about pushouts. If you need an explicit construction of the pushout, you might want to take a look at how this is done there for the pullback and dualize.

[Michael Rothgang]

This looks exactly like what I would do, thanks a lot!