NYLL
Module

FiniteExtensionGalois.lean

Nyll.GaloisCohomology.Topology.FiniteExtensionGalois
4 declarations indexed from sourceView source ↗

Module documentation

Open Galois subgroups from finite field extensions

Scalar restriction is continuous and identifies the upper Galois group with the open subgroup fixing the embedded finite extension field.

Imports4
Imported by4

Declarations

theorem

continuous_galoisRestrictScalars

L30 ↗
GaloisCohomology.continuous_galoisRestrictScalars
Documentation

Restriction of scalars is continuous for an algebraic upper extension.

Source context 4 commands

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

namespace GaloisCohomology
open scoped Topology
universe u v w
variable (K : Type u) (E : Type v) (Ω : Type w)
  [Field K] [Field E] [Field Ω] [Algebra K E] [Algebra E Ω] [Algebra K Ω]
  [IsScalarTower K E Ω]
Lean source · statement
theorem continuous_galoisRestrictScalars [Algebra.IsAlgebraic E Ω] :
    Continuous (AlgEquiv.restrictScalarsHom K : Gal(Ω/E) →* Gal(Ω/K))
theorem

galoisRestrictScalars_range

L55 ↗
GaloisCohomology.galoisRestrictScalars_range
Documentation

The image of scalar restriction fixes exactly the embedded lower field.

Source context 4 commands

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

namespace GaloisCohomology
open scoped Topology
universe u v w
variable (K : Type u) (E : Type v) (Ω : Type w)
  [Field K] [Field E] [Field Ω] [Algebra K E] [Algebra E Ω] [Algebra K Ω]
  [IsScalarTower K E Ω]
Lean source · statement
theorem galoisRestrictScalars_range :
    (AlgEquiv.restrictScalarsHom K : Gal(Ω/E) →* Gal(Ω/K)).range =
      (IsScalarTower.toAlgHom K E Ω).fieldRange.fixingSubgroup
def

finiteExtensionGaloisOpenSubgroup

L74 ↗
GaloisCohomology.finiteExtensionGaloisOpenSubgroup
Documentation

The finite extension gives an actual open subgroup of the lower Galois group.

Source context 5 commands

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

namespace GaloisCohomology
open scoped Topology
universe u v w
variable (K : Type u) (E : Type v) (Ω : Type w)
  [Field K] [Field E] [Field Ω] [Algebra K E] [Algebra E Ω] [Algebra K Ω]
  [IsScalarTower K E Ω]
variable [FiniteDimensional K E]
Lean source · full declaration
def finiteExtensionGaloisOpenSubgroup : OpenSubgroup Gal(Ω/K) where
  toSubgroup := (AlgEquiv.restrictScalarsHom K : Gal(Ω/E) →* Gal(Ω/K)).range
  isOpen' := by
    rw [galoisRestrictScalars_range K E Ω]
    have : FiniteDimensional K (IsScalarTower.toAlgHom K E Ω).fieldRange :=
      Module.Finite.equiv (IsScalarTower.toAlgHom K E Ω).equivFieldRange.toLinearEquiv
    exact IntermediateField.fixingSubgroup_isOpen _
def

finiteExtensionGaloisOpenSubgroupEquiv

L86 ↗
GaloisCohomology.finiteExtensionGaloisOpenSubgroupEquiv
Documentation

Scalar restriction identifies the upper absolute Galois group with this open subgroup. This includes inseparable finite extensions of the lower field.

Source context 6 commands

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

namespace GaloisCohomology
open scoped Topology
universe u v w
variable (K : Type u) (E : Type v) (Ω : Type w)
  [Field K] [Field E] [Field Ω] [Algebra K E] [Algebra E Ω] [Algebra K Ω]
  [IsScalarTower K E Ω]
variable [FiniteDimensional K E]
variable [IsAlgClosure E Ω]
Lean source · statement
def finiteExtensionGaloisOpenSubgroupEquiv :
    Gal(Ω/E) ≃ₜ* (finiteExtensionGaloisOpenSubgroup K E Ω : Subgroup Gal(Ω/K))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.