Mathlib.FieldTheory.Normal.Defs

Normal structure

extends Algebra.IsAlgebraic F K

Full source

/-- Typeclass for normal field extensions: an algebraic extension of fields `K/F` is *normal*
if the minimal polynomial of every element `x` in `K` splits in `K`, i.e. every `F`-conjugate
of `x` is in `K`. -/
@[stacks 09HM]
class Normal : Prop extends Algebra.IsAlgebraic F K where
  splits' (x : K) : Splits (algebraMap F K) (minpoly F x)

Normal field extension

Informal description

A field extension $ K $ over $ F $ is called *normal* if it is algebraic and the minimal polynomial of every element $ x \in K $ splits completely in $ K $. In other words, every $ F $-conjugate of $ x $ lies in $ K $.

Normal.isIntegral theorem

(_ : Normal F K) (x : K) : IsIntegral F x

Full source

theorem Normal.isIntegral (_ : Normal F K) (x : K) : IsIntegral F x :=
  Algebra.IsIntegral.isIntegral x

Integrality of Elements in Normal Field Extensions

Informal description

Let $K$ be a normal field extension of $F$. Then every element $x \in K$ is integral over $F$.

Normal.splits theorem

(_ : Normal F K) (x : K) : Splits (algebraMap F K) (minpoly F x)

Full source

theorem Normal.splits (_ : Normal F K) (x : K) : Splits (algebraMap F K) (minpoly F x) :=
  Normal.splits' x

Splitting of Minimal Polynomials in Normal Extensions

Informal description

Let $K$ be a normal field extension of $F$. Then for every element $x \in K$, the minimal polynomial of $x$ over $F$ splits completely in $K$ via the algebra map $F \to K$.

normal_iff theorem

: Normal F K ↔ ∀ x : K, IsIntegral F x ∧ Splits (algebraMap F K) (minpoly F x)

Full source

theorem normal_iff : NormalNormal F K ↔ ∀ x : K, IsIntegral F x ∧ Splits (algebraMap F K) (minpoly F x) :=
  ⟨fun h x => ⟨h.isIntegral x, h.splits x⟩, fun h =>
    { isAlgebraic := fun x => (h x).1.isAlgebraic
      splits' := fun x => (h x).2 }⟩

Characterization of Normal Field Extensions via Integrality and Splitting

Informal description

A field extension $K$ of $F$ is normal if and only if for every element $x \in K$, $x$ is integral over $F$ and the minimal polynomial of $x$ over $F$ splits completely in $K$ via the algebra map $F \to K$.

Normal.out theorem

: Normal F K → ∀ x : K, IsIntegral F x ∧ Splits (algebraMap F K) (minpoly F x)

Full source

theorem Normal.out : Normal F K → ∀ x : K, IsIntegralIsIntegral F x ∧ Splits (algebraMap F K) (minpoly F x) :=
  normal_iff.1

Characterization of Elements in Normal Field Extensions

Informal description

If $K$ is a normal field extension of $F$, then for every element $x \in K$, $x$ is integral over $F$ and the minimal polynomial of $x$ over $F$ splits completely in $K$ via the canonical algebra map $F \to K$.

normal_self instance

: Normal F F

Full source

instance normal_self : Normal F F where
  isAlgebraic := fun _ => isIntegral_algebraMap.isAlgebraic
  splits' := fun x => (minpoly.eq_X_sub_C' x).symm ▸ splits_X_sub_C _

A Field is Normal Over Itself

Informal description

For any field $F$, the extension $F/F$ is normal. That is, the minimal polynomial of every element $x \in F$ splits completely in $F$.

Normal.tower_top_of_normal theorem

[h : Normal F E] : Normal K E

Full source

@[stacks 09HN]
theorem Normal.tower_top_of_normal [h : Normal F E] : Normal K E :=
  normal_iff.2 fun x => by
    obtain ⟨hx, hhx⟩ := h.out x
    rw [algebraMap_eq F K E] at hhx
    exact
      ⟨hx.tower_top,
        Polynomial.splits_of_splits_of_dvd (algebraMap K E)
          (Polynomial.map_ne_zero (minpoly.ne_zero hx))
          ((Polynomial.splits_map_iff (algebraMap F K) (algebraMap K E)).mpr hhx)
          (minpoly.dvd_map_of_isScalarTower F K x)⟩

