AlgebraicGeometry.RelPicard.RigidifiedLineBundle.exists_isClosedImmersion_forall_nonempty_pullbackAlong_iso_unit_iff_of_isNoetherianRing
Over a Noetherian base, trivial pullbacks of a rigidified bundle are represented by a closed subscheme.
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_forall_nonempty_pullbackAlong_iso_unit_iff_of_isNoetherianRing
{R : Type} [CommRing R] [IsNoetherianRing 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)) [LocallyOfFiniteType g]
(M : RigidifiedLineBundle f (L.one (𝟙 (Spec (CommRingCat.of R)))) g) :
∃ (Z : Scheme.{0}) (ι : Z ⟶ X), IsClosedImmersion ι ∧
∀ {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