AlgebraicGeometry.RelPicard.exists_twoAffineOpenCover_fibre_finrank_H0_eq_and_subsingleton_H1_iff
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace Exists_twoAffineOpenCover_fibre_finrank_H0_eq_and_subsingleton_H1_iff
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
NeronModelInfra
open Exists_twoAffineOpenCover_fibre_finrank_H0_eq_and_subsingleton_H1_iff in
with_weak_namespace _root_.AlgebraicGeometry.RelPicardLean source · statement
theorem exists_twoAffineOpenCover_fibre_finrank_H0_eq_and_subsingleton_H1_iff
{R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
{T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (F : (pullback c t).Modules)
(hF : Scheme.Modules.IsInvertible F)
{k : Type u} [Field k] (s : Spec (CommRingCat.of k) ⟶ T)
(𝒲 : (pullback (pullback.snd c t) s).TwoAffineOpenCover) (K : Type u) [Field K] [Algebra k K] :
∃ 𝒲' : (pullback (pullback.snd c t) (Scheme.TwoAffineOpenCover.specMap k K ≫
s)).TwoAffineOpenCover,
Module.finrank K (𝒲'.sectionsOf (fibreAt c t (Scheme.TwoAffineOpenCover.specMap k K ≫ s))
(fibreModule c t (Scheme.TwoAffineOpenCover.specMap k K ≫ s) F)).H0 =
Module.finrank k (𝒲.sectionsOf (fibreAt c t s) (fibreModule c t s F)).H0 ∧
(Subsingleton (𝒲'.sectionsOf (fibreAt c t (Scheme.TwoAffineOpenCover.specMap k K ≫ s))
(fibreModule c t (Scheme.TwoAffineOpenCover.specMap k K ≫ s) F)).H1 ↔
Subsingleton (𝒲.sectionsOf (fibreAt c t s) (fibreModule c t s F)).H1)