English
An auxiliary lemma: if there exists a function f on the units that is continuous on unit elements and satisfies f(u) = ↑u^{-1} for all units u, then the coercion map val: Mˣ → M is a topological embedding.
Русский
Дополнительная ламма: если существует функция f на модулях единиц, непрерывная на единицах, и удовлетворяет f(u) = ↑u^{-1} для всех единиц u, тогда отображение включения val: Mˣ → M — топологическое вложение.
LaTeX
$$$\\exists f : M \\to M\\, (ContinuousOn\\, f\\, \\{x : M\\mid IsUnit x\\})\\land (\\forall u : M^×, f(u.1) = ↑u^{-1}) \\Rightarrow IsEmbedding(\\mathrm{val} : M^× \\to M)$$$
Lean4
/-- An auxiliary lemma that can be used to prove that coercion `Mˣ → M` is a topological embedding.
Use `Units.isEmbedding_val₀`, `Units.isEmbedding_val`, or `toUnits_homeomorph` instead. -/
@[to_additive /-- An auxiliary lemma that can be used to prove that coercion `AddUnits M → M` is a
topological embedding. Use `AddUnits.isEmbedding_val` or `toAddUnits_homeomorph` instead. -/
]
theorem isEmbedding_val_mk' {M : Type*} [Monoid M] [TopologicalSpace M] {f : M → M}
(hc : ContinuousOn f {x : M | IsUnit x}) (hf : ∀ u : Mˣ, f u.1 = ↑u⁻¹) : IsEmbedding (val : Mˣ → M) :=
by
refine ⟨⟨?_⟩, val_injective⟩
rw [topology_eq_inf, inf_eq_left, ← continuous_iff_le_induced, @continuous_iff_continuousAt _ _ (.induced _ _)]
intro u s hs
simp only [← hf, nhds_induced, Filter.mem_map] at hs ⊢
exact ⟨_, mem_inf_principal.1 (hc u u.isUnit hs), fun u' hu' ↦ hu' u'.isUnit⟩
