AlgebraicCurve.germToFunctionField_mem_lSpaceOn_placesOf
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GermToFunctionField_mem_lSpaceOn_placesOf
attribute [-instance]
AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] 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
open CategoryTheory AlgebraicGeometry AlgebraicCurve
universe uLean source · full declaration
theorem _root_.AlgebraicCurve.germToFunctionField_mem_lSpaceOn_placesOf
{K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
[IsIntegral C]
(U : C.Opens) [Nonempty (U : C.Opens)] (s : Γ(C, U)) :
letI := (AlgebraicCurve.baseToFunctionField c).toAlgebra
(C.germToFunctionField U).hom s ∈
AlgebraicCurve.lSpaceOn (AlgebraicCurve.placesOf c U) (0 : AlgebraicCurve.Divisor K
C.functionField) := by
let := (AlgebraicCurve.baseToFunctionField c).toAlgebra
rintro v ⟨x, hxU, -, hvx⟩
simp only [Finsupp.coe_zero, Pi.zero_apply, WithZero.exp_zero]
rw [← Place.mem_iff_adicValuation_le_one]
change (C.germToFunctionField U).hom s ∈ v.toValuationSubring.toSubring
rw [← hvx]
let := C.presheaf.algebra_section_stalk (⟨x, hxU⟩ : U)
have := AlgebraicGeometry.functionField_isScalarTower (X := C) U ⟨x, hxU⟩
exact RingHom.mem_range.mpr ⟨algebraMap Γ(C, U) (C.presheaf.stalk x) s,
(IsScalarTower.algebraMap_apply Γ(C, U) (C.presheaf.stalk x) C.functionField s).symm⟩