Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Hom.normalization.hom_ext

∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {T : AlgebraicGeometry.Scheme}
  (f₁ f₂ : AlgebraicGeometry.Scheme.Hom.normalization f ⟶ T) (g : T ⟶ Y) [AlgebraicGeometry.IsAffineHom g],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toNormalization f) f₁ =
      CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toNormalization f) f₂ →
    CategoryTheory.CategoryStruct.comp f₁ g = AlgebraicGeometry.Scheme.Hom.fromNormalization f →
      CategoryTheory.CategoryStruct.comp f₂ g = AlgebraicGeometry.Scheme.Hom.fromNormalization f → f₁ = f₂

The uniqueness part of the universal property for relative normalization. Suppose f : X ⟶ Y is qcqs and factors into X ⟶ T ⟶ Y with T ⟶ Y affine, then there is at most one map f.normalization ⟶ T that commutes with them.

Defined in

Mathlib.AlgebraicGeometry.Normalization

Cited by

0 results in Mathlib

Foundations

Depth 225 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AlgebraicGeometry.QuasiCompactAlgebraicGeometry.QuasiSeparatedAlgebraicGeometry.IsAffineHom