AlgebraicGeometry.RelPicard.RigidifiedLineBundle.exists_isClosedImmersion_lfp_chart_iff_of_descent
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry.RelPicard.RigidifiedLineBundle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.PolarisationLean source · statement
theorem exists_isClosedImmersion_lfp_chart_iff_of_descent
{R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
(L : RelativeGroupLaw R f)
{X : Scheme.{0}} (g : X ⟶ Spec (CommRingCat.of R))
(M : RigidifiedLineBundle f (L.one (𝟙 (Spec (CommRingCat.of R)))) g) (U : X.affineOpens)
(R₀ : Type) [CommRing R₀] [IsNoetherianRing R₀] (φ : R₀ →+* R)
(A₀ : Scheme.{0}) (f₀ : A₀ ⟶ Spec (CommRingCat.of R₀)) (L₀ : RelativeGroupLaw R₀ f₀)
(X₀ : Scheme.{0}) (g₀ : X₀ ⟶ Spec (CommRingCat.of R₀)) [LocallyOfFiniteType g₀]
(M₀ : RigidifiedLineBundle f₀ (L₀.one (𝟙 (Spec (CommRingCat.of R₀)))) g₀)
(a : A ⟶ A₀) (ha : IsPullback a f f₀ (Spec.map (CommRingCat.ofHom φ)))
(u : ((U : X.Opens) : Scheme.{0}) ⟶ X₀)
(hu : IsPullback u ((U : X.Opens).ι ≫ g) g₀ (Spec.map (CommRingCat.ofHom φ)))
(hM : Nonempty ((M.pullbackAlong
(⟨(U : X.Opens).ι, rfl⟩ : SchemeHomOver ((U : X.Opens).ι ≫ g) g)).L ≅
(Scheme.Modules.pullback
(pullback.map f ((U : X.Opens).ι ≫ g) f₀ g₀ a u
(Spec.map (CommRingCat.ofHom φ)) ha.w.symm hu.w.symm)).obj M₀.L))
(Z₀ : Scheme.{0}) (ι₀ : Z₀ ⟶ X₀) (hι₀ : IsClosedImmersion ι₀)
(hZ₀ : ∀ {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) :
∃ (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)