AlgebraicGeometry.SmoothProperCurve.bijective_algebraMap_sections_baseChange_of_finiteMapData
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_bijective_algebraMap_sections_baseChange_of_finiteMapData
attribute [-instance]
AlgebraicCurve.IsCurveOver.instNontrivialKaehler
AlgebraicCurve.IsCurveOver.instFreeKaehler
AlgebraicCurve.IsCurveOver.toHasPrincipalDivisors
AlgebraicCurve.IsCurveOver.instFiniteResidue
AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp]
AlgebraicCurve.mulAdele_apply
AlgebraicCurve.residuePairing_apply_coe
AlgebraicCurve.mem_adeleBdd
AlgebraicCurve.weilSmul_one
AlgebraicCurve.diagonalHom_apply
AlgebraicCurve.weilSmul_apply
AlgebraicCurve.adeleSpaceMul_coe
AlgebraicCurve.mulAdele_one
AlgebraicCurve.coe_cechH0Equiv_apply
AlgebraicCurve.cechH1ToH1_mk
AlgebraicCurve.lSpaceOn_univ
AlgebraicCurve.lSpaceOn_empty
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.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
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
AlgebraicCurve.Place.differentialCoeff_zero
AlgebraicCurve.Place.differentialCoeff_dCoord
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
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
with_weak_namespace _root_.AlgebraicGeometry.SmoothProperCurveLean source · full declaration
theorem bijective_algebraMap_sections_baseChange_of_finiteMapData
(R : Type u) [CommRing R] [IsNoetherianRing R] [_root_.IsReduced 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)
(A : Type u) [CommRing A] [Algebra R A] :
letI := Scheme.TwoAffineOpenCover.algebraOfHom
(Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A)) ⊤
Function.Bijective (algebraMap A
Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A), ⊤)) := by
obtain ⟨𝔉, -⟩ := h𝔉 0
refine Scheme.TwoAffineOpenCover.bijective_algebraMap_sections_baseChange_of_isReduced
𝔉.twoAffineOpenCover c (SmoothProperCurve.FiniteMapData.finite_H0_H1_lineBundle 𝔉 1) ?_ A
intro K _ _
refine Scheme.TwoAffineOpenCover.finrank_ker_cechDiff_baseChange_eq_one
𝔉.twoAffineOpenCover c ?_ ?_ K
· intro L _ _ _
infer_instance
· intro L _ _ _
exact (Scheme.TwoAffineOpenCover.finrank_cechDiff_baseChange_of_isAlgClosed
𝔉.twoAffineOpenCover c L).1