NYLL
Module

LSpaceOn_setOf_exists_centre_eq_span_integralClosure.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.LSpaceOn_setOf_exists_centre_eq_span_integralClosure
6 declarations indexed from sourceView source ↗

Module documentation

LSpace On set Of exists centre eq span integral Closure

Imports6
Imported by2

Declarations

theorem

mem_iff_adicValuation_le_one

L72 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpaceOnSetOfExistsCentreSpan.HoloICAux.mem_iff_adicValuation_le_one
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpaceOnSetOfExistsCentreSpan
attribute [-instance]
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instIsLocalHomRestrictInclusion
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord 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.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
universe u
open CategoryTheory AlgebraicGeometry AlgebraicCurve
namespace HoloICAux
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.IsLocalRing
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) [IsIntegral C]
Lean source · statement
theorem mem_iff_adicValuation_le_one {K : Type u} [Field K] [Algebra k K] (v : Place k K) (f : K) :
    f ∈ v.toValuationSubring ↔ v.adicValuation f ≤ 1
theorem

germ_res_apply'

L101 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpaceOnSetOfExistsCentreSpan.HoloICAux.germ_res_apply'
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpaceOnSetOfExistsCentreSpan
attribute [-instance]
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instIsLocalHomRestrictInclusion
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord 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.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
universe u
open CategoryTheory AlgebraicGeometry AlgebraicCurve
namespace HoloICAux
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.IsLocalRing
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) [IsIntegral C]
Lean source · statement
theorem germ_res_apply' {U V : C.Opens} (h : V ≤ U) (hV : genericPoint C ∈ V) (s : Γ(C, U)) :
    (C.presheaf.germ V (genericPoint C) hV).hom ((C.presheaf.map (homOfLE h).op).hom s) =
      (C.presheaf.germ U (genericPoint C) (h hV)).hom s
theorem

algebraMap_eq_germ

L106 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpaceOnSetOfExistsCentreSpan.HoloICAux.algebraMap_eq_germ
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpaceOnSetOfExistsCentreSpan
attribute [-instance]
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instIsLocalHomRestrictInclusion
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord 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.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
universe u
open CategoryTheory AlgebraicGeometry AlgebraicCurve
namespace HoloICAux
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.IsLocalRing
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) [IsIntegral C]
Lean source · full declaration
theorem algebraMap_eq_germ (U : C.Opens) (hU : genericPoint C ∈ U) (a : k) :
    letI := (baseToFunctionField c).toAlgebra
    algebraMap k C.functionField a =
      (C.presheaf.germ U (genericPoint C) hU).hom ((c.appLE ⊤ U le_top).hom ((Scheme.ΓSpecIso
        (CommRingCat.of k)).inv.hom a)) := by
  have : c.appLE ⊤ U le_top = c.appTop ≫ C.presheaf.map (homOfLE le_top).op := rfl
  rw [this, CommRingCat.hom_comp, RingHom.comp_apply, germ_res_apply' le_top hU]
  rfl
theorem

germ_eq_algebraMap_germ

L115 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpaceOnSetOfExistsCentreSpan.HoloICAux.germ_eq_algebraMap_germ
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpaceOnSetOfExistsCentreSpan
attribute [-instance]
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instIsLocalHomRestrictInclusion
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord 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.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
universe u
open CategoryTheory AlgebraicGeometry AlgebraicCurve
namespace HoloICAux
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.IsLocalRing
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) [IsIntegral C]
Lean source · statement
theorem germ_eq_algebraMap_germ (U : C.Opens) (hU : genericPoint C ∈ U) (z : C) (hz : z ∈ U) (s :
  Γ(C, U)) :
    (C.presheaf.germ U (genericPoint C) hU).hom s =
      algebraMap (C.presheaf.stalk z) C.functionField ((C.presheaf.germ U z hz).hom s)
theorem

isIntegral_iff_isIntegral_range

L123 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpaceOnSetOfExistsCentreSpan.HoloICAux.isIntegral_iff_isIntegral_range
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpaceOnSetOfExistsCentreSpan
attribute [-instance]
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instIsLocalHomRestrictInclusion
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord 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.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
universe u
open CategoryTheory AlgebraicGeometry AlgebraicCurve
namespace HoloICAux
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.IsLocalRing
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) [IsIntegral C]
Lean source · full declaration
theorem isIntegral_iff_isIntegral_range {A K : Type u} [CommRing A] [Field K] (φ : A →+* K) (f :
  K) :
    (letI := φ.toAlgebra; IsIntegral A f) ↔ IsIntegral φ.range f := by
  let := φ.toAlgebra
  constructor
  · rintro ⟨p, hp, hpf⟩
    refine ⟨p.map φ.rangeRestrict, hp.map _, ?_⟩
    rw [Polynomial.eval₂_map]
    exact hpf
  · rintro ⟨q, hq, hqf⟩
    obtain ⟨p, hpq, -, hp⟩ := Polynomial.lifts_and_degree_eq_and_monic
      (Polynomial.mem_lifts_of_surjective φ.rangeRestrict_surjective q) hq
    refine ⟨p, hp, ?_⟩
    have : (algebraMap (↥φ.range) K).comp φ.rangeRestrict = algebraMap A K := RingHom.ext fun _ =>
      rfl
    rw [← this, ← Polynomial.eval₂_map, hpq]
    exact hqf
