English
For a fixed finite Galois intermediate field L, the image of its fixing subgroup under the limit-to-alg-equiv map is an open subset in the profinite limit space.
Русский
При фиксированном конечном Галуа-подпрефиксе L образ фиксационной подгруппы через предел к алгебро-эквиваленту является открытым подмножеством в пространстве профинитного предела.
LaTeX
$$$\text{IsOpen}\; (\text{mulEquivToLimit}\; k\; K '' L.{fixingSubgroup})$$$
Lean4
theorem isOpen_mulEquivToLimit_image_fixingSubgroup [IsGalois k K] (L : FiniteGaloisIntermediateField k K) :
IsOpen (mulEquivToLimit k K '' L.fixingSubgroup) :=
by
let fix1 : Set (Π L, (asProfiniteGaloisGroupFunctor k K).obj L) := {f | f (op L) = 1}
suffices mulEquivToLimit k K '' L.1.fixingSubgroup = Set.preimage Subtype.val fix1
by
rw [this]
exact (isOpen_induced <| (continuous_apply (op L)).isOpen_preimage { 1 } trivial)
ext x
obtain ⟨σ, rfl⟩ := (mulEquivToLimit k K).surjective x
simpa using FiniteGaloisIntermediateField.mem_fixingSubgroup_iff _ _
