Module

FiniteGaloisRestrictionSeparation.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteGaloisRestrictionSeparation

1 declaration indexed from sourceView source ↗

Module documentation

Actual finite Galois restrictions separate original automorphisms

Every coefficient belongs to its finite Galois closure. Agreement on all actual finite restrictions therefore gives agreement on every coefficient.

Imports3

Nyll.EtaleFundamentalGroups.Inertia.FiniteGaloisRestrictionGroupMap
Mathlib.FieldTheory.Galois.GaloisClosure
Mathlib.FieldTheory.Normal.Defs

Imported by2

theorem

finiteGaloisRestrictionGroupMap_jointly_injective

L23 ↗

EtaleFundamentalGroups.Inertia.finiteGaloisRestrictionGroupMap_jointly_injective

Documentation

Joint faithfulness is derived from the actual finite Galois closures.

Source context 2 commands

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

namespace EtaleFundamentalGroups.Inertia
universe v w

Lean source · statement

theorem finiteGaloisRestrictionGroupMap_jointly_injective
    (K : Type v) (L : Type w) [Field K] [Field L] [Algebra K L] [IsGalois K L]
    (σ τ : Gal(L/K))
    (h : ∀ E : FiniteGaloisIntermediateField K L,
      (finiteGaloisRestrictionGroupMap K L E).hom'.toFun σ =
        (finiteGaloisRestrictionGroupMap K L E).hom'.toFun τ) : σ = τ

Module documentation

Actual finite Galois restrictions separate original automorphisms

Declarations

finiteGaloisRestrictionGroupMap_jointly_injective