AlgebraicCurves.Models.Proofs.IsCurveOver_of_ringEquiv_functionField_of_isIntegral_of_smoothOfRelativeDimension_one.SmoothModelFunctionFieldGen.stageA3
Source context 21 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace IsCurveOver_of_ringEquiv_functionField_of_isIntegral_of_smoothOfRelativeDimension_one
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.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
open scoped TensorProduct
open CategoryTheory AlgebraicGeometry AlgebraicCurve Opposite
universe u v
namespace SmoothModelFunctionFieldGenLean source · full declaration
theorem stageA3 {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
[IsIntegral C]
[SmoothOfRelativeDimension 1 c] :
letI := (baseToFunctionField c).toAlgebra
Algebra.EssFiniteType K C.functionField ∧
Module.rank C.functionField Ω[C.functionField⁄K] = 1 ∧
Algebra.Transcendental K C.functionField := by
let algKF : Algebra K C.functionField := (baseToFunctionField c).toAlgebra
obtain ⟨x⟩ := (inferInstance : Nonempty C)
obtain ⟨U, hU, V, hV, hxV, e, hstd⟩ :=
SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension (n := 1) (f := c) x
have : Nonempty V := ⟨⟨x, hxV⟩⟩
obtain rfl : U = ⊤ := by
ext y
simp only [TopologicalSpace.Opens.coe_top, Set.mem_univ, iff_true]
have : y = c.base x := Subsingleton.elim _ _
rw [this]; exact e hxV
let eK : Γ(Spec (CommRingCat.of K), ⊤) ≃+* K := (Scheme.ΓSpecIso
(.of K)).commRingCatIsoToRingEquiv
let algRA : Algebra Γ(Spec (CommRingCat.of K), ⊤) Γ(C, V) := (c.appLE ⊤ V e).hom.toAlgebra
have hstdA : Algebra.IsStandardSmoothOfRelativeDimension 1 Γ(Spec (CommRingCat.of K), ⊤) Γ(C,
V) :=
hstd
let algKR : Algebra K Γ(Spec (CommRingCat.of K), ⊤) := eK.symm.toRingHom.toAlgebra
have : Algebra.IsStandardSmoothOfRelativeDimension 0 K Γ(Spec (CommRingCat.of K), ⊤) :=
.of_algebraMap_bijective eK.symm.bijective
let algKA : Algebra K Γ(C, V) :=
((algebraMap Γ(Spec (CommRingCat.of K), ⊤) Γ(C, V)).comp
(algebraMap K Γ(Spec (CommRingCat.of K), ⊤))).toAlgebra
have : IsScalarTower K Γ(Spec (CommRingCat.of K), ⊤) Γ(C, V) :=
IsScalarTower.of_algebraMap_eq fun _ => rfl
have hKA : Algebra.IsStandardSmoothOfRelativeDimension (1 + 0) K Γ(C, V) :=
Algebra.IsStandardSmoothOfRelativeDimension.trans 0 1 K Γ(Spec (CommRingCat.of K), ⊤) Γ(C, V)
have : IsFractionRing Γ(C, V) C.functionField :=
functionField_isFractionRing_of_isAffineOpen C V hV
have : IsScalarTower K Γ(C, V) C.functionField := by
refine IsScalarTower.of_algebraMap_eq fun k => ?_
change baseToFunctionField c k =
(C.germToFunctionField V).hom ((c.appLE ⊤ V e).hom (eK.symm k))
simp only [baseToFunctionField, RingHom.coe_comp, Function.comp_apply, Scheme.Hom.appLE,
Scheme.germToFunctionField, CommRingCat.hom_comp]
rw [TopCat.Presheaf.germ_res_apply]
rfl
have := Algebra.IsStandardSmoothOfRelativeDimension.isStandardSmooth (n := 1 + 0) (R := K)
(S := Γ(C, V))
have : Algebra.EssFiniteType Γ(C, V) C.functionField :=
Algebra.EssFiniteType.of_isLocalization C.functionField (nonZeroDivisors Γ(C, V))
have hT : Algebra.Transcendental K C.functionField := by
obtain ⟨g, hg⟩ := Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial
(1 + 0) K Γ(C, V)
let algPA : Algebra (MvPolynomial (Fin (1 + 0)) K) Γ(C, V) := g.toRingHom.toAlgebra
have : Algebra.Etale (MvPolynomial (Fin (1 + 0)) K) Γ(C, V) := hg.toAlgebra
have : IsScalarTower K (MvPolynomial (Fin (1 + 0)) K) Γ(C, V) :=
IsScalarTower.of_algebraMap_eq fun k => (g.commutes k).symm
have hinj : Function.Injective (algebraMap (MvPolynomial (Fin (1 + 0)) K) Γ(C, V)) := by
rw [injective_iff_map_eq_zero]
intro p hp
by_contra hp0
have hreg : IsSMulRegular Γ(C, V) p :=
Module.Flat.isSMulRegular_of_nonZeroDivisors (mem_nonZeroDivisors_of_ne_zero hp0)
have h1 : p • (1 : Γ(C, V)) = p • (0 : Γ(C, V)) := by
rw [Algebra.smul_def, mul_one, hp, smul_zero]
exact one_ne_zero (hreg h1)
have hX : Transcendental K
(algebraMap (MvPolynomial (Fin (1 + 0)) K) Γ(C, V) (MvPolynomial.X 0)) :=
(transcendental_algebraMap_iff hinj).mpr (MvPolynomial.transcendental_X K 0)
exact ⟨⟨algebraMap Γ(C, V) C.functionField _,
(transcendental_algebraMap_iff (IsFractionRing.injective Γ(C, V) C.functionField)).mpr hX⟩⟩
refine ⟨Algebra.EssFiniteType.comp K Γ(C, V) C.functionField, ?_, hT⟩
have : Algebra.FormallyEtale Γ(C, V) C.functionField :=
Algebra.FormallyEtale.of_isLocalization (nonZeroDivisors Γ(C, V))
have h := (KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale K Γ(C, V)
C.functionField).lift_rank_eq
rw [Module.rank_baseChange,
Algebra.IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential (1 + 0)] at h
simpa using h.symm