AlgebraicCurve.exists_kaehlerToFunctionField_eq_of_forall_mem_placesOf_exists_eq_smul_dCoord
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open scoped TensorProduct
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs.KaehlerSectionsRegularDifferentials in
Lean source · full declarationtheorem exists_kaehlerToFunctionField_eq_of_forall_mem_placesOf_exists_eq_smul_dCoord
{k : Type u} [Field k] {X : Scheme.{u}} (c : X ⟶ Spec (CommRingCat.of k))
[IsIntegral X] [SmoothOfRelativeDimension 1 c]
(U : X.Opens) (hU : IsAffineOpen U) [Nonempty U]
(η : letI := (baseToFunctionField c).toAlgebra; Ω[X.functionField⁄k])
(hη : letI := (baseToFunctionField c).toAlgebra
∀ v : Place k X.functionField, v ∈ placesOf c U → ∃ f ∈ v.toValuationSubring, η = f •
v.dCoord) :
letI := Scheme.TwoAffineOpenCover.algebraOfHom c U
letI := (baseToFunctionField c).toAlgebra
∃ ω : Ω[Γ(X, U)⁄k], kaehlerToFunctionField c U ω = η := by
let := Scheme.TwoAffineOpenCover.algebraOfHom c U
let : Algebra k X.functionField := (baseToFunctionField c).toAlgebra
set φ : Γ(X, U) →+* X.functionField := (X.germToFunctionField U).hom with hφ
let I : Ideal Γ(X, U) :=
{ carrier := {a | ∃ ω : Ω[Γ(X, U)⁄k], kaehlerToFunctionField c U ω = φ a • η}
add_mem' := by
rintro a b ⟨ω, hω⟩ ⟨ω', hω'⟩
exact ⟨ω + ω', by rw [map_add, hω, hω', map_add, add_smul]⟩
zero_mem' := ⟨0, by rw [map_zero, map_zero, zero_smul]⟩
smul_mem' := by
rintro r a ⟨ω, hω⟩
refine ⟨r • ω, ?_⟩
rw [kaehlerToFunctionField_smul, hω, smul_eq_mul, map_mul, mul_smul] }
suffices h1 : (1 : Γ(X, U)) ∈ I by
obtain ⟨ω, hω⟩ := h1
exact ⟨ω, by rw [hω, map_one, one_smul]⟩
by_contra h1
have hItop : I ≠ ⊤ := fun h => h1 (h ▸ Submodule.mem_top)
obtain ⟨P, hP, hIP⟩ := Ideal.exists_le_maximal I hItop
have : Smooth c := SmoothOfRelativeDimension.smooth 1 c
have : LocallyOfFiniteType c := inferInstance
have : JacobsonSpace X := LocallyOfFiniteType.jacobsonSpace c
let p : PrimeSpectrum Γ(X, U) := ⟨P, hP.isPrime⟩
let x : X := hU.fromSpec.base p
have hxU : x ∈ U := by
have : x ∈ Set.range hU.fromSpec.base := ⟨p, rfl⟩
rwa [hU.range_fromSpec] at this
have hxcl : IsClosed ({x} : Set X) := by
have hp : IsClosed ({p} : Set (PrimeSpectrum Γ(X, U))) :=
(PrimeSpectrum.isClosed_singleton_iff_isMaximal p).mpr hP
have h := hU.fromSpec.isOpenEmbedding.preimage_closedPoints
have hp' : p ∈ hU.fromSpec.base ⁻¹' closedPoints X := by rw [h]; exact hp
exact hp'
obtain ⟨v, hv⟩ := AlgebraicCurve.exists_place_range_stalk_eq c x hxcl
have hvU : v ∈ placesOf c U := ⟨x, hxU, hxcl, hv⟩
obtain ⟨f, hf, hηf⟩ := hη v hvU
obtain ⟨π, hπ, hdπ⟩ := AlgebraicCurve.SurjAux.exists_mem_and_dCoord_eq v
let := TopCat.Presheaf.algebra_section_stalk X.presheaf (⟨x, hxU⟩ : U)
have : IsLocalization.AtPrime (X.presheaf.stalk x) P := hU.isLocalization_stalk' p hxU
have : IsScalarTower Γ(X, U) (X.presheaf.stalk x) X.functionField :=
AlgebraicGeometry.functionField_isScalarTower X U ⟨x, hxU⟩
have key : ∀ g ∈ v.toValuationSubring, ∃ (a s : Γ(X, U)), s ∉ P ∧ g * φ s = φ a := by
intro g hg
have hg' : g ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range := by
rw [hv]; exact hg
obtain ⟨z, rfl⟩ := hg'
obtain ⟨⟨a, s⟩, hz⟩ := IsLocalization.surj P.primeCompl z
refine ⟨a, s, s.2, ?_⟩
have h2 := congrArg (algebraMap (X.presheaf.stalk x) X.functionField) hz
rw [map_mul, ← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply] at h2
exact h2
obtain ⟨a, s, hs, hfs⟩ := key f hf
obtain ⟨b, t, ht, hπt⟩ := key π hπ
have hmem : s * t ^ 2 ∈ I := by
refine ⟨(a * t) • KaehlerDifferential.D k Γ(X, U) b - (a * b) • KaehlerDifferential.D k Γ(X, U)
t, ?_⟩
rw [map_sub, kaehlerToFunctionField_smul_D, kaehlerToFunctionField_smul_D, hηf, hdπ, ← hφ]
simp only [map_mul, map_pow]
rw [← hfs, ← hπt]
simp only [Derivation.leibniz, smul_add, smul_smul]
module
have hstP : s * t ^ 2 ∈ P := hIP hmem
rcases hP.isPrime.mem_or_mem hstP with h | h
· exact hs h
· exact ht (hP.isPrime.mem_of_pow_mem 2 h)