Documentation

TauCeti.FieldTheory.Galois.Restriction

Restricting automorphisms along an embedding of a normal extension #

Mathlib's AlgEquiv.restrictNormalHom restricts automorphisms of K/F to a normal subextension M/F given by a scalar tower F → M → K. This file restricts along an arbitrary embedding f : M →ₐ[F] K instead, which is convenient when M is an intermediate field sitting inside K through a map other than the algebra map (for example an IntermediateField.inclusion).

In an abstract scalar tower with a normal intermediate field, restriction to the intermediate field is the identity precisely when the automorphism fixes it pointwise; its kernel is the image of restriction of scalars.

Main definitions and results #

source
instance AlgHom.normal_fieldRange {F : Type u_1} {K : Type u_2} {M : Type u_3} [Field F] [Field K] [Field M] [Algebra F K] [Algebra F M] (f : M →ₐ[F] K) [Normal F M] :
Normal F ↥f.fieldRange

The image of a normal extension M/F under an F-embedding is normal over F.

source
noncomputable def AlgHom.restrictNormalHom {F : Type u_1} {K : Type u_2} {M : Type u_3} [Field F] [Field K] [Field M] [Algebra F K] [Algebra F M] (f : M →ₐ[F] K) [Normal F M] :
Gal(K/F) →* Gal(M/F)

Restriction of automorphisms along an embedding f : M →ₐ[F] K of a normal extension M/F. Every σ : Gal(K/F) maps the image of f to itself, and f.restrictNormalHom σ is the automorphism of M it induces, so that f (f.restrictNormalHom σ x) = σ (f x) (AlgHom.restrictNormalHom_commutes). For the algebra map of a scalar tower this is AlgEquiv.restrictNormalHom (AlgHom.restrictNormalHom_toAlgHom).

