exist_openNormalSubgroup_sub_clopen_nhds_of_one

English

The forgetful functor to Top (or to Grp) reflects isomorphisms; an isomorphism in the underlying category implies an isomorphism upstairs.

Русский

Забывающий функтор отражает изоморфизмы: изоморфизм в базовой категории означает изоморфизм и над ProfiniteGrp.

LaTeX

$$$\text{forget}\;\mathrm{ProfiniteGrp} \text{ reflects isomorphisms}$$$

Lean4

theorem exist_openNormalSubgroup_sub_clopen_nhds_of_one {G : Type*} [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] [CompactSpace G] {W : Set G} (WClopen : IsClopen W) (einW : 1 ∈ W) :
    ∃ H : OpenNormalSubgroup G, (H : Set G) ⊆ W :=
  by
  rcases exist_openSubgroup_sub_clopen_nhds_of_one WClopen einW with ⟨H, hH⟩
  have : Subgroup.FiniteIndex H.toSubgroup := H.finiteIndex_of_finite_quotient
  use {
      toSubgroup := Subgroup.normalCore H
      isOpen' := Subgroup.isOpen_of_isClosed_of_finiteIndex _ (H.normalCore_isClosed H.isClosed) }
  exact fun _ b ↦ hH (H.normalCore_le b)

Похожие утверждения