English
If f: M →* N is injective and an open map, then the induced map map f: Mˣ → Nˣ is open.
Русский
Если f инъективно отображает и является открытым отображением, то map f: Mˣ → Nˣ открыто.
LaTeX
$$$\\forall f : M \\to^* N,\\; (\\mathrm{Injective}\\, f) \\to (\\text{IsOpenMap} f) \\to \\text{IsOpenMap}(\\mathrm{map} f)$$$
Lean4
@[to_additive]
theorem isOpenMap_map {f : M →* N} (hf_inj : Function.Injective f) (hf : IsOpenMap f) : IsOpenMap (map f) :=
by
rintro _ ⟨U, hU, rfl⟩
have hg_openMap := hf.prodMap <| opHomeomorph.isOpenMap.comp (hf.comp opHomeomorph.symm.isOpenMap)
refine ⟨_, hg_openMap U hU, Set.ext fun y ↦ ?_⟩
simp only [embedProduct, OneHom.coe_mk, Set.mem_preimage, Set.mem_image, Prod.mk.injEq, Prod.map, Prod.exists,
MulOpposite.exists, MonoidHom.coe_mk]
refine
⟨fun ⟨a, b, h, ha, hb⟩ ↦ ⟨⟨a, b, hf_inj ?_, hf_inj ?_⟩, ?_⟩, fun ⟨x, hxV, hx⟩ ↦ ⟨x, x.inv, by simp [hxV, ← hx]⟩⟩
all_goals simp_all
