Module

ActualFiniteNormalizationResidueMap.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteNormalizationResidueMap

1 declaration indexed from sourceView source ↗

Module documentation

Residue embeddings of finite normalizations

Constructs the residue-field embedding from a finite contracted normalization prime into the residue field of the original prime.

Imports3

Nyll.SchemeTheory.Normalization.SubalgebraPreimage
Nyll.EtaleFundamentalGroups.Inertia.AbsoluteFiniteNormalization
Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Imported by9

def

actualFiniteNormalizationResidueMap

L26 ↗

EtaleFundamentalGroups.Inertia.actualFiniteNormalizationResidueMap

Documentation

The canonical residue embedding at the literal finite contraction of the original normalization prime. No infinite local valuation is required.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w

Lean source · full declaration

def actualFiniteNormalizationResidueMap
    (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
    (Q : Ideal (SchemeTheory.normalizationCommAlgCat A L)) [Q.IsPrime]
    (E : FiniteGaloisIntermediateField K L) :
    letI := finiteAbsoluteNormalizationPrime_isPrime A K L Q E
    (finiteAbsoluteNormalizationPrime A K L Q E).ResidueField →+* Q.ResidueField := by
  letI := finiteAbsoluteNormalizationPrime_isPrime A K L Q E
  exact Ideal.ResidueField.map (finiteAbsoluteNormalizationPrime A K L Q E) Q
    (finiteAbsoluteNormalizationRingMap A K L E) rfl

Module documentation

Residue embeddings of finite normalizations

Declarations

actualFiniteNormalizationResidueMap