Documentation

Mathlib.AlgebraicGeometry.Normalization

Relative Normalization #

Given a qcqs morphism f : X ⟶ Y, we define the relative normalization f.normalization, along with the maps that f factor into:

TODO #

source
def AlgebraicGeometry.Scheme.Hom.normalizationDiagram {X Y : Scheme} (f : X ⟶ Y) :
CategoryTheory.Functor Y.Opensᵒᵖ CommRingCat

Given a morphism f : X ⟶ Y, this is the presheaf of integral closure of Y in X.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def AlgebraicGeometry.Scheme.Hom.normalizationDiagramMap {X Y : Scheme} (f : X ⟶ Y) :
    Y.presheaf ⟶ normalizationDiagram f

    The inclusion from the structure presheaf of Y to the integral closure of Y in X.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem AlgebraicGeometry.Scheme.Hom.isCompact_preimage {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] {U : Y.Opens} (hU : IsCompact ↑U) :
      IsCompact ↑((TopologicalSpace.Opens.map f.base).obj U)
      source
      theorem AlgebraicGeometry.Scheme.Hom.isQuasiSeparated_preimage {X Y : Scheme} (f : X ⟶ Y) [QuasiSeparated f] {U : Y.Opens} (hU : IsQuasiSeparated ↑U) :
      IsQuasiSeparated ↑((TopologicalSpace.Opens.map f.base).obj U)
      source
      theorem AlgebraicGeometry.Scheme.Hom.preservesLocalization_normalizationDiagramMap {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :
      AffineZariskiSite.PreservesLocalization ((AffineZariskiSite.toOpensFunctor Y).op.comp (normalizationDiagram f)) ((AffineZariskiSite.toOpensFunctor Y).op.whiskerLeft (normalizationDiagramMap f))
      source
      instance AlgebraicGeometry.Scheme.Hom.instIsLocallyDirectedAffineZariskiSiteCompOppositeCommRingCatRightOpOpensOpToOpensFunctorNormalizationDiagramSpecForget {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :
      ((((AffineZariskiSite.toOpensFunctor Y).op.comp (normalizationDiagram f)).rightOp.comp Scheme.Spec).comp forget).IsLocallyDirected
      source
      instance AlgebraicGeometry.Scheme.Hom.instIsOpenImmersionMapAffineZariskiSiteCompOppositeCommRingCatRightOpOpensOpToOpensFunctorNormalizationDiagramSpec {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {U V : Y.AffineZariskiSite} (i : U ⟶ V) :
      IsOpenImmersion ((((AffineZariskiSite.toOpensFunctor Y).op.comp (normalizationDiagram f)).rightOp.comp Scheme.Spec).map i)
      source
      def AlgebraicGeometry.Scheme.Hom.normalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :
      Scheme

      Given f : X ⟶ Y, f.normalization is the relative normalization of Y in X.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def AlgebraicGeometry.Scheme.Hom.normalizationOpenCover {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :
        (normalization f).OpenCover

        This is the open cover of f.normalization by Spec of integral closures of Γ(Y, U) in Γ(X, f ⁻¹ U) where U ranges over all affine opens.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def AlgebraicGeometry.Scheme.Hom.toNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :
          X ⟶ normalization f

          The dominant morphism into the relative normalization.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem AlgebraicGeometry.Scheme.Hom.ι_toNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] (U : ↑Y.affineOpens) :
            CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj ↑U).ι (toNormalization f) = CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj ↑U).toSpecΓ (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (integralClosure ↑(Y.presheaf.obj (Opposite.op ↑U)) ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj ↑U)))).val.toRingHom)) ((normalizationOpenCover f).f U))
            source
            theorem AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] (U : ↑Y.affineOpens) {Z : Scheme} (h : normalization f ⟶ Z) :
            CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj ↑U).ι (CategoryTheory.CategoryStruct.comp (toNormalization f) h) = CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj ↑U).toSpecΓ (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (integralClosure ↑(Y.presheaf.obj (Opposite.op ↑U)) ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj ↑U)))).val.toRingHom)) (CategoryTheory.CategoryStruct.comp ((normalizationOpenCover f).f U) h))
            source
            def AlgebraicGeometry.Scheme.Hom.fromNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :
            normalization f ⟶ Y

            The morphism from the relative normalization to itself. This map is integral.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem AlgebraicGeometry.Scheme.Hom.ι_fromNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] (U : ↑Y.affineOpens) :
              CategoryTheory.CategoryStruct.comp ((normalizationOpenCover f).f U) (fromNormalization f) = CategoryTheory.CategoryStruct.comp (Spec.map ((normalizationDiagramMap f).app (Opposite.op ↑U))) (IsAffineOpen.fromSpec ⋯)
              source
              theorem AlgebraicGeometry.Scheme.Hom.ι_fromNormalization_assoc {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] (U : ↑Y.affineOpens) {Z : Scheme} (h : Y ⟶ Z) :
              CategoryTheory.CategoryStruct.comp ((normalizationOpenCover f).f U) (CategoryTheory.CategoryStruct.comp (fromNormalization f) h) = CategoryTheory.CategoryStruct.comp (Spec.map ((normalizationDiagramMap f).app (Opposite.op ↑U))) (CategoryTheory.CategoryStruct.comp (IsAffineOpen.fromSpec ⋯) h)
              source
              theorem AlgebraicGeometry.Scheme.Hom.fromNormalization_preimage {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] (U : ↑Y.affineOpens) :
              (TopologicalSpace.Opens.map (fromNormalization f).base).obj ↑U = opensRange ((normalizationOpenCover f).f U)
              source
              @[simp]
              theorem AlgebraicGeometry.Scheme.Hom.toNormalization_fromNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :
              CategoryTheory.CategoryStruct.comp (toNormalization f) (fromNormalization f) = f
              source
              @[simp]
              theorem AlgebraicGeometry.Scheme.Hom.toNormalization_fromNormalization_assoc {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] {Z : Scheme} (h : Y ⟶ Z) :
              CategoryTheory.CategoryStruct.comp (toNormalization f) (CategoryTheory.CategoryStruct.comp (fromNormalization f) h) = CategoryTheory.CategoryStruct.comp f h
              source
              instance AlgebraicGeometry.Scheme.Hom.instIsIntegralHomFromNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :
              IsIntegralHom (fromNormalization f)
              source
              theorem AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] (U : ↑Y.affineOpens) :
              let this := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra; app (toNormalization f) ((TopologicalSpace.Opens.map (fromNormalization f).base).obj ↑U) = CategoryTheory.CategoryStruct.comp ((normalization f).presheaf.map (CategoryTheory.eqToHom ⋯).op) (CategoryTheory.CategoryStruct.comp (appIso ((normalizationOpenCover f).f U) ⊤).hom (CategoryTheory.CategoryStruct.comp (ΓSpecIso (Opposite.unop (((AffineZariskiSite.toOpensFunctor Y).op.comp (normalizationDiagram f)).rightOp.obj U))).hom (CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (integralClosure ↑(Y.presheaf.obj (Opposite.op ↑U)) ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj ↑U)))).val.toRingHom) (X.presheaf.map (CategoryTheory.eqToHom ⋯).op))))
              source
              instance AlgebraicGeometry.Scheme.Hom.instIsIsoToNormalizationOfIsIntegralHom {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] [IsIntegralHom f] :
              CategoryTheory.IsIso (toNormalization f)

              Stacks Tag 03GP

              source
              instance AlgebraicGeometry.Scheme.Hom.instIsAffineHomToNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] [IsAffineHom f] :
              IsAffineHom (toNormalization f)
              source
              instance AlgebraicGeometry.Scheme.Hom.instQuasiCompactToNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :
              QuasiCompact (toNormalization f)
              source
              instance AlgebraicGeometry.Scheme.Hom.instQuasiSeparatedToNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :
              QuasiSeparated (toNormalization f)
              source
              @[simp]
              theorem AlgebraicGeometry.Scheme.Hom.ker_toNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :
              ker (toNormalization f) = ⊥
              source
              instance AlgebraicGeometry.Scheme.Hom.instIsDominantToNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] :
              IsDominant (toNormalization f)
              source
              instance AlgebraicGeometry.Scheme.Hom.instIsReducedNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] [IsReduced X] :
              IsReduced (normalization f)

              Stacks Tag 0AXN

              source
              instance AlgebraicGeometry.Scheme.Hom.instIsIntegralNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f] [IsIntegral X] :
              IsIntegral (normalization f)