Define strict maps between topological space

[ADedecker]

Following Bourbaki, Topologie Algébrique, Chapter I, § 1, def 5, a map f : X → Y between topological spaces is strict if it satisfies the following equivalent conditions:

• the map rangeFactorization f : X → range f satisfies Topology.IsQuotientMap
• the map Setoid.kerLift f : Quotient (ker f) → Y satisfies Topology.IsEmbedding
• the map Setoid.quotientKerEquivRange : Quotient (ker f) ≃ range f is an homeomorphism

This condition is mostly important for morphisms of topological groups, and comes up quite a lot in the context of abstract functional analysis (e.g a Fredholm operator between locally convex spaces is strict)

[zw810-ctrl]

Hi @ADedecker, I would love to take a stab at this issue and formalize the TFAE for strict maps!
Before I start my local first pass, could you advise on where this definition and theorem should live? Would Mathlib.Topology.Maps be an appropriate place, or should it be in a new file like Mathlib.Topology.StrictMap?
I'll open a draft PR once I get the basic skeleton and proofs working. Let me know if anyone else is already on it!

[ADedecker]

I think the natural place would be Mathlib.Toplogy.Maps.Strict.Basic. To my knowledge no one is working on this yet!