AlgebraicGeometry.RelPicard.isInvertible_thetaBundle
Source context 14 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsInvertible_thetaBundle
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
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.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
attribute [-simp]
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
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
PresheafOfModules.pushforwardCongr_inv_app_app_apply
PresheafOfModules.pushforwardNatTrans_app_app_apply
PresheafOfModules.pushforwardCongr_hom_app_app_apply
PresheafOfModules.freeεIso_hom_app
PresheafOfModules.freeμIso_hom_app
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.SmoothProperCurveLean source · statement
theorem _root_.AlgebraicGeometry.RelPicard.isInvertible_thetaBundle
(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) :
Scheme.Modules.IsInvertible (thetaBundle c ε t M r n)