theorem
L320 ↗exists_isClosedImmersion_locallyOfFinitePresentation_forall_iff_of_locallyOfFinitePresentation
AlgebraicGeometry.RelPicard.RigidifiedLineBundle.exists_isClosedImmersion_locallyOfFinitePresentation_forall_iff_of_locallyOfFinitePresentation
Glue the closed loci on affine charts using the existing affine-chart criterion.
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_locallyOfFinitePresentation_forall_iff_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) :
∃ (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