Module

NormalSubgroupEmbeddings.lean

Nyll.EtaleFundamentalGroups.Inertia.NormalSubgroupEmbeddings

1 declaration indexed from sourceView source ↗

Module documentation

Normal subgroups acting on field embeddings

For a normal subgroup of the automorphism group of a normal field extension, fixing an intermediate field is equivalent to fixing every embedding of that field into the ambient extension. The intermediate field need not be normal or finite, and the subgroup need not be closed.

Imports3

Mathlib.FieldTheory.Galois.Basic
Mathlib.FieldTheory.Normal.Basic
Mathlib.GroupTheory.GroupAction.SubMulAction

Imported by3

theorem

normalSubgroup_fixes_embeddings_iff_le_fixingSubgroup

L31 ↗

EtaleFundamentalGroups.normalSubgroup_fixes_embeddings_iff_le_fixingSubgroup

Documentation

A normal subgroup acts trivially on all embeddings of an intermediate field precisely when it fixes that field pointwise. Embeddings are extended to ambient automorphisms using normality of the ambient extension, without any normality assumption on the intermediate field.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace EtaleFundamentalGroups
universe u v
variable {K : Type u} {E : Type v} [Field K] [Field E] [Algebra K E]
  [Normal K E]

Lean source · statement

theorem normalSubgroup_fixes_embeddings_iff_le_fixingSubgroup
    (H : Subgroup (E ≃ₐ[K] E)) [H.Normal] (L : IntermediateField K E) :
    (∀ g ∈ H, ∀ φ : L →ₐ[K] E, g.toAlgHom.comp φ = φ) ↔
      H ≤ L.fixingSubgroup

Module documentation

Normal subgroups acting on field embeddings

Declarations

normalSubgroup_fixes_embeddings_iff_le_fixingSubgroup