Theorems · Theorem · field theory

InfiniteGalois.restrict_fixedField

∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] (H : Subgroup Gal(K/k))
  (L : IntermediateField k K) [inst_3 : Normal k ↥L],
  IntermediateField.fixedField H ⊓ L =
    IntermediateField.lift (IntermediateField.fixedField (Subgroup.map (AlgEquiv.restrictNormalHom ↥L) H))

For a subgroup H of Gal(K/k), the fixed field of the image of H under the restriction to a normal intermediate field E is equal to the fixed field of H in K intersecting with E.

Defined in

Mathlib.FieldTheory.Galois.Infinite

Cited by

2 results in Mathlib

Foundations

Depth 152 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebraNormal