AlgebraicGeometry.RelPicard.exists_representsRelSubPic_algEquivZeroCut_of_chartData
The specified charts represent the algebraically trivial rigidified Picard functor.
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry.RelPicard
open _root_.JacobianVarieties.Picard.Proofs.ChartRepresentation
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobianLean source · full declaration
theorem exists_representsRelSubPic_algEquivZeroCut_of_chartData
(R : Type u) [CommRing R] [IsNoetherianRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of
R))
[IsProper c] [Flat c] (𝒱 : C.TwoAffineOpenCover)
(hH0 : ∀ (A : Type u) [CommRing A] [Algebra R A],
let : Algebra A Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A), ⊤) :=
Scheme.TwoAffineOpenCover.algebraOfHom
(Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A)) ⊤
Function.Bijective (algebraMap A Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A),
⊤)))
(ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
(hlfp : AffineLimit.IsLFPSurj (relSubPicPresheaf c ε (algEquivZeroCut c ε)))
(U : C.Opens) [SmoothOfRelativeDimension 1 (U.ι ≫ c)]
(hεU : Set.range ε.1 ⊆ (U : Set C))
{ι : Type u} [Finite ι] (g e r : ℕ) (hr : g + e = r)
(hg : ∀ (k : Type u) [Field k] [IsAlgClosed k] (x : Spec (CommRingCat.of k) ⟶ Spec
(CommRingCat.of R))
(𝒲 : (pullback (pullback.snd c (𝟙 (Spec (CommRingCat.of R)))) x).TwoAffineOpenCover),
Module.finrank k (𝒲.sectionsOf (fibreAt c (𝟙 _) x)
(𝟙_ (pullback (pullback.snd c (𝟙 (Spec (CommRingCat.of R)))) x).Modules)).H1 = g)
(Y : Scheme.{u}) (y : Y ⟶ Spec (CommRingCat.of R)) [LocallyOfFiniteType y] [CompactSpace Y]
(Duniv : RelEffCartierDiv c g y) (hDunivU : Duniv.SupportedIn U)
(huniv : ∀ ⦃T : Scheme.{u}⦄ (g' : T ⟶ Spec (CommRingCat.of R)) (D : RelEffCartierDiv c g g'),
D.SupportedIn U →
∃! φ : {φ : T ⟶ Y // φ ≫ y = g'}, PullsBackOver Duniv φ.1 φ.2 D)
(hsect : ∀ ⦃V : Scheme.{u}⦄ (u : V ⟶ Spec (CommRingCat.of R)) [LocallyOfFiniteType u] (M :
(pullback c u).Modules),
Scheme.Modules.IsInvertible M →
(∀ (k : Type u) [Field k] (s : Spec (CommRingCat.of k) ⟶ V) (𝒲 : (pullback (pullback.snd c u)
s).TwoAffineOpenCover),
Subsingleton (𝒲.sectionsOf (fibreAt c u s) (fibreModule c u s M)).H1 ∧
Module.finrank k (𝒲.sectionsOf (fibreAt c u s) (fibreModule c u s M)).H0 = 1) →
(∀ (k : Type u) [Field k] [IsAlgClosed k] (x : Spec (CommRingCat.of k) ⟶ V)
(σ : 𝟙_ (pullback c (x ≫ u)).Modules ⟶ (Scheme.Modules.pullback (mapOnProdOver c x
rfl)).obj M), σ ≠ 0 →
∃ Dx : RelEffCartierDiv c g (x ≫ u), Dx.I = Scheme.Modules.zeroSchemeIdeal σ ∧
Dx.SupportedIn U) →
∃ (D₀ : RelEffCartierDiv c g u) (N : V.Modules), Scheme.Modules.IsInvertible N ∧
Nonempty (D₀.lineBundle ≅ M ⊗ (Scheme.Modules.pullback (pullback.snd c u)).obj N) ∧
∀ (d' : ℕ) (D' : RelEffCartierDiv c d' u) (N' : V.Modules), Scheme.Modules.IsInvertible N'
→ D'.SupportedIn U →
Nonempty (D'.lineBundle ≅ M ⊗ (Scheme.Modules.pullback (pullback.snd c u)).obj N') → D'.I
= D₀.I)
(Dγ : ι → RelEffCartierDiv c e (𝟙 (Spec (CommRingCat.of R))))
(hDγU : ∀ i, (Dγ i).SupportedIn U)
(hχ : ∀ (i : ι) (k : Type u) [Field k] [IsAlgClosed k]
(x : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
(𝒲 : (pullback (pullback.snd c (𝟙 (Spec (CommRingCat.of R)))) x).TwoAffineOpenCover),
(Module.finrank k (𝒲.sectionsOf (fibreAt c (𝟙 _) x)
(fibreModule c (𝟙 _) x (sectionTwist c ε (𝟙 _) r ⊗ (Dγ i).idealModule))).H0 : ℤ) -
Module.finrank k (𝒲.sectionsOf (fibreAt c (𝟙 _) x)
(fibreModule c (𝟙 _) x (sectionTwist c ε (𝟙 _) r ⊗ (Dγ i).idealModule))).H1 = 1)
(hZfibγ : ∀ (i : ι) ⦃T : Scheme.{u}⦄ (t : T ⟶ Spec (CommRingCat.of R)) [LocallyOfFiniteType t]
(L : RigidifiedLineBundle c ε t), FibrewiseAlgEquivZero L →
∀ (k : Type u) [Field k] [IsAlgClosed k] (x : Spec (CommRingCat.of k) ⟶ T)
(σ : 𝟙_ (pullback c (x ≫ t)).Modules ⟶ (Scheme.Modules.pullback (mapOnProdOver c x rfl)).obj
(L.L ⊗ (sectionTwist c ε t r ⊗ ((Dγ i).pullbackAlong t (Category.comp_id
t)).idealModule))), σ ≠ 0 →
∃ Dx : RelEffCartierDiv c g (x ≫ t), Dx.I = Scheme.Modules.zeroSchemeIdeal σ ∧
Dx.SupportedIn U)
(hH0one : ∀ (i : ι) ⦃T : Scheme.{u}⦄ (t : T ⟶ Spec (CommRingCat.of R)) (L :
RigidifiedLineBundle c ε t), FibrewiseAlgEquivZero L →
∀ (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
(L.L ⊗ (sectionTwist c ε t r ⊗ ((Dγ i).pullbackAlong t (Category.comp_id
t)).idealModule)))).H1 →
Module.finrank k (𝒲.sectionsOf (fibreAt c t s) (fibreModule c t s
(L.L ⊗ (sectionTwist c ε t r ⊗ ((Dγ i).pullbackAlong t (Category.comp_id
t)).idealModule)))).H0 = 1)
(hcover : ∀ ⦃T : Scheme.{u}⦄ (t : T ⟶ Spec (CommRingCat.of R)) (L : RigidifiedLineBundle c ε t),
FibrewiseAlgEquivZero L → ∀ (k : Type u) [Field k] (s : Spec (CommRingCat.of k) ⟶ T),
∃ i : ι, ∀ (𝒲 : (pullback (pullback.snd c t) s).TwoAffineOpenCover),
Subsingleton (𝒲.sectionsOf (fibreAt c t s) (fibreModule c t s
(L.L ⊗ (sectionTwist c ε t r ⊗ ((Dγ i).pullbackAlong t (Category.comp_id
t)).idealModule)))).H1)
(havoid : ∀ (i : ι) ⦃T : Scheme.{u}⦄ (t : T ⟶ Spec (CommRingCat.of R)) [LocallyOfFiniteType t]
(L : RigidifiedLineBundle c ε t), FibrewiseAlgEquivZero L →
∀ (D₀ : RelEffCartierDiv c g t) (N : T.Modules), Scheme.Modules.IsInvertible N →
Nonempty (D₀.lineBundle ≅
(L.L ⊗ (sectionTwist c ε t r ⊗ ((Dγ i).pullbackAlong t (Category.comp_id
t)).idealModule)) ⊗
(Scheme.Modules.pullback (pullback.snd c t)).obj N) →
D₀.SupportedIn U)
(hcut : ∀ (i : ι) ⦃T : Scheme.{u}⦄ (t : T ⟶ Spec (CommRingCat.of R)) [LocallyOfFiniteType t]
(D : RelEffCartierDiv c r t) (D₀ : RelEffCartierDiv c g t), D₀.SupportedIn U →
D.I = D₀.I * ((Dγ i).pullbackAlong t (Category.comp_id t)).I →
∃ W : T.Opens, ∀ (k : Type u) [Field k] [IsAlgClosed k] (s : Spec (CommRingCat.of k) ⟶ T),
Set.range ⇑s ⊆ (W : Set T) ↔
IsAlgEquivZero (fibreAt c t s)
((Scheme.Modules.pullback (pullback.fst (pullback.snd c t) s)).obj (D.twistModule c ε)))
(hfib : ∀ (k : Type u) [Field k] [IsAlgClosed k]
(x : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
(L : (pullback c x).Modules), Scheme.Modules.IsInvertible L →
IsAlgEquivZero (pullback.snd c x) L →
∀ s : 𝟙_ (pullback c x).Modules ⟶ L, s ≠ 0 → Nonempty (L ≅ 𝟙_ (pullback c x).Modules)) :
∃ D : RelativePic0Designation R c,
Nonempty (RepresentsRelSubPic c ε (algEquivZeroCut c ε) D) ∧
Smooth D.toBase ∧ IsSeparated D.toBase ∧ QuasiCompact D.toBase ∧
Surjective D.toBase ∧ GeometricallyConnected D.toBase := by
obtain ⟨X, f, hopen, hft, hqc, hsurj, -, -⟩ :=
exists_openCharts_of_relEffCartierDiv_supportedIn_of_fibrewise_zeroScheme
R c 𝒱 hH0 ε hlfp U hεU g e r hr hg Y y Duniv hDunivU huniv hsect Dγ hDγU hχ hZfibγ hH0one
hcover havoid hcut
have : ∀ i, CompactSpace (X i) := hqc
obtain ⟨D, ⟨h⟩, hsm, hsep, hq⟩ :=
exists_representsRelSubPic_algEquivZeroCut_of_openCharts_of_bijective_sections
R c 𝒱 ε hH0 hfib X f hopen hft hsurj
exact ⟨D, ⟨h⟩, hsm, hsep, hq,
AlgebraicGeometry.RelPicard.surjective_toBase_of_representsRelSubPic_algEquivZeroCut R c ε D h,
AlgebraicGeometry.RelPicard.geometricallyConnected_of_representsRelSubPic_algEquivZeroCut R c ε
D h⟩