AlgebraicCurve.isAffineOpen_of_maximal_domain
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.IsAffineOpen_of_maximal_domain
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.PolynomialLean source · full declaration
theorem _root_.AlgebraicCurve.isAffineOpen_of_maximal_domain
{k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
[IsIntegral C] [IsProper c] [SmoothOfRelativeDimension 1 c]
(U : C.Opens) [Nonempty U] (s : Γ(C, U))
(hU : ∀ x : C, C.germToFunctionField U s ∈
(algebraMap (C.presheaf.stalk x) C.functionField).range → x ∈ U)
(hs : letI := (AlgebraicCurve.baseToFunctionField c).toAlgebra
Transcendental k (C.germToFunctionField U s)) :
IsAffineOpen U := by
let φ : (U : Scheme.{u}) ⟶ Spec (CommRingCat.of k[X]) :=
(U : Scheme.{u}).toSpecΓ ≫ Spec.map (CommRingCat.ofHom
(Polynomial.eval₂RingHom ((U.ι ≫ c).appTop.hom.comp (Scheme.ΓSpecIso
(CommRingCat.of k)).inv.hom)
(U.topIso.inv s)))
have : IsProper φ := Scheme.Opens.isProper_toSpecPolynomial_of_maximal c
(valuationRing_stalk_of_smoothOfRelativeDimension_one c) U s hU
have : LocallyQuasiFinite φ := LocallyQuasiFinite.of_finite_preimage_singleton φ
(Scheme.Opens.finite_preimage_singleton_toSpecPolynomial c U s hs)
have : IsFinite φ := IsFinite.of_isProper_of_locallyQuasiFinite φ
exact isAffine_of_isAffineHom φ