NYLL
Module

FiniteCurveBoundaryMap.lean

Nyll.AlgebraicCurves.Models.FiniteCurveBoundaryMap
7 declarations indexed from sourceView source ↗

Module documentation

The actual finite curve map and its boundary places

Imports2
Imported by3

Declarations

def

finiteCurveFieldMap

L30 ↗
AlgebraicCurve.CurveModel.finiteCurveFieldMap
Documentation

The field map of the original finite morphism, retaining its generic stalk construction.

Source context 7 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve
open AlgebraicCurves.Models.Proofs
open CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve
namespace AlgebraicCurve.CurveModel
attribute [local instance] CurveModel.isIntegral CurveModel.isProper CurveModel.smooth
variable {K F E : Type} [Field K] [IsAlgClosed K]
  [Field F] [Field E] [Algebra K F] [Algebra K E]
  (M : CurveModel K F) (N : CurveModel K E)
  (d : N.C ⟶ M.C) (hd : d ≫ M.toBase = N.toBase)
  [IsFinite d] (hsurj : Function.Surjective d)
Lean source · statement
def finiteCurveFieldMap : F →ₐ[K] E
theorem

finiteCurveFieldMap_integral

L35 ↗
AlgebraicCurve.CurveModel.finiteCurveFieldMap_integral
Documentation

The actual finite curve map induces an integral extension of function fields.

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve
open AlgebraicCurves.Models.Proofs
open CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve
namespace AlgebraicCurve.CurveModel
attribute [local instance] CurveModel.isIntegral CurveModel.isProper CurveModel.smooth
variable {K F E : Type} [Field K] [IsAlgClosed K]
  [Field F] [Field E] [Algebra K F] [Algebra K E]
  (M : CurveModel K F) (N : CurveModel K E)
  (d : N.C ⟶ M.C) (hd : d ≫ M.toBase = N.toBase)
  [IsFinite d] (hsurj : Function.Surjective d)
omit [IsAlgClosed K] in
Lean source · statement
theorem finiteCurveFieldMap_integral :
    (M.finiteCurveFieldMap N d hd hsurj).toRingHom.IsIntegral
theorem

finiteCurveFieldMap_finite

L41 ↗
AlgebraicCurve.CurveModel.finiteCurveFieldMap_finite
Documentation

The actual induced function-field extension is finite.

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve
open AlgebraicCurves.Models.Proofs
open CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve
namespace AlgebraicCurve.CurveModel
attribute [local instance] CurveModel.isIntegral CurveModel.isProper CurveModel.smooth
variable {K F E : Type} [Field K] [IsAlgClosed K]
  [Field F] [Field E] [Algebra K F] [Algebra K E]
  (M : CurveModel K F) (N : CurveModel K E)
  (d : N.C ⟶ M.C) (hd : d ≫ M.toBase = N.toBase)
  [IsFinite d] (hsurj : Function.Surjective d)
omit [IsAlgClosed K] in
Lean source · statement
theorem finiteCurveFieldMap_finite :
    FiniteAlong K (M.finiteCurveFieldMap N d hd hsurj)
theorem

finiteCurveFieldMap_generic

L47 ↗
AlgebraicCurve.CurveModel.finiteCurveFieldMap_generic
Documentation

The induced function-field map agrees with the original generic-point morphism.

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve
open AlgebraicCurves.Models.Proofs
open CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve
namespace AlgebraicCurve.CurveModel
attribute [local instance] CurveModel.isIntegral CurveModel.isProper CurveModel.smooth
variable {K F E : Type} [Field K] [IsAlgClosed K]
  [Field F] [Field E] [Algebra K F] [Algebra K E]
  (M : CurveModel K F) (N : CurveModel K E)
  (d : N.C ⟶ M.C) (hd : d ≫ M.toBase = N.toBase)
  [IsFinite d] (hsurj : Function.Surjective d)
omit [IsAlgClosed K] [IsFinite d] in
Lean source · statement
theorem finiteCurveFieldMap_generic :
    N.C.fromSpecStalk (genericPoint N.C) ≫ d =
      Spec.map (CommRingCat.ofHom (N.ffEquiv.toRingHom.comp
        ((M.finiteCurveFieldMap N d hd hsurj).toRingHom.comp M.ffEquiv.symm.toRingHom))) ≫
          M.C.fromSpecStalk (genericPoint M.C)
theorem

pointEquivPlace_symm_closedPoint

