Module

NormalizationPointRigidity.lean

Nyll.EtaleFundamentalGroups.Inertia.NormalizationPointRigidity

1 declaration indexed from sourceView source ↗

Module documentation

Point rigidity of actual normalization endomorphisms

Normalization of an integral source is integral and its structure map is separated. If this structure map is unramified, fixing a nonempty test morphism forces an actual normalization endomorphism to be the identity.

Imports4

Nyll.SchemeTheory.Morphisms.UnramifiedPointRigidity
Nyll.EtaleFundamentalGroups.Inertia.NormalizationBaseChange
Mathlib.AlgebraicGeometry.Normalization
Mathlib.AlgebraicGeometry.Morphisms.Separated

Imported by3

theorem

normalizationEndomorphism_eq_id_of_fixes_nonempty

L30 ↗

EtaleFundamentalGroups.Inertia.normalizationEndomorphism_eq_id_of_fixes_nonempty

Documentation

The actual extension by normalization is rigid at a nonempty point whenever the normalization morphism is unramified.

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_fixes_nonempty
    {X S T : Scheme.{u}} [IsIntegral X] [Nonempty T]
    (f : X ⟶ S) [QuasiCompact f] [QuasiSeparated f]
    [FormallyUnramified f.fromNormalization] [LocallyOfFiniteType f.fromNormalization]
    (σ : X ⟶ X) (hσ : σ ≫ f = f) (z : T ⟶ f.normalization)
    (hz : z ≫ normalizationEndomorphism f σ hσ = z) :
    normalizationEndomorphism f σ hσ = 𝟙 f.normalization

Module documentation

Point rigidity of actual normalization endomorphisms

Declarations

normalizationEndomorphism_eq_id_of_fixes_nonempty