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)
Following Bourbaki, Topologie Algébrique, Chapter I, § 1, def 5, a map
f : X → Ybetween topological spaces is strict if it satisfies the following equivalent conditions:rangeFactorization f : X → range fsatisfies Topology.IsQuotientMapSetoid.kerLift f : Quotient (ker f) → Ysatisfies Topology.IsEmbeddingSetoid.quotientKerEquivRange : Quotient (ker f) ≃ range fis an homeomorphismThis 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)