Module

SupportComplementFunctionField.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.SupportComplementFunctionField

3 declarations indexed from sourceView source ↗

Module documentation

Function fields of divisor complements

The function field of the open complement of an ideal sheaf is the ambient function field. The algebra structure below remembers the canonical map from a chosen ambient stalk, which is needed for normalization at a boundary prime.

Imports2

Imported by2

def

supportComplementFunctionFieldAlgebra

L32 ↗

AlgebraicGeometry.Scheme.IdealSheafData.supportComplementFunctionFieldAlgebra

Documentation

The canonical algebra structure from an ambient stalk to the function field of the support complement.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X : Scheme.{u}} [IsIntegral X]

Lean source · statement

def supportComplementFunctionFieldAlgebra
    (I : X.IdealSheafData) [Nonempty I.supportComplement]
    (x : X) : Algebra (X.presheaf.stalk x)
      (I.supportComplement : Scheme).functionField

def

supportComplementFunctionFieldAlgEquiv

L41 ↗

AlgebraicGeometry.Scheme.IdealSheafData.supportComplementFunctionFieldAlgEquiv

Documentation

The canonical open-immersion function-field equivalence, as an equivalence over the chosen ambient stalk.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X : Scheme.{u}} [IsIntegral X]

Lean source · full declaration

def supportComplementFunctionFieldAlgEquiv
    (I : X.IdealSheafData) [Nonempty I.supportComplement]
    (x : X) :
    letI : Algebra (X.presheaf.stalk x)
        (I.supportComplement : Scheme).functionField :=
      I.supportComplementFunctionFieldAlgebra x
    X.functionField ≃ₐ[X.presheaf.stalk x]
      (I.supportComplement : Scheme).functionField := by
  letI : Algebra (X.presheaf.stalk x)
      (I.supportComplement : Scheme).functionField :=
    I.supportComplementFunctionFieldAlgebra x
  exact AlgEquiv.ofRingEquiv
    (f := I.supportComplement.ι.functionFieldRingEquivOfIsOpenImmersion) (by
      intro a
      change
        I.supportComplement.ι.functionFieldRingEquivOfIsOpenImmersion
            (algebraMap (X.presheaf.stalk x) X.functionField a) =
          I.supportComplement.ι.functionFieldRingEquivOfIsOpenImmersion
            (algebraMap (X.presheaf.stalk x) X.functionField a)
      rfl)

theorem

supportComplementFunctionField_isFractionRing

L64 ↗

AlgebraicGeometry.Scheme.IdealSheafData.supportComplementFunctionField_isFractionRing

Documentation

The complement function field is a fraction field of every ambient stalk, through the canonical open-immersion map.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X : Scheme.{u}} [IsIntegral X]

Lean source · full declaration

theorem supportComplementFunctionField_isFractionRing
    (I : X.IdealSheafData) [Nonempty I.supportComplement]
    (x : X) :
    letI : Algebra (X.presheaf.stalk x)
        (I.supportComplement : Scheme).functionField :=
      I.supportComplementFunctionFieldAlgebra x
    IsFractionRing (X.presheaf.stalk x)
      (I.supportComplement : Scheme).functionField := by
  let : Algebra (X.presheaf.stalk x)
      (I.supportComplement : Scheme).functionField :=
    I.supportComplementFunctionFieldAlgebra x
  exact IsFractionRing.of_algEquiv
    (I.supportComplementFunctionFieldAlgEquiv x)

Module documentation

Function fields of divisor complements

Declarations

supportComplementFunctionFieldAlgebra

supportComplementFunctionFieldAlgEquiv

supportComplementFunctionField_isFractionRing