Module

Range_algebraMap_functionField_eq_iInf_of_isAffineOpen.lean

Nyll.AlgebraicCurves.Models.Range_algebraMap_functionField_eq_iInf_of_isAffineOpen

1 declaration indexed from sourceView source ↗

Module documentation

Range algebraMap functionField eq iInf of isAffineOpen

The image of the coordinate ring of an affine curve open is the intersection of its local valuation subrings in the function field.

Imports5

Imported by11

theorem

range_algebraMap_functionField_eq_iInf_of_isAffineOpen

L34 ↗

AlgebraicCurve.range_algebraMap_functionField_eq_iInf_of_isAffineOpen

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Range_algebraMap_functionField_eq_iInf_of_isAffineOpen
open CategoryTheory AlgebraicGeometry AlgebraicCurve
universe u

Lean source · full declaration

theorem _root_.AlgebraicCurve.range_algebraMap_functionField_eq_iInf_of_isAffineOpen
    {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
    [IsIntegral C] [SmoothOfRelativeDimension 1 c]
    (U : C.Opens) (hU : IsAffineOpen U) [Nonempty U] :
    letI := (AlgebraicCurve.baseToFunctionField c).toAlgebra
    (algebraMap Γ(C, U) C.functionField).range =
      ⨅ (v : AlgebraicCurve.Place K C.functionField)
        (_ : ∃ x : C, x ∈ U ∧ IsClosed ({x} : Set C) ∧
          (algebraMap (C.presheaf.stalk x) C.functionField).range =
            v.toValuationSubring.toSubring),
        v.toValuationSubring.toSubring := by
  let := (AlgebraicCurve.baseToFunctionField c).toAlgebra
  rw [hU.range_algebraMap_functionField_eq_iInf]
  apply le_antisymm
  · refine le_iInf₂ fun v hv => ?_
    obtain ⟨x, hxU, -, hrange⟩ := hv
    rw [← hrange]
    exact iInf₂_le x hxU
  · refine le_iInf₂ fun x hxU => ?_
    by_cases hη : x = genericPoint C
    · subst hη
      intro f _
      refine ⟨f, ?_⟩
      change (C.presheaf.stalkSpecializes (specializes_refl _)).hom f = f
      rw [TopCat.Presheaf.stalkSpecializes_refl]
      rfl
    · have hxcl : IsClosed ({x} : Set C) := isClosed_singleton_of_ne_genericPoint c x hη
      obtain ⟨v, hv⟩ := exists_place_range_stalk_eq c x hxcl
      rw [hv]
      exact iInf₂_le v ⟨x, hxU, hxcl, hv⟩

Module documentation

Range algebraMap functionField eq iInf of isAffineOpen

Declarations

range_algebraMap_functionField_eq_iInf_of_isAffineOpen