Equations
Instances For
    source
    @[simp]
    theorem AlgHom.restrictNormalHom_commutes {F : Type u_1} {K : Type u_2} {M : Type u_3} [Field F] [Field K] [Field M] [Algebra F K] [Algebra F M] (f : M →ₐ[F] K) [Normal F M] (σ : Gal(K/F)) (x : M) :
    f ((f.restrictNormalHom σ) x) = σ (f x)
    source
    theorem AlgHom.restrictNormalHom_eq_iff {F : Type u_1} {K : Type u_2} {M : Type u_3} [Field F] [Field K] [Field M] [Algebra F K] [Algebra F M] (f : M →ₐ[F] K) [Normal F M] {σ : Gal(K/F)} {τ : Gal(M/F)} :
    f.restrictNormalHom σ = τ ↔ ∀ (x : M), σ (f x) = f (τ x)

    f.restrictNormalHom σ is the unique automorphism of M intertwined with σ by f.

    source
    @[simp]
    theorem AlgHom.restrictNormalHom_toAlgHom {F : Type u_1} {K : Type u_2} {M : Type u_3} [Field F] [Field K] [Field M] [Algebra F K] [Algebra F M] [Algebra M K] [IsScalarTower F M K] [Normal F M] :
    (IsScalarTower.toAlgHom F M K).restrictNormalHom = AlgEquiv.restrictNormalHom M

    For the algebra map of a scalar tower, restriction along it is Mathlib's AlgEquiv.restrictNormalHom.

    source
    theorem AlgHom.restrictNormalHom_surjective {F : Type u_1} {K : Type u_2} {M : Type u_3} [Field F] [Field K] [Field M] [Algebra F K] [Algebra F M] (f : M →ₐ[F] K) [Normal F M] [Normal F K] :
    Function.Surjective ⇑f.restrictNormalHom

    For a normal K/F, every automorphism of M/F is the restriction of one of K/F.

    source
    theorem AlgHom.ker_restrictNormalHom {F : Type u_1} {K : Type u_2} {M : Type u_3} [Field F] [Field K] [Field M] [Algebra F K] [Algebra F M] (f : M →ₐ[F] K) [Normal F M] :
    f.restrictNormalHom.ker = f.fieldRange.fixingSubgroup

    The kernel of restriction along f is the subgroup fixing the image of f pointwise.

    source
    @[simp]
    theorem IntermediateField.restrictNormalHom_val {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (L : IntermediateField F K) [Normal F ↥L] :
    L.val.restrictNormalHom = AlgEquiv.restrictNormalHom ↥L

    Restriction along the inclusion of an intermediate field is Mathlib's AlgEquiv.restrictNormalHom.

    source
    theorem IntermediateField.units_map_val_restrictNormalHom {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (L : IntermediateField F K) [Normal F ↥L] (σ : Gal(K/F)) (u : (↥L)ˣ) :
    (Units.map ↑L.val.toRingHom) ((Units.map ↑((AlgEquiv.restrictNormalHom ↥L) σ)) u) = σ • (Units.map ↑L.val.toRingHom) u

    Including the units of a normal intermediate field L into Kˣ intertwines the action of Gal(L/F) on Lˣ, through restriction, with the action of Gal(K/F) on Kˣ.

    source
    theorem AlgHom.restrictNormalHom_comp {F : Type u_1} {K : Type u_2} {M : Type u_3} [Field F] [Field K] [Field M] [Algebra F K] [Algebra F M] (f : M →ₐ[F] K) [Normal F M] (τ : Gal(M/F)) (σ : Gal(K/F)) :
    (f.comp ↑τ).restrictNormalHom σ = τ⁻¹ * f.restrictNormalHom σ * τ

    Restriction along a twisted embedding is conjugate: precomposing f with an automorphism τ of M/F conjugates restriction along f by τ.

    source
    theorem IntermediateField.normalClosure_eq_fieldRange {F : Type u_1} {K : Type u_2} {M : Type u_3} [Field F] [Field K] [Field M] [Algebra F K] [Algebra F M] (f : M →ₐ[F] K) [Normal F M] :
    normalClosure F M K = f.fieldRange

    The normal closure of a normal extension is its image: every F-embedding of a normal extension M/F into K has image the normal closure of M in K, so all of them have the same image.

    source
    theorem AlgHom.exists_comp_eq_of_normal {F : Type u_1} {K : Type u_2} {M : Type u_3} [Field F] [Field K] [Field M] [Algebra F K] [Algebra F M] (f g : M →ₐ[F] K) [Normal F M] :
    ∃ (τ : Gal(M/F)), f.comp ↑τ = g

    Two embeddings of a normal extension differ by an automorphism: for F-embeddings f g : M →ₐ[F] K of a normal extension M/F, there is τ ∈ Gal(M/F) with g = f ∘ τ.

    source
    noncomputable def AlgHom.restrictNormalHomOfLE {F : Type u_1} {K : Type u_2} {M : Type u_3} [Field F] [Field K] [Field M] [Algebra F K] [Algebra F M] (f : M →ₐ[F] K) {N : IntermediateField F K} [Normal F ↥N] (h : N ≤ f.fieldRange) :
    Gal(M/F) →* Gal(↥N/F)

    Restriction of automorphisms of M/F to a normal intermediate field N of K lying in the image of an embedding f : M →ₐ[F] K. Through f, the field N is a subextension of M, and f.restrictNormalHomOfLE h σ is the automorphism of N induced by σ: it sends f x to f (σ x) (AlgHom.coe_restrictNormalHomOfLE_apply).

    Equations
    Instances For
      source
      theorem AlgHom.coe_restrictNormalHomOfLE_apply {F : Type u_1} {K : Type u_2} {M : Type u_3} [Field F] [Field K] [Field M] [Algebra F K] [Algebra F M] (f : M →ₐ[F] K) {N : IntermediateField F K} [Normal F ↥N] (h : N ≤ f.fieldRange) (σ : Gal(M/F)) {x : M} {y : ↥N} (hxy : f x = ↑y) :
      ↑(((f.restrictNormalHomOfLE h) σ) y) = f (σ x)

      f.restrictNormalHomOfLE h σ sends f x to f (σ x).

      source
      theorem AlgHom.restrictNormalHomOfLE_surjective {F : Type u_1} {K : Type u_2} {M : Type u_3} [Field F] [Field K] [Field M] [Algebra F K] [Algebra F M] (f : M →ₐ[F] K) [Normal F M] {N : IntermediateField F K} [Normal F ↥N] (h : N ≤ f.fieldRange) :
      Function.Surjective ⇑(f.restrictNormalHomOfLE h)

      Restriction to a normal intermediate field in the image of f is surjective.

      Restriction to an intermediate field in a tower #

      source
      theorem AlgEquiv.restrictNormal_eq_one_iff_algebraMap (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [Normal K L] (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (σ : Gal(M/K)) :
      σ.restrictNormal L = 1 ↔ ∀ (x : L), σ ((algebraMap L M) x) = (algebraMap L M) x

      σ restricts to the identity on L exactly when it fixes L pointwise. Mathlib's AlgEquiv.restrictNormal_eq_one_iff says this for an IntermediateField, while AlgEquiv.restrictNormal itself is already stated for an abstract algebra L, so only the characterisation needs transporting to a tower K ⊆ L ⊆ M.

      source
      theorem AlgEquiv.restrictNormalHom_apply_eq_restrictNormal (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [Normal K L] (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (σ : Gal(M/K)) :
      (restrictNormalHom L) σ = σ.restrictNormal L

      Restriction as a group homomorphism agrees with restriction of an automorphism.

      source
      theorem AlgEquiv.mem_range_restrictScalarsHom_iff_restrictNormal_eq_one (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [Normal K L] (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (σ : Gal(M/K)) :
      σ ∈ (restrictScalarsHom K).range ↔ σ.restrictNormal L = 1

      An automorphism of M/K comes from an automorphism of M/L exactly when its restriction to L is the identity.

      source
      theorem AlgEquiv.range_restrictScalarsHom_eq_ker_restrictNormalHom (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [Normal K L] (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] :
      (restrictScalarsHom K).range = (restrictNormalHom L).ker

      The image of Gal(M/L) in Gal(M/K) under restriction of scalars is the kernel of restriction to L.

      source
      @[simp]
      theorem AlgEquiv.restrictNormal_mul_restrictScalars (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [Normal K L] (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (σ : Gal(M/K)) (τ : Gal(M/L)) :
      (σ * restrictScalars K τ).restrictNormal L = σ.restrictNormal L

      Multiplying by an automorphism of M/L does not change the restriction to L.

      Restriction to a simple normal subextension #

      source
      theorem AlgEquiv.restrictNormalHom_adjoin_simple_eq_one_iff {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {α : E} [Normal F ↥F⟮α⟯] (σ : Gal(E/F)) :
      (restrictNormalHom ↥F⟮α⟯) σ = 1 ↔ σ α = α

      σ restricts to the identity on F⟮α⟯ exactly when it fixes α, for a normal simple subextension F⟮α⟯ of E/F.