mulEquivToLimit_symm_continuous — Mathlib

English

The inverse of the limit-to-alg-equivalence map is continuous in the Krull topology.

Русский

Обратное отображение предела к эквивалентности ограничено непрерывностью в крауловской топологии.

LaTeX

$$$ Continuous\ (\text{mulEquivToLimit } k\; K)^{-1} $$$

Lean4

theorem mulEquivToLimit_symm_continuous [IsGalois k K] : Continuous (mulEquivToLimit k K).symm :=
  by
  apply continuous_of_continuousAt_one _ (continuousAt_def.mpr _)
  simp only [map_one, krullTopology_mem_nhds_one_iff_of_isGalois, ← MulEquiv.coe_toEquiv_symm,
    ← MulEquiv.toEquiv_eq_coe, ← (mulEquivToLimit k K).image_eq_preimage]
  intro H ⟨L, le⟩
  rw [mem_nhds_iff]
  use mulEquivToLimit k K '' L.1.fixingSubgroup
  simp only [isOpen_mulEquivToLimit_image_fixingSubgroup L]
  simpa [one_mem] using Set.image_subset_iff.mp (Set.image_mono le)

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