feat(Topology): stoneCechUnit injective for T35Space #12536

Stream: PR reviews

[Johan Commelin]

I invite further reviews of

feat(Topology): stoneCechUnit injective for T35Space #12536

[Patrick Massot]

I’ll take a look.

[Patrick Massot]

I fell into a rabbit hole. The reason why this PR is so painful is because of our suboptimal Stone-Cech compactification. See a previous discussion at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/universes/near/213975002. This afternoon I spent time thinking about a way to fix this. I think I found something that works and give the general universal property, without universe restriction. But I need to take a detour because I think we don’t have the left adjoint to the inclusion of T₂ spaces into all topological spaces.

[Patrick Massot]

I hope I’ll be able to do this before the end of the week.