Theorems · Theorem · general topology

coinduced_eq_induced_of_isOpenQuotientMap_of_isInducing

∀ {A : Type u_4} {B : Type u_5} {C : Type u_6} {D : Type u_7} [inst : TopologicalSpace A] [inst_1 : TopologicalSpace B]
  [inst_2 : TopologicalSpace D] (f : A → B) (g : C → D) (p : A → C) (q : B → D),
  g ∘ p = q ∘ f →
    Topology.IsInducing f →
      Function.Surjective p →
        IsOpenQuotientMap q →
          Function.Injective g →
            q ⁻¹' q '' Set.range f ⊆ Set.range f → TopologicalSpace.coinduced p inst = TopologicalSpace.induced g inst_2

Given the following diagram with f inducing, p surjective, q an open quotient map, and g injective. Suppose the image of A in B is stable under the equivalence mod q, then the coinduced topology on C (from A) coincides with the induced topology (from D). `` A -f→ B ∣ ∣ p q ↓ ↓ C -g→ D ` A typical application is when K ≤ H are subgroups of G, then the quotient topology on H/K is also the subspace topology from G/K`.

Defined in

Mathlib.Topology.Maps.OpenQuotient

Cited by

2 results in Mathlib

Foundations

Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpace