Nyll.EtaleFundamentalGroups.Inertia.NormalizationResidueInertia

Module documentation

Literal point-and-residue inertia on an unramified normalization

An actual normalization endomorphism fixing a point and acting trivially on its residue field fixes the canonical residue-field point morphism. The proved normalization rigidity therefore makes that endomorphism the identity. This uses the original point-and-residue condition directly, without defining a substitute inertia group.

theorem

normalizationEndomorphism_eq_id_of_trivial_residue

L32 ↗

EtaleFundamentalGroups.Inertia.normalizationEndomorphism_eq_id_of_trivial_residue

Documentation

On an unramified normalization of an integral source, the original point-and-residue inertia condition forces the actual normalization endomorphism to be the identity.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · statement

theorem normalizationEndomorphism_eq_id_of_trivial_residue
    {X S : Scheme.{u}} [IsIntegral X]
    (f : X ⟶ S) [QuasiCompact f] [QuasiSeparated f]
    [FormallyUnramified f.fromNormalization] [LocallyOfFiniteType f.fromNormalization]
    (σ : X ⟶ X) (hσ : σ ≫ f = f) (y : f.normalization)
    (hy : normalizationEndomorphism f σ hσ y = y)
    (hres : (normalizationEndomorphism f σ hσ).residueFieldMap y =
      (f.normalization.residueFieldCongr hy).hom) :
    normalizationEndomorphism f σ hσ = 𝟙 f.normalization

Module documentation

Literal point-and-residue inertia on an unramified normalization

Declarations

normalizationEndomorphism_eq_id_of_trivial_residue