English
For a subgroup H and intermediate field L, the fixed field of H restricted to L is equal to the lift of the fixed field from the restriction.
Русский
Для подгруппы H и промежуточного поля L фиксированное поле H, ограниченное на L, равно возведённому фиксированному полю из ограничения.
LaTeX
$$$ \text{restrictFixedField}(H,L) = \dots $$$
Lean4
/-- 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`. -/
theorem restrict_fixedField (H : Subgroup (K ≃ₐ[k] K)) (L : IntermediateField k K) [Normal k L] :
fixedField H ⊓ L = lift (fixedField (Subgroup.map (restrictNormalHom L) H)) :=
by
apply SetLike.ext'
ext x
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· have xL := h.out.2
apply (mem_lift (⟨x, xL⟩ : L)).mpr
simp only [mem_fixedField_iff, Subgroup.mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
intro σ hσ
apply Subtype.val_injective
dsimp only
nth_rw 2 [← (h.out.1 ⟨σ, hσ⟩)]
exact AlgEquiv.restrictNormal_commutes σ L ⟨x, xL⟩
· have xL := lift_le _ h
apply(mem_lift (⟨x, xL⟩ : L)).mp at h
simp only [mem_fixedField_iff, Subgroup.mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at h
simp only [coe_inf, Set.mem_inter_iff, SetLike.mem_coe, mem_fixedField_iff, xL, and_true]
intro σ hσ
have : ((restrictNormalHom L σ) ⟨x, xL⟩).1 = x := by rw [h σ hσ]
nth_rw 2 [← this]
exact (AlgEquiv.restrictNormal_commutes σ L ⟨x, xL⟩).symm
