NYLL
Module

NormalizationSquare.lean

Nyll.EtaleFundamentalGroups.Inertia.NormalizationSquare
7 declarations indexed from sourceView source ↗

Module documentation

Relative normalization along an actual commuting square

A commuting square induces a map on relative normalizations, by applying the universal property to the pullback of the target normalization. The map preserves the base and commutes with compatible source endomorphisms.

Imports1
Imported by3

Declarations

def

normalizationSquareLift

L30 ↗
EtaleFundamentalGroups.Inertia.normalizationSquareLift
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 {A B S T : Scheme.{u}}
  (f : A ⟶ S) (g : B ⟶ T) [QuasiCompact f] [QuasiSeparated f]
  [QuasiCompact g] [QuasiSeparated g]
  (a : A ⟶ B) (b : S ⟶ T) (h : a ≫ g = f ≫ b)
Lean source · statement
def normalizationSquareLift :
    f.normalization ⟶ pullback g.fromNormalization b
theorem

normalizationSquareLift_source

L37 ↗
EtaleFundamentalGroups.Inertia.normalizationSquareLift_source
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 {A B S T : Scheme.{u}}
  (f : A ⟶ S) (g : B ⟶ T) [QuasiCompact f] [QuasiSeparated f]
  [QuasiCompact g] [QuasiSeparated g]
  (a : A ⟶ B) (b : S ⟶ T) (h : a ≫ g = f ≫ b)
Lean source · full declaration
theorem normalizationSquareLift_source :
    f.toNormalization ≫ normalizationSquareLift f g a b h =
      pullback.lift (a ≫ g.toNormalization) f (by
        rw [Category.assoc, Scheme.Hom.toNormalization_fromNormalization, h]) :=
  Scheme.Hom.toNormalization_normalizationDesc _ _ _ _
theorem

normalizationSquareLift_base

L43 ↗
EtaleFundamentalGroups.Inertia.normalizationSquareLift_base
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 {A B S T : Scheme.{u}}
  (f : A ⟶ S) (g : B ⟶ T) [QuasiCompact f] [QuasiSeparated f]
  [QuasiCompact g] [QuasiSeparated g]
  (a : A ⟶ B) (b : S ⟶ T) (h : a ≫ g = f ≫ b)
Lean source · statement
theorem normalizationSquareLift_base :
    normalizationSquareLift f g a b h ≫ pullback.snd g.fromNormalization b =
      f.fromNormalization
def

normalizationMapOfSquare

L49 ↗
EtaleFundamentalGroups.Inertia.normalizationMapOfSquare
Documentation

The normalization map induced by a displayed commuting square.

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 {A B S T : Scheme.{u}}
  (f : A ⟶ S) (g : B ⟶ T) [QuasiCompact f] [QuasiSeparated f]
  [QuasiCompact g] [QuasiSeparated g]
  (a : A ⟶ B) (b : S ⟶ T) (h : a ≫ g = f ≫ b)
Lean source · statement
def normalizationMapOfSquare : f.normalization ⟶ g.normalization
theorem

normalizationMapOfSquare_source

L53 ↗
EtaleFundamentalGroups.Inertia.normalizationMapOfSquare_source
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 {A B S T : Scheme.{u}}
  (f : A ⟶ S) (g : B ⟶ T) [QuasiCompact f] [QuasiSeparated f]
  [QuasiCompact g] [QuasiSeparated g]
  (a : A ⟶ B) (b : S ⟶ T) (h : a ≫ g = f ≫ b)
Lean source · statement
theorem normalizationMapOfSquare_source :
    f.toNormalization ≫ normalizationMapOfSquare f g a b h =
      a ≫ g.toNormalization
theorem

normalizationMapOfSquare_base

L60 ↗
EtaleFundamentalGroups.Inertia.normalizationMapOfSquare_base
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 {A B S T : Scheme.{u}}
  (f : A ⟶ S) (g : B ⟶ T) [QuasiCompact f] [QuasiSeparated f]
  [QuasiCompact g] [QuasiSeparated g]
  (a : A ⟶ B) (b : S ⟶ T) (h : a ≫ g = f ≫ b)
Lean source · statement
theorem normalizationMapOfSquare_base :
    normalizationMapOfSquare f g a b h ≫ g.fromNormalization =
      f.fromNormalization ≫ b
theorem

normalizationMapOfSquare_endomorphism

L69 ↗
EtaleFundamentalGroups.Inertia.normalizationMapOfSquare_endomorphism
Documentation

The induced normalization map intertwines actual compatible source endomorphisms. No comparison of the induced actions is assumed.

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 {A B S T : Scheme.{u}}
  (f : A ⟶ S) (g : B ⟶ T) [QuasiCompact f] [QuasiSeparated f]
  [QuasiCompact g] [QuasiSeparated g]
  (a : A ⟶ B) (b : S ⟶ T) (h : a ≫ g = f ≫ b)
Lean source · statement
theorem normalizationMapOfSquare_endomorphism
    (τ : A ⟶ A) (hτ : τ ≫ f = f)
    (σ : B ⟶ B) (hσ : σ ≫ g = g)
    (he : τ ≫ a = a ≫ σ) :
    normalizationEndomorphism f τ hτ ≫ normalizationMapOfSquare f g a b h =
      normalizationMapOfSquare f g a b h ≫ normalizationEndomorphism g σ hσ

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