Module

OpenPlaceTransport.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.OpenPlaceTransport

3 declarations indexed from sourceView source ↗

Module documentation

Actual interior places under the open function-field identification

Imports4

Imported by3

theorem

openFunctionFieldEquiv_algebraMap

L26 ↗

AlgebraicCurve.CurveModel.openFunctionFieldEquiv_algebraMap

Documentation

The literal function-field identification of the open curve preserves the scalar map from its actual structure morphism.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace AlgebraicCurve.CurveModel
attribute [local instance] CurveModel.isIntegral CurveModel.isProper CurveModel.smooth
variable {K F : Type} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem openFunctionFieldEquiv_algebraMap
    (M : CurveModel K F) {X : Scheme} [IsIntegral X]
    (j : X ⟶ M.C) [IsOpenImmersion j] (a : K) :
    (M.ffEquiv.trans j.functionFieldRingEquivOfIsOpenImmersion)
        (algebraMap K F a) = baseToFunctionField (j ≫ M.toBase) a

theorem

openFunctionFieldEquiv_mem_stalk_range_iff

L39 ↗

AlgebraicCurve.CurveModel.openFunctionFieldEquiv_mem_stalk_range_iff

Documentation

Membership in the valuation ring at an interior model point is equivalent to membership in the actual local-ring image of the open curve.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace AlgebraicCurve.CurveModel
attribute [local instance] CurveModel.isIntegral CurveModel.isProper CurveModel.smooth
variable {K F : Type} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem openFunctionFieldEquiv_mem_stalk_range_iff
    (M : CurveModel K F) {X : Scheme} [IsIntegral X]
    (j : X ⟶ M.C) [IsOpenImmersion j]
    (x : X) (z : closedPoints M.C) (hz : z.val = j x) (a : F) :
    (M.ffEquiv.trans j.functionFieldRingEquivOfIsOpenImmersion) a ∈
        (algebraMap (X.presheaf.stalk x) X.functionField).range ↔
      a ∈ (M.placeOfPoint z).toValuationSubring

theorem

exists_openPlaceEquiv_stalk_range_ord

L71 ↗

AlgebraicCurve.CurveModel.exists_openPlaceEquiv_stalk_range_ord

Documentation

Every interior place has its transported valuation ring equal to the actual stalk image, and its order function is unchanged. The equivalence of places is obtained from the existing field-isomorphism theorem.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace AlgebraicCurve.CurveModel
attribute [local instance] CurveModel.isIntegral CurveModel.isProper CurveModel.smooth
variable {K F : Type} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

theorem exists_openPlaceEquiv_stalk_range_ord
    (M : CurveModel K F) {X : Scheme} [IsIntegral X]
    (j : X ⟶ M.C) [IsOpenImmersion j] :
    let : Algebra K X.functionField := (baseToFunctionField (j ≫ M.toBase)).toAlgebra
    ∃ Φ : Place K F ≃ Place K X.functionField,
      (∀ (v : Place K F) (a : F),
        (Φ v).ord ((M.ffEquiv.trans j.functionFieldRingEquivOfIsOpenImmersion) a) =
          v.ord a) ∧
      ∀ v : Place K F, v ∉ M.openBoundaryPlaces j →
        ∃ x : closedPoints X,
          (algebraMap (X.presheaf.stalk x.val) X.functionField).range =
            (Φ v).toValuationSubring.toSubring := by
  intro algX
  let e := M.ffEquiv.trans j.functionFieldRingEquivOfIsOpenImmersion
  obtain ⟨Φ, hΦ, hord, _⟩ :=
    Place.exists_equiv_comap_eq_and_ord_eq_and_deg_eq_of_ringEquiv
      (RingEquiv.refl K) e (fun a => M.openFunctionFieldEquiv_algebraMap j a)
  refine ⟨Φ, hord, ?_⟩
  intro v hv
  obtain ⟨x, hx⟩ := M.exists_closedPoint_of_not_mem_openBoundaryPlaces j v hv
  refine ⟨x, ?_⟩
  ext b
  have hmem := M.openFunctionFieldEquiv_mem_stalk_range_iff j x.val
    (M.placeEquiv.symm v) hx.symm (e.symm b)
  change e (e.symm b) ∈ _ ↔ _ at hmem
  rw [e.apply_symm_apply] at hmem
  have hp : M.placeOfPoint (M.placeEquiv.symm v) = v :=
    M.placeEquiv.apply_symm_apply v
  rw [hp] at hmem
  change b ∈ (algebraMap (X.presheaf.stalk x.val) X.functionField).range ↔
    b ∈ (Φ v).toValuationSubring
  rw [hΦ v]
  exact hmem

Module documentation

Actual interior places under the open function-field identification

Declarations

openFunctionFieldEquiv_algebraMap

openFunctionFieldEquiv_mem_stalk_range_iff

exists_openPlaceEquiv_stalk_range_ord