English
If φ is a continuous surjective group homomorphism that is a quotient map, then φ is an open quotient map (hence open map).
Русский
Если φ — непрерывный сюръективный гомоморфизм групп, являющийся квазиобразом, то он — открытое фактор-мое отображение.
LaTeX
$$$IsOpenQuotientMap \ φ$$$
Lean4
/-- Let `A` and `B` be topological groups, and let `φ : A → B` be a continuous surjective group
homomorphism. Assume furthermore that `φ` is a quotient map (i.e., `V ⊆ B`
is open iff `φ⁻¹ V` is open). Then `φ` is an open quotient map, and in particular an open map. -/
@[to_additive /-- Let `A` and `B` be topological additive groups, and let `φ : A → B` be a
continuous surjective additive group homomorphism. Assume furthermore that `φ` is a quotient map
(i.e., `V ⊆ B` is open iff `φ⁻¹ V` is open). Then `φ` is an open quotient map, and in particular an
open map. -/
]
theorem isOpenQuotientMap_of_isQuotientMap {A : Type*} [Group A] [TopologicalSpace A] [ContinuousMul A] {B : Type*}
[Group B] [TopologicalSpace B] {F : Type*} [FunLike F A B] [MonoidHomClass F A B] {φ : F} (hφ : IsQuotientMap φ) :
IsOpenQuotientMap φ where
surjective := hφ.surjective
continuous := hφ.continuous
isOpenMap := by
-- We need to check that if `U ⊆ A` is open then `φ⁻¹ (φ U)` is open.
intro U hU
rw [← hφ.isOpen_preimage]
-- It suffices to show that `φ⁻¹ (φ U) = ⋃ (U * k⁻¹)` as `k` runs through the kernel of `φ`,
-- as `U * k⁻¹` is open because `x ↦ x * k` is continuous.
-- Remark: here is where we use that we have groups not monoids (you cannot avoid
-- using both `k` and `k⁻¹` at this point).
suffices ⇑φ ⁻¹' (⇑φ '' U) = ⋃ k ∈ ker (φ : A →* B), (fun x ↦ x * k) ⁻¹' U by
exact this ▸ isOpen_biUnion (fun k _ ↦ Continuous.isOpen_preimage (by fun_prop) _ hU)
ext x
constructor
· rintro ⟨y, hyU, hyx⟩
apply Set.mem_iUnion_of_mem (x⁻¹ * y)
simp_all
· rintro ⟨_, ⟨k, rfl⟩, _, ⟨(hk : φ k = 1), rfl⟩, hx⟩
use x * k, hx
rw [map_mul, hk, mul_one]
