Module

FiniteNormalizationGaloisFaithful.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteNormalizationGaloisFaithful

2 declarations indexed from sourceView source ↗

Module documentation

Faithfulness of actual finite normalization automorphisms

Fraction-field uniqueness proves faithfulness in the native finite field owner. The actual finite-stage map then uses that closed result.

Imports6

Imported by2

theorem

nativeNormalizationGaloisGroupMap_injective

L28 ↗

EtaleFundamentalGroups.Inertia.nativeNormalizationGaloisGroupMap_injective

Documentation

A native finite field automorphism is determined by its normalization.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w

Lean source · full declaration

theorem nativeNormalizationGaloisGroupMap_injective
    (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.Injective
      (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
  intro σ τ hστ
  apply normalizationGaloisRingHom_injective A K C.carrier
  exact congrArg (commAlgAutomorphismRingHom A (normalizationCommAlgCat A C.carrier)) hστ

theorem

finiteNormalizationGaloisGroupMap_injective

L44 ↗

EtaleFundamentalGroups.Inertia.finiteNormalizationGaloisGroupMap_injective