Module

FiniteNormalizationGaloisSurjectivity.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteNormalizationGaloisSurjectivity

2 declarations indexed from sourceView source ↗

Module documentation

Finite normalization automorphisms have actual field lifts

The fraction-field extension theorem is applied in the native coefficient field owner. The original ambient field does not enter that proof.

Imports4

Imported by3

theorem

nativeNormalizationGaloisGroupMap_surjective

L29 ↗

EtaleFundamentalGroups.Inertia.nativeNormalizationGaloisGroupMap_surjective

Documentation

Every coefficient automorphism extends over the actual finite fraction field. The native coefficient algebra keeps its original ring.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w

Lean source · full declaration

theorem nativeNormalizationGaloisGroupMap_surjective
    (A : Type u) (K : Type v) [CommRing A] [Field K]
    [Algebra A K] [IsFractionRing A K]
    (C : CommAlgCat.{w} A) (hC : IsField C.carrier)
    [Algebra K C.carrier] [IsScalarTower A K C.carrier]
    [FiniteDimensional K C.carrier] :
    Function.Surjective
      (fun g : (galoisGroupObject K C.carrier).carrier =>
        (normalizationAutomorphismGroupMap A C).hom'.toFun
          ((scalarRestrictionGroupMap A K C).hom'.toFun g)) := by
  let : Field C.carrier := hC.toField
  exact normalizationGaloisGroupMap_surjective A K C.carrier

theorem

finiteNormalizationGaloisGroupMap_surjective

L44 ↗

EtaleFundamentalGroups.Inertia.finiteNormalizationGaloisGroupMap_surjective