ClassFieldTower.Sawin.fixedField_iInf_eq_iSup_of_isClosed
Intersecting closed Galois subgroups forms the compositum of their fixed fields, without a finite-generation or normality assumption.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u v w
namespace ClassFieldTower.SawinLean source · statement
theorem fixedField_iInf_eq_iSup_of_isClosed
(F : Type u) (Ω : Type v) [Field F] [Field Ω] [Algebra F Ω] [IsGalois F Ω]
{ι : Sort w} (H : ι → Subgroup (Ω ≃ₐ[F] Ω))
(hClosed : ∀ i : ι, IsClosed (H i : Set (Ω ≃ₐ[F] Ω))) :
IntermediateField.fixedField (⨅ i : ι, H i) =
⨆ i : ι, IntermediateField.fixedField (H i)