Module

BoundaryStrictLocalModel.lean

Nyll.Yamaguchi26SolvableCoverings.Geometry.BoundaryStrictLocalModel

8 declarations indexed from sourceView source ↗

Module documentation

The canonical strict local model at a boundary component

The shared component generic point and the manuscript component point agree by the proved generic-point equation. Transporting the actual local-ring results along that equation gives the domain and DVR structures used here. All strict-local maps use the manuscript's original component point and its original residue-field algebraic closure.

Imports6

Imported by3

theorem

isDomain_stalk_componentPoint

L34 ↗

Yamaguchi26SolvableCoverings.isDomain_stalk_componentPoint

Documentation

The original component point has a domain stalk.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open EtaleFundamentalGroups EtaleFundamentalGroups.StrictHenselian
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]

Lean source · statement

theorem isDomain_stalk_componentPoint
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport) (E : Component D) :
    IsDomain (X.presheaf.stalk (componentPoint D E))

theorem

isDiscreteValuationRing_stalk_componentPoint

L42 ↗

Yamaguchi26SolvableCoverings.isDiscreteValuationRing_stalk_componentPoint

Documentation

The original component point has a DVR stalk.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open EtaleFundamentalGroups EtaleFundamentalGroups.StrictHenselian
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]

Lean source · full declaration

theorem isDiscreteValuationRing_stalk_componentPoint
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport) (E : Component D) :
    let : IsDomain (X.presheaf.stalk (componentPoint D E)) :=
      isDomain_stalk_componentPoint D hreg E
    IsDiscreteValuationRing (X.presheaf.stalk (componentPoint D E)) := by
  intro hDomain
  have hlocal : ∃ h : IsDomain (X.presheaf.stalk (componentPoint D E)),
      let : IsDomain (X.presheaf.stalk (componentPoint D E)) := h
      IsDiscreteValuationRing (X.presheaf.stalk (componentPoint D E)) := by
    apply Eq.mp (congrArg (fun x : X => ∃ h : IsDomain (X.presheaf.stalk x),
      let : IsDomain (X.presheaf.stalk x) := h
      IsDiscreteValuationRing (X.presheaf.stalk x))
        (D.1.componentGenericPoint_eq E.val E.property))
    exact ⟨isDomain_stalk_componentGenericPoint D hreg E.val E.property,
      isDiscreteValuationRing_stalk_componentGenericPoint D hreg E.val E.property⟩
  obtain ⟨_, h⟩ := hlocal
  exact h

def

boundaryComponentResidueMap

L61 ↗

Yamaguchi26SolvableCoverings.boundaryComponentResidueMap

Documentation

The actual closed geometric point map into the prescribed algebraic closure.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open EtaleFundamentalGroups EtaleFundamentalGroups.StrictHenselian
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]

Lean source · statement

def boundaryComponentResidueMap (D : X.EffectiveCartierDivisor) (E : Component D) :
    X.presheaf.stalk (componentPoint D E) →+*
      AlgebraicClosure (X.residueField (componentPoint D E))

instance

boundaryComponentResidueMap_isLocalHom

L68 ↗

Yamaguchi26SolvableCoverings.boundaryComponentResidueMap_isLocalHom

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open EtaleFundamentalGroups EtaleFundamentalGroups.StrictHenselian
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]

Lean source · statement

instance boundaryComponentResidueMap_isLocalHom
    (D : X.EffectiveCartierDivisor) (E : Component D) :
    IsLocalHom (boundaryComponentResidueMap D E)

abbrev

boundaryStrictFractionField

L84 ↗

Yamaguchi26SolvableCoverings.boundaryStrictFractionField

Documentation

The fraction ring of the actual geometric etale stalk at the component.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open EtaleFundamentalGroups EtaleFundamentalGroups.StrictHenselian
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]

Lean source · statement

abbrev boundaryStrictFractionField (D : X.EffectiveCartierDivisor) (E : Component D)

def

boundaryStrictFractionFieldField

L88 ↗

Yamaguchi26SolvableCoverings.boundaryStrictFractionFieldField

Documentation

Its canonical field structure is supplied by the actual DVR stalk theorem.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open EtaleFundamentalGroups EtaleFundamentalGroups.StrictHenselian
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]

Lean source · statement

def boundaryStrictFractionFieldField
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport) (E : Component D) :
    Field (boundaryStrictFractionField D E)

def

boundaryStrictGenericMorphism

L98 ↗

Yamaguchi26SolvableCoverings.boundaryStrictGenericMorphism

Documentation

The canonical strict generic morphism into the original complement.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open EtaleFundamentalGroups EtaleFundamentalGroups.StrictHenselian
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]

Lean source · full declaration

def boundaryStrictGenericMorphism
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport) (E : Component D) :
    let : Field (boundaryStrictFractionField D E) := boundaryStrictFractionFieldField D hreg E
    Spec (.of (boundaryStrictFractionField D E)) ⟶ D.1.supportComplement := by
  intro hField
  let : IsDomain (X.presheaf.stalk (componentPoint D E)) :=
    isDomain_stalk_componentPoint D hreg E
  let : IsDiscreteValuationRing (X.presheaf.stalk (componentPoint D E)) :=
    isDiscreteValuationRing_stalk_componentPoint D hreg E
  exact geometricStalkFractionFieldToComplement D (componentPoint D E)
    (boundaryComponentResidueMap D E)

def

boundaryStrictGenericPoint

L111 ↗

Yamaguchi26SolvableCoverings.boundaryStrictGenericPoint

Documentation

The canonical geometric point of the strict fraction field.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open EtaleFundamentalGroups EtaleFundamentalGroups.StrictHenselian
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]

Lean source · full declaration

def boundaryStrictGenericPoint
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport) (E : Component D) :
    let : Field (boundaryStrictFractionField D E) := boundaryStrictFractionFieldField D hreg E
    Spec (.of (AlgebraicClosure (boundaryStrictFractionField D E))) ⟶
      Spec (.of (boundaryStrictFractionField D E)) := by
  intro hField
  exact Spec.map (CommRingCat.ofHom (algebraMap (boundaryStrictFractionField D E)
    (AlgebraicClosure (boundaryStrictFractionField D E))))

Module documentation

The canonical strict local model at a boundary component

Declarations