AlgebraicGeometry.RelPicard.RigidifiedLineBundle.exists_isClosedImmersion_lfp_chart_iff_affineOpens_of_locallyOfFinitePresentation
Descend to a noetherian base and transport its closed triviality locus to each affine chart.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
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.Polarisation
namespace AlgebraicGeometry.RelPicard.RigidifiedLineBundleLean source · statement
theorem exists_isClosedImmersion_lfp_chart_iff_affineOpens_of_locallyOfFinitePresentation
{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)) [LocallyOfFinitePresentation g]
(M : RigidifiedLineBundle f (L.one (𝟙 (Spec (CommRingCat.of R)))) g) (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)