NYLL
Module

NormalizationSourceIso.lean

Nyll.EtaleFundamentalGroups.Inertia.NormalizationSourceIso
5 declarations indexed from sourceView source ↗

Module documentation

Relative normalization under an isomorphism of source schemes

The comparison is constructed in both directions by normalizationDesc. Its compatibility with endomorphisms follows from the same universal property. It can therefore transport an actual cover to its affine spectrum without replacing geometric-point equality by topological-point equality.

Imports2
Imported by18

Declarations

def

normalizationSourceIso

L34 ↗
EtaleFundamentalGroups.Inertia.normalizationSourceIso
Documentation

An actual source isomorphism over the base extends to an isomorphism of relative normalizations, by their universal properties.

Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
variable {A B S : Scheme.{u}}
variable (f : A ⟶ S) (g : B ⟶ S)
variable [QuasiCompact f] [QuasiSeparated f] [QuasiCompact g] [QuasiSeparated g]
variable (e : A ≅ B) (he : e.hom ≫ g = f)
Lean source · statement
def normalizationSourceIso : f.normalization ≅ g.normalization
theorem

toNormalization_normalizationSourceIso_hom

L58 ↗
EtaleFundamentalGroups.Inertia.toNormalization_normalizationSourceIso_hom
Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
variable {A B S : Scheme.{u}}
variable (f : A ⟶ S) (g : B ⟶ S)
variable [QuasiCompact f] [QuasiSeparated f] [QuasiCompact g] [QuasiSeparated g]
variable (e : A ≅ B) (he : e.hom ≫ g = f)
Lean source · statement
theorem toNormalization_normalizationSourceIso_hom :
    f.toNormalization ≫ (normalizationSourceIso f g e he).hom =
      e.hom ≫ g.toNormalization
theorem

normalizationSourceIso_hom_fromNormalization

L65 ↗
EtaleFundamentalGroups.Inertia.normalizationSourceIso_hom_fromNormalization
Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
variable {A B S : Scheme.{u}}
variable (f : A ⟶ S) (g : B ⟶ S)
variable [QuasiCompact f] [QuasiSeparated f] [QuasiCompact g] [QuasiSeparated g]
variable (e : A ≅ B) (he : e.hom ≫ g = f)
Lean source · statement
theorem normalizationSourceIso_hom_fromNormalization :
    (normalizationSourceIso f g e he).hom ≫ g.fromNormalization = f.fromNormalization
theorem

normalizationSourceIso_hom_endomorphism

L73 ↗
EtaleFundamentalGroups.Inertia.normalizationSourceIso_hom_endomorphism
Documentation

Extending commuting endomorphisms preserves their commutation with the actual source isomorphism.

Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
variable {A B S : Scheme.{u}}
variable (f : A ⟶ S) (g : B ⟶ S)
variable [QuasiCompact f] [QuasiSeparated f] [QuasiCompact g] [QuasiSeparated g]
variable (e : A ≅ B) (he : e.hom ≫ g = f)
Lean source · statement
theorem normalizationSourceIso_hom_endomorphism
    (sigma : A ⟶ A) (hsigma : sigma ≫ f = f)
    (tau : B ⟶ B) (htau : tau ≫ g = g)
    (hcommute : sigma ≫ e.hom = e.hom ≫ tau) :
    normalizationEndomorphism f sigma hsigma ≫ (normalizationSourceIso f g e he).hom =
      (normalizationSourceIso f g e he).hom ≫ normalizationEndomorphism g tau htau
theorem

normalizationSourceIso_fixes_iff

L91 ↗
EtaleFundamentalGroups.Inertia.normalizationSourceIso_fixes_iff
Documentation

The resulting comparison preserves exact fixed geometric-point morphisms.

Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
variable {A B S : Scheme.{u}}
variable (f : A ⟶ S) (g : B ⟶ S)
variable [QuasiCompact f] [QuasiSeparated f] [QuasiCompact g] [QuasiSeparated g]
variable (e : A ≅ B) (he : e.hom ≫ g = f)
Lean source · statement
theorem normalizationSourceIso_fixes_iff
    {T : Scheme.{u}} (z : T ⟶ f.normalization)
    (sigma : A ⟶ A) (hsigma : sigma ≫ f = f)
    (tau : B ⟶ B) (htau : tau ≫ g = g)
    (hcommute : sigma ≫ e.hom = e.hom ≫ tau) :
    (z ≫ (normalizationSourceIso f g e he).hom) ≫ normalizationEndomorphism g tau htau =
        z ≫ (normalizationSourceIso f g e he).hom ↔
      z ≫ normalizationEndomorphism f sigma hsigma = z

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.