Module

NormalizationBaseChange.lean

Nyll.EtaleFundamentalGroups.Inertia.NormalizationBaseChange

9 declarations indexed from sourceView source ↗

Module documentation

Normalization endomorphisms and smooth base change

An endomorphism of X over S extends to the relative normalization of f : X → S by normalizationDesc. The actual normalization/base-change comparison commutes with this extension and the pulled-back endomorphism. This compatibility follows from the uniqueness part of normalization and holds for every base change.

For a smooth base change, including an etale chart, the comparison is an isomorphism. A point of the original normalization and a compatible lift of its base point then determine a point of the base-changed normalization; the two points have exactly the same fixing endomorphisms. This applies to geometric points and deck transformations without assuming the compatibility of either action. Localization of a stalk is not asserted to be smooth.

Imports3

Mathlib.AlgebraicGeometry.Normalization
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Imported by8

def

pullbackEndomorphism

L40 ↗

EtaleFundamentalGroups.Inertia.pullbackEndomorphism

Documentation

Pull back an actual endomorphism over the base, keeping the second factor fixed. The displayed equation is exactly the over-base condition.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u
variable {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S)

Lean source · statement

def pullbackEndomorphism (σ : X ⟶ X) (hσ : σ ≫ f = f) :
    pullback f g ⟶ pullback f g

theorem

pullbackEndomorphism_fst

L47 ↗

EtaleFundamentalGroups.Inertia.pullbackEndomorphism_fst

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u
variable {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S)

Lean source · statement

theorem pullbackEndomorphism_fst (σ : X ⟶ X) (hσ : σ ≫ f = f) :
    pullbackEndomorphism f g σ hσ ≫ pullback.fst f g =
      pullback.fst f g ≫ σ

theorem

pullbackEndomorphism_snd

L53 ↗

EtaleFundamentalGroups.Inertia.pullbackEndomorphism_snd

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u
variable {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S)

Lean source · statement

theorem pullbackEndomorphism_snd (σ : X ⟶ X) (hσ : σ ≫ f = f) :
    pullbackEndomorphism f g σ hσ ≫ pullback.snd f g = pullback.snd f g

def

normalizationEndomorphism

L64 ↗

EtaleFundamentalGroups.Inertia.normalizationEndomorphism

Documentation

Extend an endomorphism over the base by the universal property of relative normalization. This is the construction used for normalization deck maps.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u
variable {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S)
section Normalization
variable [QuasiCompact f] [QuasiSeparated f]

Lean source · statement

def normalizationEndomorphism (σ : X ⟶ X) (hσ : σ ≫ f = f) :
    f.normalization ⟶ f.normalization

theorem

toNormalization_normalizationEndomorphism

L70 ↗

EtaleFundamentalGroups.Inertia.toNormalization_normalizationEndomorphism

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u
variable {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S)
section Normalization
variable [QuasiCompact f] [QuasiSeparated f]

Lean source · statement

theorem toNormalization_normalizationEndomorphism
    (σ : X ⟶ X) (hσ : σ ≫ f = f) :
    f.toNormalization ≫ normalizationEndomorphism f σ hσ =
      σ ≫ f.toNormalization

theorem

normalizationEndomorphism_fromNormalization

L77 ↗

EtaleFundamentalGroups.Inertia.normalizationEndomorphism_fromNormalization

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u
variable {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S)
section Normalization
variable [QuasiCompact f] [QuasiSeparated f]

Lean source · statement

theorem normalizationEndomorphism_fromNormalization
    (σ : X ⟶ X) (hσ : σ ≫ f = f) :
    normalizationEndomorphism f σ hσ ≫ f.fromNormalization = f.fromNormalization

theorem

normalizationPullback_endomorphism

L85 ↗

EtaleFundamentalGroups.Inertia.normalizationPullback_endomorphism

Documentation

Normalization/base-change comparison intertwines the actual extended endomorphisms. Smoothness is unnecessary for this commuting square.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u
variable {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S)
section Normalization
variable [QuasiCompact f] [QuasiSeparated f]

Lean source · statement

theorem normalizationPullback_endomorphism
    (σ : X ⟶ X) (hσ : σ ≫ f = f) :
    normalizationEndomorphism (pullback.snd f g)
        (pullbackEndomorphism f g σ hσ)
        (pullbackEndomorphism_snd f g σ hσ) ≫
      f.normalizationPullback g =
    f.normalizationPullback g ≫
      pullbackEndomorphism f.fromNormalization g
        (normalizationEndomorphism f σ hσ)
        (normalizationEndomorphism_fromNormalization f σ hσ)

theorem

normalizationPullback_conjugates_endomorphism

L115 ↗

EtaleFundamentalGroups.Inertia.normalizationPullback_conjugates_endomorphism

Documentation

Whenever the canonical comparison is an isomorphism, it conjugates the two normalization endomorphisms. This applies to smooth base change and to the canonical comparison constructed for an affine localization.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u
variable {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S)
section Normalization
variable [QuasiCompact f] [QuasiSeparated f]

Lean source · statement

theorem normalizationPullback_conjugates_endomorphism [IsIso (f.normalizationPullback g)]
    (σ : X ⟶ X) (hσ : σ ≫ f = f) :
    normalizationEndomorphism (pullback.snd f g)
        (pullbackEndomorphism f g σ hσ)
        (pullbackEndomorphism_snd f g σ hσ) =
      f.normalizationPullback g ≫
        pullbackEndomorphism f.fromNormalization g
          (normalizationEndomorphism f σ hσ)
          (normalizationEndomorphism_fromNormalization f σ hσ) ≫
        inv (f.normalizationPullback g)

theorem

normalizationPullback_fixes_point_iff

L134 ↗

EtaleFundamentalGroups.Inertia.normalizationPullback_fixes_point_iff

Documentation

When the canonical normalization comparison is an isomorphism, a point and its compatible lift have exactly the same fixing endomorphisms. For a geometric point, take T = Spec Ω. The lifted point is constructed by the pullback universal property and the inverse of the actual normalization comparison.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u
variable {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S)
section Normalization
variable [QuasiCompact f] [QuasiSeparated f]

Lean source · statement

theorem normalizationPullback_fixes_point_iff [IsIso (f.normalizationPullback g)]
    {T : Scheme.{u}} (z : T ⟶ f.normalization) (y : T ⟶ Y)
    (hzy : z ≫ f.fromNormalization = y ≫ g)
    (σ : X ⟶ X) (hσ : σ ≫ f = f) :
    (pullback.lift z y hzy ≫ inv (f.normalizationPullback g)) ≫
        normalizationEndomorphism (pullback.snd f g)
          (pullbackEndomorphism f g σ hσ)
          (pullbackEndomorphism_snd f g σ hσ) =
      pullback.lift z y hzy ≫ inv (f.normalizationPullback g) ↔
    z ≫ normalizationEndomorphism f σ hσ = z

Module documentation

Normalization endomorphisms and smooth base change

Declarations