AlgebraicGeometry.RelPicard.RigidifiedLineBundle.exists_isClosedImmersion_lfp_iff_of_forall_affineOpens_chart
Local finite-presentation criteria for the triviality locus of a rigidified line bundle.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry.RelPicard.RigidifiedLineBundle
open _root_.JacobianVarieties.Picard.Proofs.LfpChartCriterion
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.PolarisationLean source · statement
theorem exists_isClosedImmersion_lfp_iff_of_forall_affineOpens_chart
{R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
(L : RelativeGroupLaw R f) (hA : AbelianSchemePropertyBundle R f)
{X : Scheme.{0}} (g : X ⟶ Spec (CommRingCat.of R))
(M : RigidifiedLineBundle f (L.one (𝟙 (Spec (CommRingCat.of R)))) g)
(hloc : ∀ U : X.affineOpens, ∃ (ZU : Scheme.{0}) (ιU : ZU ⟶ ((U : X.Opens) : Scheme.{0})),
IsClosedImmersion ιU ∧ LocallyOfFinitePresentation ιU ∧
∀ {T : Scheme.{0}} (t : T ⟶ Spec (CommRingCat.of R)) (ψU : T ⟶ ((U : X.Opens) : Scheme.{0}))
(hψ : (ψU ≫ (U : X.Opens).ι) ≫ g = t),
(Nonempty ((M.pullbackAlong (⟨ψU ≫ (U : X.Opens).ι, hψ⟩ : SchemeHomOver t g)).L ≅
(RigidifiedLineBundle.unit (c := f) (ε := L.one (𝟙 (Spec (CommRingCat.of R)))) t).L) ↔
∃ ψ₀ : T ⟶ ZU, ψ₀ ≫ ιU = ψU)) :
∃ (Z : Scheme.{0}) (ι : Z ⟶ X), IsClosedImmersion ι ∧ LocallyOfFinitePresentation ι ∧
∀ {T : Scheme.{0}} (t : T ⟶ Spec (CommRingCat.of R)) (ψ : SchemeHomOver t g),
Nonempty ((M.pullbackAlong ψ).L ≅
(RigidifiedLineBundle.unit (c := f) (ε := L.one (𝟙 (Spec (CommRingCat.of R)))) t).L) ↔
∃ ψ₀ : T ⟶ Z, ψ₀ ≫ ι = ψ.1