AlgebraicGeometry.RelPicard.exists_finite_etale_hasChartSections_of_finiteMapData
Split sufficiently large etale level sets and use Riemann--Roch to construct chart sections after a finite faithfully flat etale extension of a local noetherian base.
Source context 21 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FiniteEtaleChartSections
attribute [-instance]
AlgebraicCurve.instHasLocalResidue_of_hasCanonicalLocalResidueK
AlgebraicCurve.instHasCanonicalLocalResidueK_of_hasCanonicalLocalResidueKStar
AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
AlgebraicCurve.Place.instIsLocalHomRestrictInclusion
AlgebraicCurve.Place.kw_ffgc_finiteDimensional_adicCompletion
AlgebraicCurve.Place.kw_ffgc_isScalarTower_integersIntegersCompletion
ModularCurve.KwF4gRRTate.instAlgebraKAdicCompletionIntegers
AlgebraicCurve.Place.kw_ffgc_continuousSMul_adicCompletionComap
AlgebraicCurve.Place.kw_ffgc_isScalarTower_integersCompletionCompletion
attribute [-instance]
instLiesOverSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegersCompletionIdealAsIdeal
attribute [-instance]
AlgebraicCurve.instHasCanonicalLocalResidueK AlgebraicCurve.Place.instAlgebra_restrictResidueField
AlgebraicCurve.Place.instIsScalarTower_restrictResidueField AlgebraicCurve.instHasLocalResidue
AlgebraicCurve.HasSeparableResidue.of_perfectField_of_isCurveOver
AlgebraicCurve.HasSeparableResidue.of_perfectField
AlgebraicCurve.Place.instIsLocalHom_restrictSubringHom
AlgebraicCurve.instHasCanonicalLocalResidueKStar ModularCurve.KwNo6Pin.isLocalRing_completion
AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
AlgebraicCurve.Place.instIsPrimeCenter AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
AlgebraicCurve.SemilinearAut.instDistribMulActionSubtypeProdRingAutMemSubgroupPic0
AlgebraicCurve.SemilinearAut.instDistribMulActionSubtypeProdRingAutMemSubgroupDivisor
AlgebraicCurve.Pic0.instModuleZModTorsion
AlgebraicCurve.SemilinearAut.instSMulSubtypeProdRingAutMemSubgroupPlace
AlgebraicCurve.SemilinearAut.instDistribMulActionTorsion
attribute [-instance]
AlgebraicCurve.SemilinearAut.instSMulSubtypeProdRingAutMemSubgroupPic0
AlgebraicCurve.SemilinearAut.instSMulTorsion
AlgebraicCurve.SemilinearAut.instMulActionSubtypeProdRingAutMemSubgroupPlace
AlgebraicCurve.SemilinearAut.instSMulCommClassZModTorsion
AlgebraicCurve.SemilinearAut.instMulSemiringActionSubtypeProdRingAutMemSubgroup
attribute [-simp]
AlgebraicCurve.Place.differentialCoeff_zero AlgebraicCurve.Place.differentialCoeff_dCoord
AlgebraicCurve.Place.CanonicalLocalResidueDataK.mk.sizeOf_spec
AlgebraicCurve.Place.CanonicalLocalResidueDataK.mk.injEq AlgebraicCurve.adeleSingle_coe
AlgebraicCurve.kaehlerResidueTermKFam_apply AlgebraicCurve.Place.LocalResidueData.mk.injEq
AlgebraicCurve.Place.LocalResidueData.mk.sizeOf_spec 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.kw_ffgc_adicCompletionComapIntegers_coe
AlgebraicCurve.Place.CanonicalLocalResidueDataS.mk.sizeOf_spec
AlgebraicCurve.Place.mem_simplePoleSubmodule AlgebraicCurve.Place.coe_uniformizerSubring
ModularCurve.Lg37.Lg37CompletionSection.mk.injEq
AlgebraicCurve.Place.CoefficientFieldSection.mk.injEq
AlgebraicCurve.Place.CanonicalLocalResidueDataS.mk.injEq
ModularCurve.Lg37.Lg37CompletionSection.mk.sizeOf_spec
AlgebraicCurve.Place.CoefficientFieldSection.mk.sizeOf_spec AlgebraicCurve.Place.poleSubmodule_one
AlgebraicCurve.Place.mem_poleSubmodule 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
AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp]
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
AlgebraicCurve.Divisor.degree_pushforwardAlong AlgebraicCurve.Pic0.coe_degZeroCorrespondence
AlgebraicCurve.Place.mem_fiberAlong AlgebraicCurve.SemilinearAut.toRingAut_inv
AlgebraicCurve.SemilinearAut.smul_def AlgebraicCurve.SemilinearAut.smul_single
AlgebraicCurve.SemilinearAut.smul_toValuationSubring AlgebraicCurve.SemilinearAut.baseAut_inv
AlgebraicCurve.SemilinearAut.baseAut_ofAlgAut AlgebraicCurve.SemilinearAut.toRingAut_ofAlgAut
AlgebraicCurve.SemilinearAut.toRingAut_one AlgebraicCurve.SemilinearAut.deg_smul
AlgebraicCurve.SemilinearAut.degree_smul AlgebraicCurve.SemilinearAut.coe_degZeroSMulHom
AlgebraicCurve.SemilinearAut.baseAut_mul
AlgebraicCurve.SemilinearAut.coe_smulValuationSubringEquiv_apply
AlgebraicCurve.SemilinearAut.baseAut_one AlgebraicCurve.SemilinearAut.ofAlgAut_smul
attribute [-simp]
AlgebraicCurve.SemilinearAut.coe_torsion_smul AlgebraicCurve.SemilinearAut.toRingAut_mul
AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec AlgebraicCurve.IntegralBasisInLSpace.mk.injEq
AlgebraicCurve.TranscendenceTower.mk.injEq AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
AlgebraicCurve.coe_cechH0Equiv_apply AlgebraicCurve.cechH1ToH1_mk
attribute [-simp] AlgebraicCurve.lSpaceOn_univ AlgebraicCurve.lSpaceOn_empty
universe u
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.AlgebraicCurve hiding genusLean source · statement
theorem _root_.AlgebraicGeometry.RelPicard.exists_finite_etale_hasChartSections_of_finiteMapData
(R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
{C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) [IsProper c]
[SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
(ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
(h𝔉 : ∀ m₀ : ℕ, ∃ 𝔉 : SmoothProperCurve.FiniteMapData c ε, m₀ ≤ 𝔉.m ∧
𝔉.LevelSetsGenericallyEtale) :
∃ (R' : Type u) (_ : CommRing R') (_ : Algebra R R') (_ : Module.Finite R R')
(_ : Algebra.Etale R R') (_ : Module.FaithfullyFlat R R') (_ : IsNoetherianRing R')
(n g r : ℕ) (_ : 2 * g < r)
(γ : Fin n → Fin (r - g) → SchemeHomOver (𝟙 (Spec (CommRingCat.of R'))) (baseChange R c R')),
HasChartSections (baseChange R c R') γ