theorem

lSpaceOn_setOf_exists_centre_eq_span_integralClosure

L143 ↗
AlgebraicCurve.lSpaceOn_setOf_exists_centre_eq_span_integralClosure
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpaceOnSetOfExistsCentreSpan
attribute [-instance]
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instIsLocalHomRestrictInclusion
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord 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.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
universe u
open CategoryTheory AlgebraicGeometry AlgebraicCurve
Lean source · full declaration
theorem _root_.AlgebraicCurve.lSpaceOn_setOf_exists_centre_eq_span_integralClosure
    (k : Type u) [Field k] [IsAlgClosed k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
    [IsIntegral C] [IsProper c]
    (hK : letI := (AlgebraicCurve.baseToFunctionField c).toAlgebra; IsCurveOver k C.functionField)
    (U : C.Opens) [Nonempty U] (hUaff : IsAffineOpen U) :
    letI := (AlgebraicCurve.baseToFunctionField c).toAlgebra
    lSpaceOn {v : Place k C.functionField | ∃ z : C, z ∈ U ∧ (∀ s : C.presheaf.stalk z,
          v.adicValuation (algebraMap (C.presheaf.stalk z) C.functionField s) ≤ 1 ∧
          (s ∈ IsLocalRing.maximalIdeal (C.presheaf.stalk z) →
            v.adicValuation (algebraMap (C.presheaf.stalk z) C.functionField s) < 1))} (0 :
              Divisor k C.functionField) =
      Submodule.span k (integralClosure Γ(C, U) C.functionField : Set C.functionField) := by
  classical
  let := (AlgebraicCurve.baseToFunctionField c).toAlgebra
  have : IsCurveOver k C.functionField := hK
  have : PerfectField k := inferInstance
  have := AlgebraicCurve.essFiniteType_functionField c
  have hη : genericPoint C ∈ U := ((genericPoint_spec C).mem_open_set_iff U.isOpen).mpr
    (by simpa using ‹Nonempty U›)
  set A : Γ(C, U) →+* C.functionField := algebraMap Γ(C, U) C.functionField with hAdef
  have hA : ∀ s, A s = (C.presheaf.germ U (genericPoint C) hη).hom s := fun s => rfl
  have hconst : ∀ a : k, ∃ s : Γ(C, U), algebraMap k C.functionField a = A s := fun a =>
    ⟨(c.appLE ⊤ U le_top).hom ((Scheme.ΓSpecIso (CommRingCat.of k)).inv.hom a), by
      rw [hA]; exact HoloICAux.algebraMap_eq_germ c U hη a⟩
  let R : Subalgebra k C.functionField :=
    { A.range with
      algebraMap_mem' := fun a => by
        obtain ⟨s, hs⟩ := hconst a
        exact ⟨s, hs.symm⟩ }
  have hRcoe : (R : Set C.functionField) = Set.range A := rfl
  have hcent : ∀ v : Place k C.functionField,
      (∃ z : C, z ∈ U ∧ (∀ s : C.presheaf.stalk z,
          v.adicValuation (algebraMap (C.presheaf.stalk z) C.functionField s) ≤ 1 ∧
          (s ∈ IsLocalRing.maximalIdeal (C.presheaf.stalk z) →
            v.adicValuation (algebraMap (C.presheaf.stalk z) C.functionField s) < 1))) ↔
        ∀ s : Γ(C, U), A s ∈ v.toValuationSubring := by
    intro v
    constructor
    · rintro ⟨z, hzU, hdom⟩ s
      rw [HoloICAux.mem_iff_adicValuation_le_one, hA, HoloICAux.germ_eq_algebraMap_germ U hη z hzU]
      exact (hdom _).1
    · intro hAv
      let ψ : Γ(C, U) →+* v.toValuationSubring := A.codRestrict v.toValuationSubring hAv
      let 𝔭 : Ideal Γ(C, U) := Ideal.comap ψ (IsLocalRing.maximalIdeal v.toValuationSubring)
      have : 𝔭.IsPrime := Ideal.comap_isPrime _ _
      let y : PrimeSpectrum Γ(C, U) := ⟨𝔭, inferInstance⟩
      let z : C := hUaff.fromSpec y
      have hzU : z ∈ U := by
        have : z ∈ Set.range hUaff.fromSpec := ⟨y, rfl⟩
        rwa [hUaff.range_fromSpec] at this
      let := C.presheaf.algebra_section_stalk (⟨z, hzU⟩ : U)
      have : IsLocalization.AtPrime (C.presheaf.stalk z) 𝔭 := hUaff.isLocalization_stalk' y hzU
      have hφ : ∀ s : Γ(C, U), algebraMap (C.presheaf.stalk z) C.functionField (algebraMap Γ(C, U)
        (C.presheaf.stalk z) s) = A s :=
        fun s => by rw [hA, HoloICAux.germ_eq_algebraMap_germ U hη z hzU]; rfl
      have hval1 : ∀ s : Γ(C, U), s ∉ 𝔭 → v.adicValuation (A s) = 1 := by
        intro s hs
        rw [show A s = ((ψ s : v.toValuationSubring) : C.functionField) from rfl,
          v.adicValuation_coe_eq_one_iff]
        by_contra hnu
        exact hs ((IsLocalRing.mem_maximalIdeal _).mpr (mem_nonunits_iff.mpr hnu))
      have hvalp : ∀ s : Γ(C, U), s ∈ 𝔭 → v.adicValuation (A s) < 1 := by
        intro s hs
        rw [show A s = ((ψ s : v.toValuationSubring) : C.functionField) from rfl,
          v.adicValuation_coe,
          IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_mem,
            Place.heightOneSpectrum_asIdeal]
        exact hs
      have hvalle : ∀ s : Γ(C, U), v.adicValuation (A s) ≤ 1 := fun s =>
        (HoloICAux.mem_iff_adicValuation_le_one v _).mp (hAv s)
      refine ⟨z, hzU, fun t => ?_⟩
      obtain ⟨⟨a, s⟩, rfl⟩ := IsLocalization.mk'_surjective 𝔭.primeCompl t
      have hs : (s : Γ(C, U)) ∉ 𝔭 := s.2
      have heq : v.adicValuation (algebraMap (C.presheaf.stalk z) C.functionField
        (IsLocalization.mk' (C.presheaf.stalk z) a s)) =
          v.adicValuation (A a) := by
        have h1 := IsLocalization.mk'_spec (C.presheaf.stalk z) a s
        have h2 := congrArg (fun w => v.adicValuation (algebraMap (C.presheaf.stalk z)
          C.functionField w)) h1
        simp only [map_mul, hφ, hval1 s hs, mul_one] at h2
        exact h2
      refine ⟨heq ▸ hvalle a, fun ht => ?_⟩
      rw [heq]
      exact hvalp a ((IsLocalization.AtPrime.mk'_mem_maximal_iff (C.presheaf.stalk z) 𝔭 a s).mp ht)
  have hIC : ∀ f : C.functionField, f ∈ integralClosure Γ(C, U) C.functionField ↔ f ∈
    integralClosure R C.functionField := by
    intro f
    change IsIntegral Γ(C, U) f ↔ IsIntegral R f
    have h1 := HoloICAux.isIntegral_iff_isIntegral_range A f
    exact h1
  let M : Submodule k C.functionField :=
    { carrier := integralClosure Γ(C, U) C.functionField
      add_mem' := fun ha hb => Subalgebra.add_mem _ ha hb
      zero_mem' := Subalgebra.zero_mem _
      smul_mem' := fun a f hf => by
        obtain ⟨s, hs⟩ := hconst a
        change a • f ∈ integralClosure Γ(C, U) C.functionField
        rw [Algebra.smul_def, hs]
        exact Subalgebra.mul_mem _ (Subalgebra.algebraMap_mem _ s) hf }
  have hspan : Submodule.span k (integralClosure Γ(C, U) C.functionField : Set C.functionField) =
    M := Submodule.span_eq M
  rw [hspan]
  ext f
  rw [AlgebraicCurve.mem_lSpaceOn_iff]
  change (∀ v ∈ {v : Place k C.functionField | _}, _) ↔ f ∈ integralClosure Γ(C, U) C.functionField
  rw [hIC, AlgebraicCurve.mem_integralClosure_iff_forall_place R f]
  simp only [Set.mem_ofPred_eq, Finsupp.zero_apply, WithZero.exp_zero]
  constructor
  · intro h v hRv
    rw [HoloICAux.mem_iff_adicValuation_le_one]
    refine h v ((hcent v).mpr fun s => hRv ⟨s, rfl⟩)
  · intro h v hv
    rw [← HoloICAux.mem_iff_adicValuation_le_one]
    refine h v ?_
    rintro _ ⟨s, rfl⟩
    exact (hcent v).mp hv s

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.