Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Hom.normalizationDesc

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

Given an qcqs morphism f : X ⟶ Y, which factors into X ⟶ T ⟶ Y with T ⟶ Y integral, the map X ⟶ T factors through f.normalization uniquely. (See normalization.hom_ext for the uniqueness result)

Defined in

Mathlib.AlgebraicGeometry.Normalization

Cited by

10 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.QuasiCompactAlgebraicGeometry.QuasiSeparatedAlgebraicGeometry.IsIntegralHom