Module

NormalRestrictionKernelFinite.lean

Nyll.GaloisCohomology.Kummer.Concrete.NormalRestrictionKernelFinite

2 declarations indexed from sourceView source ↗

Module documentation

Finite normal restriction kernels

The kernel of restriction to a finite normal extension is the fixing subgroup of its actual image in the upper field. If the upper extension is normal and the finite extension is Galois, restriction is surjective and this kernel has index equal to the field degree.

Imports6

Mathlib.FieldTheory.Galois.Basic
Mathlib.FieldTheory.KrullTopology
Mathlib.FieldTheory.Normal.Basic
Mathlib.FieldTheory.IntermediateField.Basic
Mathlib.GroupTheory.Index
Mathlib.GroupTheory.QuotientGroup.Basic

Imported by4

theorem

normalRestrictionKernel_isOpen

L32 ↗

KummerTheory.normalRestrictionKernel_isOpen

Documentation

Restriction to a finite normal extension has open kernel in the actual upper Galois group, without algebraicity assumptions on the upper field.

Source context 3 commands

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

namespace KummerTheory
universe u
variable {K M Ω : Type u} [Field K] [Field M] [Field Ω]
  [Algebra K M] [Algebra M Ω] [Algebra K Ω] [IsScalarTower K M Ω]

Lean source · statement

theorem normalRestrictionKernel_isOpen [FiniteDimensional K M] [Normal K M] :
    IsOpen (((AlgEquiv.restrictNormalHom M : Gal(Ω/K) →* Gal(M/K)).ker :
      Subgroup Gal(Ω/K)) : Set Gal(Ω/K))

theorem

normalRestrictionKernel_index

L64 ↗

KummerTheory.normalRestrictionKernel_index