Module

ClosedNormalFiniteGalois.lean

Nyll.EtaleFundamentalGroups.Inertia.ClosedNormalFiniteGalois

2 declarations indexed from sourceView source ↗

Module documentation

Closed normal subgroups detected by finite Galois subfields

Every element of the fixed field of a closed normal subgroup lies in a finite Galois subfield of that same fixed field. Thus the subgroup is the intersection of the finite Galois restriction kernels containing it. This gives the field-theoretic finite-quotient criterion needed in Tag 0BTD.

Imports3

Mathlib.FieldTheory.Galois.Infinite
Mathlib.FieldTheory.Galois.Profinite
Mathlib.Topology.Algebra.Group.Subgroup

Imported by2

theorem

closedNormalSubgroup_eq_iInf_finiteGalois_fixingSubgroup

L30 ↗

EtaleFundamentalGroups.Inertia.closedNormalSubgroup_eq_iInf_finiteGalois_fixingSubgroup

Documentation

A closed normal Galois subgroup is detected by the finite Galois subextensions which it fixes. The finite subextension containing a specified fixed element is constructed by taking its actual normal closure.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u v
variable (K : Type u) (L : Type v) [Field K] [Field L]
  [Algebra K L] [IsGalois K L]

Lean source · statement

theorem closedNormalSubgroup_eq_iInf_finiteGalois_fixingSubgroup
    (H : ClosedSubgroup Gal(L/K)) [H.toSubgroup.Normal] :
    H.toSubgroup =
      ⨅ (E : FiniteGaloisIntermediateField K L)
        (_ : H.toSubgroup ≤ E.toIntermediateField.fixingSubgroup),
        E.toIntermediateField.fixingSubgroup

theorem

topologicalClosure_normalClosure_eq_iInf_finiteGalois

L64 ↗

EtaleFundamentalGroups.Inertia.topologicalClosure_normalClosure_eq_iInf_finiteGalois