Restricting automorphisms to a stable intermediate field

Let E be an intermediate field of L / K carried onto itself by every K-automorphism of L. Restriction is then a group homomorphism Aut(L / K) →* Aut(E / K), whose kernel is the subgroup fixing E pointwise. This is the general form of the restriction map of Galois theory, which needs no normality: stability under the automorphisms is assumed instead of derived.

Main definitions

• IntermediateField.restrictAlgEquivHom: the restriction homomorphism Aut(L / K) →* Aut(E / K) for a stable intermediate field E.

Main results

• IntermediateField.coe_restrictAlgEquivHom_apply and IntermediateField.coe_restrictAlgEquivHom_symm_apply: the restriction and its inverse act as the automorphism and its inverse do.
• IntermediateField.ker_restrictAlgEquivHom: its kernel is E.fixingSubgroup.
• IntermediateField.natCard_fixingSubgroup_of_finrank_eq_two: for a separable quadratic L / E, the fixing subgroup of E has order two.

noncomputable def IntermediateField.restrictAlgEquivHom {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L) (hE : ∀ (σ : Gal(L/K)), map (↑σ) E = E) : Gal(L/K) →* Gal(↥E/K)

Restriction to a stable intermediate field: for E carried onto itself by every K-automorphism of L, the homomorphism Aut(L / K) →* Aut(E / K) restricting an automorphism to E.

Equations

• E.restrictAlgEquivHom hE = { toFun := fun (σ : Gal(L/K)) => (E.equivMap ↑σ).trans (IntermediateField.equivOfEq ⋯), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem IntermediateField.coe_restrictAlgEquivHom_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L) (hE : ∀ (σ : Gal(L/K)), map (↑σ) E = E) (σ : Gal(L/K)) (y : ↥E) : ↑(((E.restrictAlgEquivHom hE) σ) y) = σ ↑y

The restriction of σ to E acts as σ.

@[simp]

theorem IntermediateField.coe_restrictAlgEquivHom_symm_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L) (hE : ∀ (σ : Gal(L/K)), map (↑σ) E = E) (σ : Gal(L/K)) (y : ↥E) : ↑(((E.restrictAlgEquivHom hE) σ).symm y) = σ.symm ↑y

The inverse of the restriction of σ to E acts as σ⁻¹.

theorem IntermediateField.symm_apply_algebraMap_eq_algebraMap_restrictAlgEquivHom_symm_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L) (hE : ∀ (σ : Gal(L/K)), map (↑σ) E = E) (σ : Gal(L/K)) (y : ↥E) : σ.symm ((algebraMap (↥E) L) y) = (algebraMap (↥E) L) (((E.restrictAlgEquivHom hE) σ).symm y)

Restriction commutes with inverses, read in L: σ⁻¹ carries an element of E to the image of its σ|_E⁻¹-preimage.

theorem IntermediateField.ker_restrictAlgEquivHom {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L) (hE : ∀ (σ : Gal(L/K)), map (↑σ) E = E) : (E.restrictAlgEquivHom hE).ker = E.fixingSubgroup

The kernel of restriction is the fixing subgroup: an automorphism restricts to the identity of E exactly when it fixes E pointwise.

theorem IntermediateField.natCard_fixingSubgroup_of_finrank_eq_two {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L) (hdeg : Module.finrank (↥E) L = 2) [Algebra.IsSeparable (↥E) L] : Nat.card ↥E.fixingSubgroup = 2

The fixing subgroup of a separable quadratic subextension has order two: a separable quadratic extension is Galois, with Galois group of order [L : E] = 2.