AlgebraicCurve.exists_transcendental_mem_range_stalk_iff_ne
Source context 18 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_transcendental_mem_range_stalk_iff_ne
attribute [-instance] AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
attribute [-instance] AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
attribute [-instance] AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
attribute [-instance] AlgebraicCurve.Place.instIsLocalHomRestrictInclusion
attribute [-instance] AlgebraicCurve.Place.instIsPrimeCenter
attribute [-instance] AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance] AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
attribute [-instance]
instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
attribute [-instance] AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Divisor.mapRestrict_single
AlgebraicCurve.Divisor.pushforward_single AlgebraicCurve.Place.coe_restrictInclusion
AlgebraicCurve.Place.mem_fiber AlgebraicCurve.Place.restrict_toValuationSubring
AlgebraicCurve.Divisor.degree_pushforward AlgebraicCurve.Place.restrictResidueMap_residue
AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
AlgebraicCurve.Place.congrEquiv_symm_apply
AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
AlgebraicCurve.Place.differentialCoeff_zero AlgebraicCurve.Place.differentialCoeff_dCoord
AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec AlgebraicCurve.IntegralBasisInLSpace.mk.injEq
AlgebraicCurve.TranscendenceTower.mk.injEq AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
open CategoryTheory AlgebraicGeometry AlgebraicCurve
universe uLean source · full declaration
theorem _root_.AlgebraicCurve.exists_transcendental_mem_range_stalk_iff_ne
{K : Type u} [Field K] [IsAlgClosed K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
[IsIntegral C] [IsSeparated c] [SmoothOfRelativeDimension 1 c]
(Q : C) (hQ : IsClosed ({Q} : Set C)) :
letI := (AlgebraicCurve.baseToFunctionField c).toAlgebra
∃ f : C.functionField, Transcendental K f ∧
∀ x : C, f ∈ (algebraMap (C.presheaf.stalk x) C.functionField).range ↔ x ≠ Q := by
let hKF : Algebra K C.functionField := (AlgebraicCurve.baseToFunctionField c).toAlgebra
have : IsCurveOver K C.functionField :=
AlgebraicCurve.isCurveOver_of_isIntegral_of_smoothOfRelativeDimension_one c
(RingEquiv.refl _) (fun _ => rfl)
have := SmoothOfRelativeDimension.smooth 1 c
have : LocallyOfFiniteType c := inferInstance
have : Algebra.EssFiniteType K C.functionField := AlgebraicCurve.essFiniteType_functionField c
obtain ⟨vQ, hvQ⟩ := AlgebraicCurve.exists_place_range_stalk_eq c Q hQ
have hC : ConstantsAreBase K C.functionField :=
AlgebraicCurve.constantsAreBase_of_deg_eq_one vQ (IsCurveOver.deg_eq_one_of_isAlgClosed vQ)
obtain ⟨f, hfQ, hfw⟩ := AlgebraicCurve.Place.exists_not_mem_and_forall_ne_mem hC vQ
refine ⟨f, ?_, ?_⟩
· intro halg
apply hfQ
obtain ⟨a, ha⟩ := minpoly.mem_range_of_degree_eq_one K f
(IsAlgClosed.degree_eq_one_of_irreducible K (minpoly.irreducible halg.isIntegral))
rw [← ha]
exact vQ.algebraMap_mem' a
· intro x
constructor
· rintro hx rfl
rw [hvQ] at hx
exact hfQ hx
· intro hx
by_cases hxc : IsClosed ({x} : Set C)
· obtain ⟨vx, hvx⟩ := AlgebraicCurve.exists_place_range_stalk_eq c x hxc
have hne : vx ≠ vQ := by
intro h
exact hx (AlgebraicCurve.eq_of_range_stalk_eq c x Q (by rw [hvx, hvQ, h]))
change f ∈ (algebraMap (C.presheaf.stalk x) C.functionField).range
rw [hvx]
exact hfw vx hne
· have hxg : x = genericPoint C := by
by_contra h
exact hxc (AlgebraicCurve.isClosed_singleton_of_ne_genericPoint c x h)
subst hxg
refine ⟨f, ?_⟩
change (C.presheaf.stalkSpecializes (genericPoint_specializes (genericPoint C))).hom f = f
have : C.presheaf.stalkSpecializes (genericPoint_specializes (genericPoint C)) = 𝟙 _ :=
TopCat.Presheaf.stalkSpecializes_refl _ _
rw [this]
rfl