Module

FiniteFieldExtensions.lean

Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.FiniteFieldExtensions

1 declaration indexed from sourceView source ↗

Module documentation

Ab-faithfulness under finite field extension

Ab-faithfulness of the absolute Galois group passes to finite field extensions, including inseparable extensions.

Imports3

Imported by3

theorem

isAbFaithful_absoluteGaloisGroup_of_finiteExtension

L26 ↗

Yamaguchi26AbfaithfulGalois.isAbFaithful_absoluteGaloisGroup_of_finiteExtension

Documentation

Ab-faithfulness of the absolute Galois group passes to every finite field extension, including inseparable extensions.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.FiniteStepSolvableQuotients KummerTheory
universe u v

Lean source · statement

theorem isAbFaithful_absoluteGaloisGroup_of_finiteExtension
    {K : Type u} {E : Type v} [Field K] [Field E] [Algebra K E]
    [FiniteDimensional K E]
    (hK : IsAbFaithful Gal(AlgebraicClosure K/K)) :
    IsAbFaithful Gal(AlgebraicClosure E/E)

Module documentation

Ab-faithfulness under finite field extension

Declarations

isAbFaithful_absoluteGaloisGroup_of_finiteExtension