Normality is preserved under field extensions in towers

Informal description

If $E$ is a normal field extension of $F$, then $E$ is also a normal field extension of any intermediate field $K$ (where $F \subseteq K \subseteq E$).

AlgHom.normal_bijective theorem

[h : Normal F E] (ϕ : E →ₐ[F] K) : Function.Bijective ϕ

Full source

theorem AlgHom.normal_bijective [h : Normal F E] (ϕ : E →ₐ[F] K) : Function.Bijective ϕ :=
  h.toIsAlgebraic.bijective_of_isScalarTower' ϕ

Bijectivity of Algebra Homomorphisms from Normal Extensions

Informal description

Let $E$ be a normal field extension of $F$. Then any $F$-algebra homomorphism $\phi \colon E \to K$ is bijective.

Normal.of_algEquiv theorem

[h : Normal F E] (f : E ≃ₐ[F] E') : Normal F E'

Full source

theorem Normal.of_algEquiv [h : Normal F E] (f : E ≃ₐ[F] E') : Normal F E' := by
  rw [normal_iff] at h ⊢
  intro x; specialize h (f.symm x)
  rw [← f.apply_symm_apply x, minpoly.algEquiv_eq, ← f.toAlgHom.comp_algebraMap]
  exact ⟨h.1.map f, splits_comp_of_splits _ _ h.2⟩

Normality of field extensions is preserved under algebra isomorphism

Informal description

Let $E$ and $E'$ be field extensions of $F$ with $E/F$ normal, and let $f \colon E \to E'$ be an $F$-algebra isomorphism. Then $E'/F$ is also normal.

AlgEquiv.transfer_normal theorem

(f : E ≃ₐ[F] E') : Normal F E ↔ Normal F E'

Full source

theorem AlgEquiv.transfer_normal (f : E ≃ₐ[F] E') : NormalNormal F E ↔ Normal F E' :=
  ⟨fun _ ↦ Normal.of_algEquiv f, fun _ ↦ Normal.of_algEquiv f.symm⟩

Normality of Field Extensions is Preserved Under Algebra Isomorphism

Informal description

Let $E$ and $E'$ be field extensions of $F$, and let $f \colon E \to E'$ be an $F$-algebra isomorphism. Then $E/F$ is normal if and only if $E'/F$ is normal.

IntermediateField.restrictScalars_normal theorem

{E : IntermediateField K L} : Normal F (E.restrictScalars F) ↔ Normal F E

Full source

@[simp]
theorem restrictScalars_normal {E : IntermediateField K L} :
    NormalNormal F (E.restrictScalars F) ↔ Normal F E :=
  Iff.rfl

Normality is preserved under restriction of scalars for intermediate fields

Informal description

For any intermediate field $E$ between $K$ and $L$, the field extension $E$ over $F$ is normal if and only if the restriction of scalars of $E$ to $F$ is normal. In other words, $E/F$ is normal precisely when $(E \text{ viewed as an } F\text{-extension})/F$ is normal.

AlgHom.restrictNormalAux definition

[h : Normal F E] : (toAlgHom F E K₁).range →ₐ[F] (toAlgHom F E K₂).range

Full source

/-- Restrict algebra homomorphism to image of normal subfield -/
def AlgHom.restrictNormalAux [h : Normal F E] :
    (toAlgHom F E K₁).range →ₐ[F] (toAlgHom F E K₂).range where
  toFun x :=
    ⟨ϕ x, by
      suffices (toAlgHom F E K₁).range.map ϕ ≤ _ by exact this ⟨x, Subtype.mem x, rfl⟩
      rintro x ⟨y, ⟨z, hy⟩, hx⟩
      rw [← hx, ← hy]
      apply minpoly.mem_range_of_degree_eq_one E
      refine
        Or.resolve_left (h.splits z).def (minpoly.ne_zero (h.isIntegral z)) (minpoly.irreducible ?_)
          (minpoly.dvd E _ (by simp [aeval_algHom_apply]))
      simp only [AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom]
      suffices IsIntegral F _ by exact this.tower_top
      exact ((h.isIntegral z).map <| toAlgHom F E K₁).map ϕ⟩
  map_zero' := Subtype.ext (map_zero _)
  map_one' := Subtype.ext (map_one _)
  map_add' x y := Subtype.ext <| by simp
  map_mul' x y := Subtype.ext <| by simp
  commutes' x := Subtype.ext (ϕ.commutes x)

Restriction of Algebra Homomorphism to Normal Extension Image

Informal description

Given a normal field extension $ E $ over $ F $, and two field extensions $ K_1 $ and $ K_2 $ of $ E $, the function `AlgHom.restrictNormalAux` restricts an algebra homomorphism $ \phi : K_1 \to K_2 $ to the image of $ E $ in $ K_1 $, yielding an algebra homomorphism from the image of $ E $ in $ K_1 $ to the image of $ E $ in $ K_2 $. This restriction is well-defined because the minimal polynomial of any element in $ E $ splits completely in $ E $ (due to the normality condition), ensuring that the image under $ \phi $ remains within the image of $ E $ in $ K_2 $.

AlgHom.restrictNormal definition

[Normal F E] : E →ₐ[F] E

Full source

/-- Restrict algebra homomorphism to normal subfield. -/
@[stacks 0BME "Part 1"]
def AlgHom.restrictNormal [Normal F E] : E →ₐ[F] E :=
  ((AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K₂)).symm.toAlgHom.comp
        (ϕ.restrictNormalAux E)).comp
    (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K₁)).toAlgHom

Restriction of algebra homomorphism to normal field extension

Informal description

Given a normal field extension $ E $ over $ F $, and an algebra homomorphism $ \phi $ between two field extensions $ K_1 $ and $ K_2 $ of $ E $, the function `AlgHom.restrictNormal` restricts $ \phi $ to an algebra homomorphism from $ E $ to itself. This restriction is constructed by composing $ \phi $ with canonical algebra homomorphisms induced by the embeddings of $ E $ into $ K_1 $ and $ K_2 $, ensuring that the result is an endomorphism of $ E $.

AlgHom.restrictNormal' definition

[Normal F E] : E ≃ₐ[F] E

Full source

/-- Restrict algebra homomorphism to normal subfield (`AlgEquiv` version) -/
def AlgHom.restrictNormal' [Normal F E] : E ≃ₐ[F] E :=
  AlgEquiv.ofBijective (AlgHom.restrictNormal ϕ E) (AlgHom.normal_bijective F E E _)

Restriction of algebra homomorphism to normal field extension as automorphism

Informal description

Given a normal field extension $ E $ over $ F $, and an algebra homomorphism $ \phi $ between two field extensions $ K_1 $ and $ K_2 $ of $ E $, the function `AlgHom.restrictNormal'` restricts $ \phi $ to an algebra automorphism of $ E $. This is constructed by showing that the restriction `AlgHom.restrictNormal ϕ E` is bijective, yielding an algebra equivalence between $ E $ and itself.

AlgHom.restrictNormal_commutes theorem

[Normal F E] (x : E) : algebraMap E K₂ (ϕ.restrictNormal E x) = ϕ (algebraMap E K₁ x)

Full source

@[simp]
theorem AlgHom.restrictNormal_commutes [Normal F E] (x : E) :
    algebraMap E K₂ (ϕ.restrictNormal E x) = ϕ (algebraMap E K₁ x) :=
  Subtype.ext_iff.mp
    (AlgEquiv.apply_symm_apply (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K₂))
      (ϕ.restrictNormalAux E ⟨IsScalarTower.toAlgHom F E K₁ x, x, rfl⟩))

Commutation of Restricted Algebra Homomorphism with Inclusions in Normal Extension

Informal description

Let $E$ be a normal field extension of $F$, and let $\phi \colon K_1 \to K_2$ be an algebra homomorphism between field extensions $K_1$ and $K_2$ of $E$. For any $x \in E$, the following diagram commutes: \[ \begin{tikzcd} E \arrow{r}{\phi|_E} \arrow{d}[swap]{\iota_1} & E \arrow{d}{\iota_2} \\ K_1 \arrow{r}[swap]{\phi} & K_2 \end{tikzcd} \] where $\phi|_E$ denotes the restriction of $\phi$ to $E$, and $\iota_1 \colon E \hookrightarrow K_1$, $\iota_2 \colon E \hookrightarrow K_2$ are the canonical inclusion maps. In other words, $\iota_2(\phi|_E(x)) = \phi(\iota_1(x))$ for all $x \in E$.

AlgHom.restrictNormal_comp theorem

[Normal F E] : (ψ.restrictNormal E).comp (ϕ.restrictNormal E) = (ψ.comp ϕ).restrictNormal E

Full source

theorem AlgHom.restrictNormal_comp [Normal F E] :
    (ψ.restrictNormal E).comp (ϕ.restrictNormal E) = (ψ.comp ϕ).restrictNormal E :=
  AlgHom.ext fun _ =>
    (algebraMap E K₃).injective (by simp only [AlgHom.comp_apply, AlgHom.restrictNormal_commutes])

Composition of Restricted Algebra Homomorphisms on Normal Extension

Informal description

Let $E$ be a normal field extension of $F$, and let $\phi \colon K_1 \to K_2$ and $\psi \colon K_2 \to K_3$ be algebra homomorphisms between field extensions $K_1$, $K_2$, and $K_3$ of $E$. Then the composition of the restricted homomorphisms $\psi|_E \circ \phi|_E$ equals the restriction of the composition $\psi \circ \phi$ to $E$, i.e., \[ (\psi|_E) \circ (\phi|_E) = (\psi \circ \phi)|_E. \]

AlgEquiv.restrictNormal definition

[Normal F E] : E ≃ₐ[F] E

Full source

/-- Restrict algebra isomorphism to a normal subfield -/
def AlgEquiv.restrictNormal [Normal F E] : E ≃ₐ[F] E :=
  AlgHom.restrictNormal' χ.toAlgHom E

Restriction of algebra equivalence to normal field extension as automorphism

Informal description

Given a normal field extension $ E $ over $ F $, the function `AlgEquiv.restrictNormal` restricts an algebra equivalence $ \chi $ between field extensions $ K_1 $ and $ K_2 $ of $ E $ to an algebra automorphism of $ E $. This is constructed by restricting the underlying algebra homomorphism of $ \chi $ to $ E $, yielding an algebra equivalence between $ E $ and itself.

AlgEquiv.restrictNormal_commutes theorem

[Normal F E] (x : E) : algebraMap E K₂ (χ.restrictNormal E x) = χ (algebraMap E K₁ x)

Full source

@[simp]
theorem AlgEquiv.restrictNormal_commutes [Normal F E] (x : E) :
    algebraMap E K₂ (χ.restrictNormal E x) = χ (algebraMap E K₁ x) :=
  χ.toAlgHom.restrictNormal_commutes E x

Commutation of Restricted Algebra Equivalence with Inclusions in Normal Extension

Informal description

Let $E$ be a normal field extension of $F$, and let $\chi \colon K_1 \to K_2$ be an algebra equivalence between field extensions $K_1$ and $K_2$ of $E$. For any $x \in E$, the following diagram commutes: \[ \begin{tikzcd} E \arrow{r}{\chi|_E} \arrow{d}[swap]{\iota_1} & E \arrow{d}{\iota_2} \\ K_1 \arrow{r}[swap]{\chi} & K_2 \end{tikzcd} \] where $\chi|_E$ denotes the restriction of $\chi$ to $E$, and $\iota_1 \colon E \hookrightarrow K_1$, $\iota_2 \colon E \hookrightarrow K_2$ are the canonical inclusion maps. In other words, $\iota_2(\chi|_E(x)) = \chi(\iota_1(x))$ for all $x \in E$.

AlgEquiv.restrictNormal_trans theorem

[Normal F E] : (χ.trans ω).restrictNormal E = (χ.restrictNormal E).trans (ω.restrictNormal E)

Full source

theorem AlgEquiv.restrictNormal_trans [Normal F E] :
    (χ.trans ω).restrictNormal E = (χ.restrictNormal E).trans (ω.restrictNormal E) :=
  AlgEquiv.ext fun _ =>
    (algebraMap E K₃).injective
      (by simp only [AlgEquiv.trans_apply, AlgEquiv.restrictNormal_commutes])

Composition of Restricted Algebra Equivalences in Normal Extension

Informal description

Let $E$ be a normal field extension of $F$, and let $\chi \colon K_1 \to K_2$ and $\omega \colon K_2 \to K_3$ be algebra equivalences between field extensions $K_1$, $K_2$, and $K_3$ of $E$. Then the restriction of the composition $\omega \circ \chi$ to $E$ is equal to the composition of the restrictions of $\chi$ and $\omega$ to $E$, i.e., \[ (\omega \circ \chi)|_E = \omega|_E \circ \chi|_E. \]

AlgEquiv.restrictNormalHom definition

[Normal F E] : (K₁ ≃ₐ[F] K₁) →* E ≃ₐ[F] E

Full source

/-- Restriction to a normal subfield as a group homomorphism -/
def AlgEquiv.restrictNormalHom [Normal F E] : (K₁ ≃ₐ[F] K₁) →* E ≃ₐ[F] E :=
  MonoidHom.mk' (fun χ => χ.restrictNormal E) fun ω χ => χ.restrictNormal_trans ω E

Restriction homomorphism of algebra automorphisms to a normal extension

Informal description

Given a normal field extension $ E $ over $ F $, the function `AlgEquiv.restrictNormalHom` constructs a group homomorphism from the group of $ F $-algebra automorphisms of a field extension $ K_1 $ of $ E $ to the group of $ F $-algebra automorphisms of $ E $. This is done by restricting each automorphism $ \chi \colon K_1 \to K_1 $ to $ E $, yielding an automorphism $ \chi|_E \colon E \to E $. The homomorphism property is satisfied, meaning that the restriction of the composition $ \omega \circ \chi $ is equal to the composition of the restrictions $ \omega|_E \circ \chi|_E $.

AlgEquiv.restrictNormalHom_apply theorem

(L : IntermediateField F K₁) [Normal F L] (σ : (K₁ ≃ₐ[F] K₁)) (x : L) : restrictNormalHom L σ x = σ x

Full source

lemma AlgEquiv.restrictNormalHom_apply (L : IntermediateField F K₁) [Normal F L]
    (σ : (K₁ ≃ₐ[F] K₁)) (x : L) : restrictNormalHom L σ x = σ x :=
  AlgEquiv.restrictNormal_commutes σ L x

Restriction of Algebra Automorphism to Normal Intermediate Field Preserves Evaluation

Informal description

Let $F$ be a field, $K₁$ be a field extension of $F$, and $L$ be an intermediate field between $F$ and $K₁$ that is normal over $F$. For any $F$-algebra automorphism $\sigma$ of $K₁$ and any element $x \in L$, the restriction of $\sigma$ to $L$ evaluated at $x$ equals $\sigma(x)$, i.e., \[ (\sigma|_{L})(x) = \sigma(x). \]

Normal.algHomEquivAut definition

[Normal F E] : (E →ₐ[F] K₁) ≃ E ≃ₐ[F] E

Full source

/-- If `K₁/E/F` is a tower of fields with `E/F` normal then `AlgHom.restrictNormal'` is an
 equivalence. -/
@[simps, stacks 0BR4]
def Normal.algHomEquivAut [Normal F E] : (E →ₐ[F] K₁) ≃ E ≃ₐ[F] E where
  toFun σ := AlgHom.restrictNormal' σ E
  invFun σ := (IsScalarTower.toAlgHom F E K₁).comp σ.toAlgHom
  left_inv σ := by
    ext
    simp [AlgHom.restrictNormal']
  right_inv σ := by
    ext
    simp only [AlgHom.restrictNormal', AlgEquiv.toAlgHom_eq_coe, AlgEquiv.coe_ofBijective]
    apply FaithfulSMul.algebraMap_injective E K₁
    rw [AlgHom.restrictNormal_commutes]
    simp

Equivalence between algebra homomorphisms and automorphisms for normal extensions

Informal description

Given a normal field extension $ E $ over $ F $, the function `Normal.algHomEquivAut` establishes an equivalence between the set of $ F $-algebra homomorphisms from $ E $ to another field extension $ K_1 $ of $ F $, and the group of $ F $-algebra automorphisms of $ E $. More precisely: - The forward map takes an algebra homomorphism $ \sigma : E \to K_1 $ and restricts it to an automorphism of $ E $ via `AlgHom.restrictNormal'`. - The inverse map takes an automorphism $ \sigma : E \to E $ and composes it with the canonical inclusion $ E \to K_1 $. This equivalence holds because any $ F $-algebra homomorphism $ \sigma : E \to K_1 $ must map $ E $ into itself (due to normality), and thus restricts to an automorphism of $ E $.

AlgEquiv.restrictNormalHom_id theorem

 (F K : Type*) [Field F] [Field K] [Algebra F K] [Normal F K] : AlgEquiv.restrictNormalHom K = MonoidHom.id (K ≃ₐ[F] K)

Full source

/-- The group homomorphism given by restricting an algebra isomorphism to itself
is the identity map. -/
@[simp]
theorem AlgEquiv.restrictNormalHom_id (F K : Type*)
    [Field F] [Field K] [Algebra F K] [Normal F K] :
    AlgEquiv.restrictNormalHom K = MonoidHom.id (K ≃ₐ[F] K) := by
  ext f x
  dsimp only [restrictNormalHom, MonoidHom.mk'_apply, MonoidHom.id_apply]
  apply (algebraMap K K).injective
  rw [AlgEquiv.restrictNormal_commutes]
  simp only [Algebra.id.map_eq_id, RingHom.id_apply]

Restriction Homomorphism to Normal Extension is Identity on Automorphism Group

Informal description

Let $K$ be a normal field extension of $F$. The restriction homomorphism $\text{restrictNormalHom}_K$ from the group of $F$-algebra automorphisms of $K$ to itself is equal to the identity monoid homomorphism $\text{id} \colon (K \simeq_{F} K) \to (K \simeq_{F} K)$.

IsScalarTower.AlgEquiv.restrictNormalHom_comp theorem

 (F K₁ K₂ K₃ : Type*) [Field F] [Field K₁] [Field K₂] [Field K₃] [Algebra F K₁] [Algebra F K₂] [Algebra F K₃]
  [Algebra K₁ K₂] [Algebra K₁ K₃] [Algebra K₂ K₃] [IsScalarTower F K₁ K₃] [IsScalarTower F K₁ K₂]
  [IsScalarTower F K₂ K₃] [IsScalarTower K₁ K₂ K₃] [Normal F K₁] [Normal F K₂] :
  AlgEquiv.restrictNormalHom K₁ =
    (AlgEquiv.restrictNormalHom K₁).comp (AlgEquiv.restrictNormalHom (F := F) (K₁ := K₃) K₂)

Full source

/-- In a scalar tower `K₃/K₂/K₁/F` with `K₁` and `K₂` are normal over `F`, the group homomorphism
given by the restriction of algebra isomorphisms of `K₃` to `K₁` is equal to the composition of
the group homomorphism given by the restricting an algebra isomorphism of `K₃` to `K₂` and
the group homomorphism given by the restricting an algebra isomorphism of `K₂` to `K₁` -/
theorem AlgEquiv.restrictNormalHom_comp (F K₁ K₂ K₃ : Type*)
    [Field F] [Field K₁] [Field K₂] [Field K₃]
    [Algebra F K₁] [Algebra F K₂] [Algebra F K₃] [Algebra K₁ K₂] [Algebra K₁ K₃] [Algebra K₂ K₃]
    [IsScalarTower F K₁ K₃] [IsScalarTower F K₁ K₂] [IsScalarTower F K₂ K₃] [IsScalarTower K₁ K₂ K₃]
    [Normal F K₁] [Normal F K₂] :
    AlgEquiv.restrictNormalHom K₁ =
    (AlgEquiv.restrictNormalHom K₁).comp
    (AlgEquiv.restrictNormalHom (F := F) (K₁ := K₃) K₂) := by
  ext f x
  apply (algebraMap K₁ K₃).injective
  rw [IsScalarTower.algebraMap_eq K₁ K₂ K₃]
  simp only [AlgEquiv.restrictNormalHom, MonoidHom.mk'_apply, RingHom.coe_comp, Function.comp_apply,
    ← algebraMap_apply, AlgEquiv.restrictNormal_commutes, MonoidHom.coe_comp]

Composition of Restriction Homomorphisms for Normal Extensions in a Scalar Tower

Informal description

Let $ F $ be a field and $ K_1, K_2, K_3 $ be field extensions of $ F $ forming a scalar tower $ K_3/K_2/K_1/F $. Suppose $ K_1 $ and $ K_2 $ are normal extensions of $ F $. Then the restriction homomorphism from $ \text{Aut}_F(K_3) $ to $ \text{Aut}_F(K_1) $ is equal to the composition of the restriction homomorphism from $ \text{Aut}_F(K_3) $ to $ \text{Aut}_F(K_2) $ followed by the restriction homomorphism from $ \text{Aut}_F(K_2) $ to $ \text{Aut}_F(K_1) $. In other words, the following diagram of group homomorphisms commutes: \[ \begin{tikzcd} \text{Aut}_F(K_3) \arrow{r}{\text{res}_{K_3/K_2}} \arrow[swap]{dr}{\text{res}_{K_3/K_1}} & \text{Aut}_F(K_2) \arrow{d}{\text{res}_{K_2/K_1}} \\ & \text{Aut}_F(K_1) \end{tikzcd} \] where $ \text{res}_{L/K} $ denotes the restriction of automorphisms from $ L $ to $ K $.

IsScalarTower.AlgEquiv.restrictNormalHom_comp_apply theorem

 (K₁ K₂ : Type*) {F K₃ : Type*} [Field F] [Field K₁] [Field K₂] [Field K₃] [Algebra F K₁] [Algebra F K₂] [Algebra F K₃]
  [Algebra K₁ K₂] [Algebra K₁ K₃] [Algebra K₂ K₃] [IsScalarTower F K₁ K₃] [IsScalarTower F K₁ K₂]
  [IsScalarTower F K₂ K₃] [IsScalarTower K₁ K₂ K₃] [Normal F K₁] [Normal F K₂] (f : K₃ ≃ₐ[F] K₃) :
  AlgEquiv.restrictNormalHom K₁ f = (AlgEquiv.restrictNormalHom K₁) (AlgEquiv.restrictNormalHom K₂ f)

Full source

theorem AlgEquiv.restrictNormalHom_comp_apply (K₁ K₂ : Type*) {F K₃ : Type*}
    [Field F] [Field K₁] [Field K₂] [Field K₃]
    [Algebra F K₁] [Algebra F K₂] [Algebra F K₃] [Algebra K₁ K₂] [Algebra K₁ K₃] [Algebra K₂ K₃]
    [IsScalarTower F K₁ K₃] [IsScalarTower F K₁ K₂] [IsScalarTower F K₂ K₃] [IsScalarTower K₁ K₂ K₃]
    [Normal F K₁] [Normal F K₂] (f : K₃ ≃ₐ[F] K₃) :
    AlgEquiv.restrictNormalHom K₁ f =
    (AlgEquiv.restrictNormalHom K₁) (AlgEquiv.restrictNormalHom K₂ f) := by
  rw [IsScalarTower.AlgEquiv.restrictNormalHom_comp F K₁ K₂ K₃, MonoidHom.comp_apply]

Restriction of Automorphisms in a Scalar Tower of Normal Extensions

Informal description

Let $ F $ be a field and $ K_1, K_2, K_3 $ be field extensions of $ F $ forming a scalar tower $ K_3/K_2/K_1/F $. Suppose $ K_1 $ and $ K_2 $ are normal extensions of $ F $. Then for any $ F $-algebra automorphism $ f \colon K_3 \to K_3 $, the restriction of $ f $ to $ K_1 $ is equal to the restriction to $ K_1 $ of the restriction of $ f $ to $ K_2 $. In other words, the following holds for any $ f \in \text{Aut}_F(K_3) $: \[ f|_{K_1} = (f|_{K_2})|_{K_1} \] where $ f|_K $ denotes the restriction of $ f $ to a subfield $ K $.

Main Definitions