Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Hom.normalizationObjIso

{X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [inst : AlgebraicGeometry.QuasiCompact f] →
      [inst_1 : AlgebraicGeometry.QuasiSeparated f] →
        {U : Y.Opens} →
          AlgebraicGeometry.IsAffineOpen U →
            ((AlgebraicGeometry.Scheme.Hom.normalization f).presheaf.obj
                (Opposite.op
                  ((TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.Hom.fromNormalization f).base).obj U)) ≅
              CommRingCat.of
                ↥(integralClosure ↑(Y.presheaf.obj (Opposite.op U))
                    ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)))))

The sections of the relative normalization on the preimage of an affine open is isomorphic to the integral closure.

Defined in

Mathlib.AlgebraicGeometry.Normalization

Cited by

6 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.QuasiCompactAlgebraicGeometry.QuasiSeparated