L70 ↗
AlgebraicCurve.CurveModel.pointEquivPlace_symm_closedPoint
Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve
open AlgebraicCurves.Models.Proofs
open CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve
namespace AlgebraicCurve.CurveModel
attribute [local instance] CurveModel.isIntegral CurveModel.isProper CurveModel.smooth
variable {K F E : Type} [Field K] [IsAlgClosed K]
  [Field F] [Field E] [Algebra K F] [Algebra K E]
  (M : CurveModel K F) (N : CurveModel K E)
  (d : N.C ⟶ M.C) (hd : d ≫ M.toBase = N.toBase)
  [IsFinite d] (hsurj : Function.Surjective d)
omit [IsFinite d] in
Lean source · statement
theorem pointEquivPlace_symm_closedPoint
    (P : CurveModel K E) (w : Place K E) :
    (P.pointEquivPlace.symm w).val (IsLocalRing.closedPoint K) =
      (P.placeEquiv.symm w).val
theorem

openBoundaryPlaces_eq_restrict_preimage

L83 ↗
AlgebraicCurve.CurveModel.openBoundaryPlaces_eq_restrict_preimage
Documentation

Geometric equality of boundaries becomes the literal preimage of places under the actual extension map.

Source context 7 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve
open AlgebraicCurves.Models.Proofs
open CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve
namespace AlgebraicCurve.CurveModel
attribute [local instance] CurveModel.isIntegral CurveModel.isProper CurveModel.smooth
variable {K F E : Type} [Field K] [IsAlgClosed K]
  [Field F] [Field E] [Algebra K F] [Algebra K E]
  (M : CurveModel K F) (N : CurveModel K E)
  (d : N.C ⟶ M.C) (hd : d ≫ M.toBase = N.toBase)
  [IsFinite d] (hsurj : Function.Surjective d)
Lean source · full declaration
theorem openBoundaryPlaces_eq_restrict_preimage
    {X Y : Scheme} (j : X ⟶ M.C) (k : Y ⟶ N.C)
    (hboundary : ∀ y : N.C, y ∉ Set.range k ↔ d y ∉ Set.range j) :
    N.openBoundaryPlaces k =
      (fun w : Place K E => w.restrictAlong
        (M.finiteCurveFieldMap N d hd hsurj)
        (M.finiteCurveFieldMap_integral N d hd hsurj)) ⁻¹'
          M.openBoundaryPlaces j := by
  ext w
  let φ := M.finiteCurveFieldMap N d hd hsurj
  let hφ := M.finiteCurveFieldMap_integral N d hd hsurj
  have hpoint := FFLeg.point_compat K M N d hd hsurj w
  have heval := congrArg (fun q => q (IsLocalRing.closedPoint K)) hpoint
  have hM : (M.pointEquivPlace.symm (w.restrictAlong φ hφ)).val
      (IsLocalRing.closedPoint K) = (M.placeEquiv.symm (w.restrictAlong φ hφ)).val := by
    exact pointEquivPlace_symm_closedPoint M _
  have hN := pointEquivPlace_symm_closedPoint N w
  change (M.pointEquivPlace.symm (w.restrictAlong φ hφ)).val
      (IsLocalRing.closedPoint K) =
    d ((N.pointEquivPlace.symm w).val (IsLocalRing.closedPoint K)) at heval
  rw [hM, hN] at heval
  change (N.placeEquiv.symm w).val ∉ Set.range k ↔
    (M.placeEquiv.symm (w.restrictAlong φ hφ)).val ∉ Set.range j
  rw [heval]
  exact hboundary _
theorem

finiteCurveFieldMap_unramified_on_open

L111 ↗
AlgebraicCurve.CurveModel.finiteCurveFieldMap_unramified_on_open
Documentation

Interior ramification is obtained from the actual unramified open restriction of this same finite morphism.

Source context 7 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve
open AlgebraicCurves.Models.Proofs
open CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve
namespace AlgebraicCurve.CurveModel
attribute [local instance] CurveModel.isIntegral CurveModel.isProper CurveModel.smooth
variable {K F E : Type} [Field K] [IsAlgClosed K]
  [Field F] [Field E] [Algebra K F] [Algebra K E]
  (M : CurveModel K F) (N : CurveModel K E)
  (d : N.C ⟶ M.C) (hd : d ≫ M.toBase = N.toBase)
  [IsFinite d] (hsurj : Function.Surjective d)
Lean source · statement
theorem finiteCurveFieldMap_unramified_on_open
    {Y : Scheme} (k : Y ⟶ N.C) [IsOpenImmersion k]
    [FormallyUnramified (k ≫ d)]
    (w : Place K E) (hw : w ∉ N.openBoundaryPlaces k) :
    Place.ramificationIndexAlong (M.finiteCurveFieldMap N d hd hsurj) w = 1

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.