Documentation

TauCeti.AlgebraicGeometry.Normalization

Functoriality of the relative normalization #

For quasi-compact quasi-separated morphisms f : Y ⟶ J and g : Y' ⟶ J, a morphism φ : Y ⟶ Y' over J induces a morphism f.normalizationMap g φ hφ : f.normalization ⟶ g.normalization of relative normalizations over J, compatible with the canonical morphisms from Y and Y'.

Main definitions #

Main results #

source
noncomputable def AlgebraicGeometry.Scheme.Hom.normalizationMap {Y Y' J : Scheme} (f : Y ⟶ J) [QuasiCompact f] [QuasiSeparated f] (g : Y' ⟶ J) [QuasiCompact g] [QuasiSeparated g] (φ : Y ⟶ Y') (hφ : CategoryTheory.CategoryStruct.comp φ g = f) :
normalization f ⟶ normalization g

A morphism φ : Y ⟶ Y' over J induces a morphism f.normalization ⟶ g.normalization of relative normalizations over J.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    instance AlgebraicGeometry.Scheme.Hom.instIsIntegralHomNormalizationMap {Y Y' J : Scheme} (f : Y ⟶ J) [QuasiCompact f] [QuasiSeparated f] (g : Y' ⟶ J) [QuasiCompact g] [QuasiSeparated g] (φ : Y ⟶ Y') (hφ : CategoryTheory.CategoryStruct.comp φ g = f) :
    IsIntegralHom (normalizationMap f g φ hφ)
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Hom.normalizationMap_fromNormalization {Y Y' J : Scheme} (f : Y ⟶ J) [QuasiCompact f] [QuasiSeparated f] (g : Y' ⟶ J) [QuasiCompact g] [QuasiSeparated g] (φ : Y ⟶ Y') (hφ : CategoryTheory.CategoryStruct.comp φ g = f) :
    CategoryTheory.CategoryStruct.comp (normalizationMap f g φ hφ) (fromNormalization g) = fromNormalization f

    The morphism of relative normalizations induced by φ lies over J.

    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Hom.normalizationMap_fromNormalization_assoc {Y Y' J : Scheme} (f : Y ⟶ J) [QuasiCompact f] [QuasiSeparated f] (g : Y' ⟶ J) [QuasiCompact g] [QuasiSeparated g] (φ : Y ⟶ Y') (hφ : CategoryTheory.CategoryStruct.comp φ g = f) {Z : Scheme} (h : J ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (normalizationMap f g φ hφ) (CategoryTheory.CategoryStruct.comp (fromNormalization g) h) = CategoryTheory.CategoryStruct.comp (fromNormalization f) h

    The morphism of relative normalizations induced by φ lies over J.

    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationMap {Y Y' J : Scheme} (f : Y ⟶ J) [QuasiCompact f] [QuasiSeparated f] (g : Y' ⟶ J) [QuasiCompact g] [QuasiSeparated g] (φ : Y ⟶ Y') (hφ : CategoryTheory.CategoryStruct.comp φ g = f) :
    CategoryTheory.CategoryStruct.comp (toNormalization f) (normalizationMap f g φ hφ) = CategoryTheory.CategoryStruct.comp φ (toNormalization g)

    The morphism of relative normalizations induced by φ is compatible with the canonical morphisms from Y and Y'.

    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationMap_assoc {Y Y' J : Scheme} (f : Y ⟶ J) [QuasiCompact f] [QuasiSeparated f] (g : Y' ⟶ J) [QuasiCompact g] [QuasiSeparated g] (φ : Y ⟶ Y') (hφ : CategoryTheory.CategoryStruct.comp φ g = f) {Z : Scheme} (h : normalization g ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (toNormalization f) (CategoryTheory.CategoryStruct.comp (normalizationMap f g φ hφ) h) = CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp (toNormalization g) h)

    The morphism of relative normalizations induced by φ is compatible with the canonical morphisms from Y and Y'.

    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Hom.normalizationMap_id {Y J : Scheme} (f : Y ⟶ J) [QuasiCompact f] [QuasiSeparated f] :
    normalizationMap f f (CategoryTheory.CategoryStruct.id Y) ⋯ = CategoryTheory.CategoryStruct.id (normalization f)

    The identity of Y induces the identity of f.normalization.

    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Hom.normalizationMap_comp {Y Y' J : Scheme} (f : Y ⟶ J) [QuasiCompact f] [QuasiSeparated f] (g : Y' ⟶ J) [QuasiCompact g] [QuasiSeparated g] {Y'' : Scheme} (h : Y'' ⟶ J) [QuasiCompact h] [QuasiSeparated h] (φ : Y ⟶ Y') (hφ : CategoryTheory.CategoryStruct.comp φ g = f) (ψ : Y' ⟶ Y'') (hψ : CategoryTheory.CategoryStruct.comp ψ h = g) :
    CategoryTheory.CategoryStruct.comp (normalizationMap f g φ hφ) (normalizationMap g h ψ hψ) = normalizationMap f h (CategoryTheory.CategoryStruct.comp φ ψ) ⋯

    The morphisms of relative normalizations induced by φ and then ψ compose to the one induced by φ ≫ ψ.

    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Hom.normalizationMap_comp_assoc {Y Y' J : Scheme} (f : Y ⟶ J) [QuasiCompact f] [QuasiSeparated f] (g : Y' ⟶ J) [QuasiCompact g] [QuasiSeparated g] {Y'' : Scheme} (h : Y'' ⟶ J) [QuasiCompact h] [QuasiSeparated h] (φ : Y ⟶ Y') (hφ : CategoryTheory.CategoryStruct.comp φ g = f) (ψ : Y' ⟶ Y'') (hψ : CategoryTheory.CategoryStruct.comp ψ h = g) {Z : Scheme} (h✝ : normalization h ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (normalizationMap f g φ hφ) (CategoryTheory.CategoryStruct.comp (normalizationMap g h ψ hψ) h✝) = CategoryTheory.CategoryStruct.comp (normalizationMap f h (CategoryTheory.CategoryStruct.comp φ ψ) ⋯) h✝

    The morphisms of relative normalizations induced by φ and then ψ compose to the one induced by φ ≫ ψ.