English
Let A ---f---> B and C ---g---> D be a commutative diagram with p: A → C surjective and q: B → D an open quotient map. If g is injective, the image of A in B is stable under the equivalence mod q, and the induced map via f is compatible (g ∘ p = q ∘ f), then the topology on A coinduced by p coincides with the topology on D induced by g. In particular, the quotient topology on a subgroup quotient H/K agrees with the subspace topology from G/K in the standard quotient setting.
Русский
Пусть A → B и C → D образуют диаграмму, где p : A → C сюръективна, q : B → D — открытая отношенияквартиза, g инъективна, а образ A в B стабилен по отношению к эквивалентности mod q, и g ∘ p = q ∘ f. Тогда коиндucedTopology(A) по p совпадает с индуцированной Topology(D) по g. В типичном приложении, если K ≤ H — подгруппы G, то топология на H/K как на quotient равна подпространственной топологии из G/K.
LaTeX
$$$\operatorname{coinduced}_p = \operatorname{induced}_g$$$
Lean4
/-- 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`.
-/
theorem coinduced_eq_induced_of_isOpenQuotientMap_of_isInducing (h : g ∘ p = q ∘ f) (hf : IsInducing f)
(hp : Function.Surjective p) (hq : IsOpenQuotientMap q) (hg : Function.Injective g)
(H : q ⁻¹' (q '' (Set.range f)) ⊆ Set.range f) :
‹TopologicalSpace A›.coinduced p = ‹TopologicalSpace D›.induced g :=
by
ext U
change IsOpen (p ⁻¹' U) ↔ ∃ V, _
simp_rw [hf.isOpen_iff, (Set.image_surjective.mpr hq.surjective).exists, ← hq.isQuotientMap.isOpen_preimage]
constructor
· rintro ⟨V, hV, e⟩
refine ⟨V, hq.continuous.1 _ (hq.isOpenMap _ hV), ?_⟩
ext x
obtain ⟨x, rfl⟩ := hp x
constructor
· rintro ⟨y, hy, e'⟩
obtain ⟨y, rfl⟩ := H ⟨_, ⟨x, rfl⟩, (e'.trans (congr_fun h x)).symm⟩
rw [← hg ((congr_fun h y).trans e')]
exact e.le hy
· intro H
exact ⟨f x, e.ge H, congr_fun h.symm x⟩
· rintro ⟨V, hV, rfl⟩
refine ⟨_, hV, ?_⟩
simp_rw [← Set.preimage_comp, h]
