Restriction induces $\operatorname{Gal}(E/F)/H \cong \operatorname{Gal}(E^H/F)$ for normal $H$

Proved

GaloisFundamental.quotient_mulEquiv_restrict

by Lucas · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

field-theorygalois-theory

Let $E/F$ be a finite Galois extension with Galois group $G$ , and let $H$ be a normal subgroup of $G$ (so that $E^H/F$ is normal). Then restriction of automorphisms to $E^H$ induces a group isomorphism

\varphi : G/H \xrightarrow{\ \sim\ } \operatorname{Gal}(E^H/F), \qquad \varphi(\sigma H) = \sigma|_{E^H}.

(The normality of $E^H/F$ is included as a hypothesis so that the restriction map can be written down; it is equivalent to the normality of $H$ .)

Preamble

import Mathlib

Formal statement

namespace GaloisFundamental

theorem quotient_mulEquiv_restrict (F E : Type*) [Field F] [Field E] [Algebra F E]
    [FiniteDimensional F E] [IsGalois F E] (H : Subgroup (E ≃ₐ[F] E)) [H.Normal]
    [Normal F (IntermediateField.fixedField H)] :
    ∃ φ : ((E ≃ₐ[F] E) ⧸ H) ≃*
        (IntermediateField.fixedField H ≃ₐ[F] IntermediateField.fixedField H),
      ∀ σ : E ≃ₐ[F] E,
        φ (QuotientGroup.mk σ) = AlgEquiv.restrictNormalHom (IntermediateField.fixedField H) σ := by
  sorry

end GaloisFundamental

Source

Wikipedia, "Fundamental theorem of Galois theory", revision oldid=1345286594, https://en.wikipedia.org/w/index.php?title=Fundamental_theorem_of_Galois_theory&oldid=1345286594, section "Properties of the correspondence", third bullet ("In this case, the restriction of the elements of Gal(E/F) to E^H induces an isomorphism between Gal(E^H/F) and the quotient group Gal(E/F)/H")

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statement, with full knowledge of the source and of the intended meaning. It is not the blind, independent auditor read-back the platform recommends, and no reviewer should treat it as independent evidence of faithfulness. Please compare the Lean code against the source yourself (or regenerate this read-back with an independent auditor) before confirming this item.

What is fixed. Arbitrary fields $F$ , $E$ with $E$ an $F$ -algebra, $E$ finite-dimensional and Galois over $F$ ; $G$ = group of $F$ -algebra automorphisms of $E$ ; $H$ a subgroup of $G$ . Two further hypotheses: (i) $H$ is a normal subgroup of $G$ ; (ii) the fixed field $E^H$ is a normal extension of $F$ . (These two conditions are equivalent for finite Galois extensions, so assuming both is not contradictory; (ii) is needed to define restriction.)

Notation. $G/H$ is the quotient group. $\operatorname{Aut}_F(E^H)$ is the group of $F$ -algebra automorphisms of the field $E^H$ . For $\sigma \in G$ , $\operatorname{res}(\sigma) \in \operatorname{Aut}_F(E^H)$ is the restriction of $\sigma$ to $E^H$ (Mathlib's AlgEquiv.restrictNormalHom, which uses (ii) to know $\sigma(E^H) = E^H$ ).

Assertion. There exists a group isomorphism $\varphi : G/H \to \operatorname{Aut}_F(E^H)$ such that for every $\sigma \in G$ ,

\varphi(\sigma H) = \operatorname{res}(\sigma) = \sigma|_{E^H}.

So the isomorphism is required to be the one induced by restriction, not an arbitrary abstract isomorphism.

Human review

Endorsed by Shuze Chen · Sep 28, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 28, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Restriction induces Gal⁡(E/F)/H≅Gal⁡(EH/F)\operatorname{Gal}(E/F)/H \cong \operatorname{Gal}(E^H/F)Gal(E/F)/H≅Gal(EH/F) for normal HHH

Restriction induces $\operatorname{Gal}(E/F)/H \cong \operatorname{Gal}(E^H/F)$ for normal $H$