InfiniteGalois.normalAutEquivQuotient is continuous

Stream: Is there code for X?

[Jz Pan]

If $H$ is a closed normal subgroup of $\mathrm{Gal}(K / k)$, then $\mathrm{Gal}(K^H / k)$ should be isomorphic to $\mathrm{Gal}(K / k) ⧸ H$ as topological groups. We are missing continuity in mathlib.

[Kevin Buzzard]

You only need continuity in one direction because everything is compact Hausdorff so I would imagine it just boils down to proving that $Gal(K/k)\to Gal(K^H/K)$ is continuous.

[Jz Pan]

This works:

import Mathlib

/-- If `H` is a closed normal subgroup of `Gal(K / k)`,
then `Gal(fixedField H / k)` is isomorphic to `Gal(K / k) ⧸ H` as a topological group.

TODO: should go to mathlib -/
@[simps! toMulEquiv]
noncomputable def InfiniteGalois.normalAutContinuousEquivQuotient {k K : Type*} [Field k] [Field K]
    [Algebra k K] [IsGalois k K] (H : ClosedSubgroup Gal(K/k)) [H.Normal] :
    Gal(K/k) ⧸ H.1 ≃ₜ* Gal(IntermediateField.fixedField H.1/k) :=
  letI f : Gal(K/k) ⧸ H.1 ≃* Gal(IntermediateField.fixedField H.1/k) := normalAutEquivQuotient H
  haveI hc : Continuous f := by simpa only [(QuotientGroup.isQuotientMap_mk H.1).continuous_iff]
    using InfiniteGalois.restrictNormalHom_continuous (IntermediateField.fixedField H.1)
  letI f1 : Gal(K/k) ⧸ H.1 ≃ₜ Gal(IntermediateField.fixedField H.1/k) :=
    hc.homeoOfEquivCompactToT2 (f := f)
  { f, f1 with }