Module

FiniteNormalSource.lean

Nyll.SchemeTheory.Normalization.FiniteNormalSource

8 declarations indexed from sourceView source ↗

Module documentation

A finite normal source is its generic relative normalization

This generalizes the affine integral-closure argument used for finite étale covers to any finite morphism with normal integral source. It applies at ramified boundary points as well. The resulting isomorphism is over the original target, not merely an abstract isomorphism of schemes.

Imports1

Nyll.SchemeTheory.Normalization.FiniteSeparable

Imported by3

instance

fieldSpecQuasiCompact

L28 ↗

AlgebraicGeometry.Scheme.Hom.fieldSpecQuasiCompact

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {X Y : Scheme.{u}} [IsIntegral Y] [IsNormalIntegral Y]

Lean source · full declaration

instance fieldSpecQuasiCompact
    {L : Type u} [Field L] {S : Scheme.{u}} (f : Spec (.of L) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact

def

finiteNormalGenericDesc

L33 ↗

AlgebraicGeometry.Scheme.Hom.finiteNormalGenericDesc

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {X Y : Scheme.{u}} [IsIntegral Y] [IsNormalIntegral Y]
private local instance fieldSpecQuasiCompact
    {L : Type u} [Field L] {S : Scheme.{u}} (f : Spec (.of L) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact

Lean source · statement

def finiteNormalGenericDesc
    (f : Y ⟶ X) [IsFinite f] :
    ((Y.genericExtensionMorphism Y.functionField ≫ f)).normalization ⟶ Y

lemma

finiteNormalGenericDesc_comp

L44 ↗

AlgebraicGeometry.Scheme.Hom.finiteNormalGenericDesc_comp

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {X Y : Scheme.{u}} [IsIntegral Y] [IsNormalIntegral Y]
private local instance fieldSpecQuasiCompact
    {L : Type u} [Field L] {S : Scheme.{u}} (f : Spec (.of L) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
omit [IsNormalIntegral Y] in

Lean source · statement

lemma finiteNormalGenericDesc_comp
    (f : Y ⟶ X) [IsFinite f] :
    finiteNormalGenericDesc f ≫ f =
      ((Y.genericExtensionMorphism Y.functionField ≫ f)).fromNormalization

lemma

toNormalization_finiteNormalGenericDesc

L57 ↗

AlgebraicGeometry.Scheme.Hom.toNormalization_finiteNormalGenericDesc

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {X Y : Scheme.{u}} [IsIntegral Y] [IsNormalIntegral Y]
private local instance fieldSpecQuasiCompact
    {L : Type u} [Field L] {S : Scheme.{u}} (f : Spec (.of L) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
omit [IsNormalIntegral Y] in

Lean source · statement

lemma toNormalization_finiteNormalGenericDesc
    (f : Y ⟶ X) [IsFinite f] :
    ((Y.genericExtensionMorphism Y.functionField ≫ f)).toNormalization ≫
        finiteNormalGenericDesc f =
      (Y.genericExtensionMorphism Y.functionField)

lemma

appLE_preimage_eq_app_of_eq

L70 ↗

AlgebraicGeometry.Scheme.Hom.appLE_preimage_eq_app_of_eq

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {X Y : Scheme.{u}} [IsIntegral Y] [IsNormalIntegral Y]
private local instance fieldSpecQuasiCompact
    {L : Type u} [Field L] {S : Scheme.{u}} (f : Spec (.of L) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact

Lean source · full declaration

lemma appLE_preimage_eq_app_of_eq {Y Z : Scheme.{u}}
    (g q : Y ⟶ Z) (h : g = q) (U : Z.Opens) :
    g.appLE U (q ⁻¹ᵁ U) (by rw [h]) = q.app U := by
  subst q
  exact g.appLE_eq_app

theorem

finiteNormalGenericDesc_isIso

L78 ↗

AlgebraicGeometry.Scheme.Hom.finiteNormalGenericDesc_isIso

Documentation

The canonical map from the generic relative normalization to a finite normal integral source is an isomorphism.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {X Y : Scheme.{u}} [IsIntegral Y] [IsNormalIntegral Y]
private local instance fieldSpecQuasiCompact
    {L : Type u} [Field L] {S : Scheme.{u}} (f : Spec (.of L) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact

Lean source · statement

theorem finiteNormalGenericDesc_isIso
    (f : Y ⟶ X) [IsFinite f] :
    IsIso (finiteNormalGenericDesc f)

def

finiteNormalGenericIso

L218 ↗

AlgebraicGeometry.Scheme.Hom.finiteNormalGenericIso

Documentation

A finite normal integral source is its generic relative normalization.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {X Y : Scheme.{u}} [IsIntegral Y] [IsNormalIntegral Y]
private local instance fieldSpecQuasiCompact
    {L : Type u} [Field L] {S : Scheme.{u}} (f : Spec (.of L) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact

Lean source · statement

def finiteNormalGenericIso
    (f : Y ⟶ X) [IsFinite f] :
    ((Y.genericExtensionMorphism Y.functionField ≫ f)).normalization ≅ Y

theorem

finiteNormalGenericIso_inv_fromNormalization

L226 ↗

AlgebraicGeometry.Scheme.Hom.finiteNormalGenericIso_inv_fromNormalization

Documentation

The generic normalization isomorphism commutes with the original finite map.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {X Y : Scheme.{u}} [IsIntegral Y] [IsNormalIntegral Y]
private local instance fieldSpecQuasiCompact
    {L : Type u} [Field L] {S : Scheme.{u}} (f : Spec (.of L) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact

Lean source · statement

theorem finiteNormalGenericIso_inv_fromNormalization
    (f : Y ⟶ X) [IsFinite f] :
    (finiteNormalGenericIso f).inv ≫
        ((Y.genericExtensionMorphism Y.functionField ≫ f)).fromNormalization =
      f

Module documentation

A finite normal source is its generic relative normalization

Declarations