English
For an intermediate field L in a Galois extension K/k, L.fixingSubgroup.carrier is open iff L is finite-dimensional over k.
Русский
Для промежуточного поля L в Галуа-расширении K/k, множество фиксирующей подгруппы открыто тогда и только тогда, когда L конечномерно над k.
LaTeX
$$$ IsOpen L.fixingSubgroup.carrier \;\iff\; FiniteDimensional_k L $$$
Lean4
theorem isOpen_iff_finite (L : IntermediateField k K) [IsGalois k K] :
IsOpen L.fixingSubgroup.carrier ↔ FiniteDimensional k L :=
by
refine ⟨fun h ↦ ?_, fun h ↦ IntermediateField.fixingSubgroup_isOpen L⟩
have : (IntermediateFieldEquivClosedSubgroup.toFun L).carrier ∈ nhds 1 := IsOpen.mem_nhds h (congrFun rfl)
rw [GroupFilterBasis.nhds_one_eq] at this
rcases this with ⟨S, ⟨gp, ⟨M, hM, eq'⟩, eq⟩, sub⟩
rw [← eq, ← eq'] at sub
have := hM.out
let L' : FiniteGaloisIntermediateField k K :=
{ normalClosure k M K with
finiteDimensional := normalClosure.is_finiteDimensional k M K
isGalois := IsGalois.normalClosure k M K }
have : L ≤ L'.1 := by
apply le_trans _ (IntermediateField.le_normalClosure M)
rw [← fixedField_fixingSubgroup M, IntermediateField.le_iff_le]
exact sub
let _ : Algebra L L'.1 := RingHom.toAlgebra (IntermediateField.inclusion this)
exact FiniteDimensional.left k L L'.1
