AlgebraicGeometry.RelPicard.nonempty_pullback_fst_thetaBundle_iso_baseChange
Source context 18 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ThetaFirstProjection
attribute [-instance]
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instNeg
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSMulInt
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instAddCommGroup
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instAdd
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSub
attribute [-instance]
instModuleCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop
attribute [-instance]
instSMulCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop
attribute [-instance]
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSMulNat
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instZero
AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
AlgebraicGeometry.Scheme.Modules.pullback_monoidal
AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
PresheafOfModules.PullbackMonoidal.pullback_monoidal PresheafOfModules.PullbackMonoidal.isIso_δ
PresheafOfModules.pushforward_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_η
PresheafOfModules.free_monoidal PresheafOfModules.restrictScalars_laxMonoidal
PresheafOfModules.PullbackMonoidal.isIso_δ_gS PresheafOfModules.pullback_oplaxMonoidal
attribute [-instance]
instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
attribute [-instance]
PresheafOfModules.pullback_monoidal'
AlgebraicGeometry.RelEffCartierDiv.isIso_subschemeIota_snd_of_degree_one
AlgebraicGeometry.isIso_ker_graphOver_subschemeIota_snd
AlgebraicGeometry.isClosedImmersion_graphOver
attribute [-simp]
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.sub_app
AlgebraicGeometry.Scheme.IdealSheafData.sres_sresTop
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.add_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.mk.sizeOf_spec
AlgebraicGeometry.Scheme.IdealSheafData.coe_resLE
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.smul_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.coe_ofLE_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.ideal_range
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.zero_app
AlgebraicGeometry.Scheme.IdealSheafData.sres_sres
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.comp_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.neg_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.id_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.coe_mulRight_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.nsmul_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.mk.injEq
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.zsmul_app PresheafOfModules.freeεIso_hom_app
PresheafOfModules.freeμIso_hom_app AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply TwoChartCech.Mumford.ι1_apply
TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply TwoChartCech.KerCoprod.ι0_apply
PresheafOfModules.pushforwardCongr_inv_app_app_apply
PresheafOfModules.pushforwardNatTrans_app_app_apply
PresheafOfModules.pushforwardCongr_hom_app_app_apply AlgebraicGeometry.graphOver_fst_assoc
AlgebraicGeometry.RelEffCartierDiv.toPoint_comp
AlgebraicGeometry.RelEffCartierDiv.toPoint_comp_assoc AlgebraicGeometry.graphOver_fst
AlgebraicGeometry.RelEffCartierDiv.ofPoint_I AlgebraicGeometry.graphOver_snd
AlgebraicGeometry.graphOver_snd_assoc
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry.RelPicard.BaseChangeLean source · statement
theorem _root_.AlgebraicGeometry.RelPicard.nonempty_pullback_fst_thetaBundle_iso_baseChange
(R : Type u) [CommRing R] [IsNoetherianRing R] {C : Scheme.{u}}
(c : C ⟶ Spec (CommRingCat.of R))
[IsProper c] [SmoothOfRelativeDimension 1 c]
(ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
(h𝔉 : ∀ m₀ : ℕ, ∃ 𝔉 : SmoothProperCurve.FiniteMapData c ε, m₀ ≤ 𝔉.m)
{T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) [LocallyOfFiniteType t]
(M : RigidifiedLineBundle c ε t) (r n : ℕ)
(hfib : ∀ (k : Type u) [Field k] (s : Spec (CommRingCat.of k) ⟶ T)
(𝒲 : (pullback (pullback.snd c t) s).TwoAffineOpenCover),
Subsingleton
(𝒲.sectionsOf (fibreAt c t s) (fibreModule c t s (M.L ⊗ sectionTwist c ε t r))).H1 ∧
Module.finrank k
(𝒲.sectionsOf (fibreAt c t s) (fibreModule c t s (M.L ⊗ sectionTwist c ε t r))).H0 = n)
(R' : Type u) [CommRing R'] [Algebra R R']
(M' : RigidifiedLineBundle (SmoothProperCurve.baseChange R c R')
(SmoothProperCurve.sectionBaseChange R' ε)
(pullback.snd t (Spec.map (CommRingCat.ofHom (algebraMap R R')))))
(e : M'.L ≅ (BaseChange.ofR c ε R'
(M.pullbackAlong ⟨pullback.fst t (Spec.map (CommRingCat.ofHom (algebraMap R R'))),
pullback.condition⟩)).L) :
Nonempty ((Scheme.Modules.pullback
(pullback.fst t (Spec.map (CommRingCat.ofHom (algebraMap R R'))))).obj
(thetaBundle c ε t M r n) ≅
thetaBundle (SmoothProperCurve.baseChange R c R') (SmoothProperCurve.sectionBaseChange R' ε)
(pullback.snd t (Spec.map (CommRingCat.ofHom (algebraMap R R')))) M' r n)