Module

GermToFunctionField_inf_mem_lSpaceOn_inter_placesOf.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.GermToFunctionField_inf_mem_lSpaceOn_inter_placesOf

2 declarations indexed from sourceView source ↗

Module documentation

Germ To Function Field inf mem l Space On inter places Of

Imports4

Imported by4

theorem

germToFunctionField_mem_lSpaceOn_placesOf_aux

L38 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GermToFunctionFieldInfMemLSpace.germToFunctionField_mem_lSpaceOn_placesOf_aux

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GermToFunctionFieldInfMemLSpace
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 u

Lean source · full declaration

theorem germToFunctionField_mem_lSpaceOn_placesOf_aux
    {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⟩

theorem

germToFunctionField_inf_mem_lSpaceOn_inter_placesOf

L57 ↗

AlgebraicCurve.germToFunctionField_inf_mem_lSpaceOn_inter_placesOf