AlgebraicGeometry.RelPicard.RigidifiedLineBundle.exists_noetherian_descent_affineOpens
Descend a rigidified line bundle on an affine open to a Noetherian base, preserving the group law and the pullback comparison.
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 · full declaration
theorem exists_noetherian_descent_affineOpens
{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) :
∃ (R₀ : Type) (_ : CommRing R₀) (_ : IsNoetherianRing R₀) (φ : R₀ →+* R)
(A₀ : Scheme.{0}) (f₀ : A₀ ⟶ Spec (CommRingCat.of R₀)) (L₀ : RelativeGroupLaw R₀ f₀) (_ :
AbelianSchemePropertyBundle 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 φ))),
(∀ (T : Scheme.{0}) (t : T ⟶ Spec (CommRingCat.of R)) (P Q : SchemeHomOver t f),
(L.mul t P Q).1 ≫ a = (L₀.mul (t ≫ Spec.map (CommRingCat.ofHom φ))
⟨P.1 ≫ a, by rw [Category.assoc, ha.w, ← Category.assoc, P.2]⟩
⟨Q.1 ≫ a, by rw [Category.assoc, ha.w, ← Category.assoc, Q.2]⟩).1) ∧
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) := by
classical
obtain ⟨T, hTfg, -, A₁, f₁, L₁, π, hπ, hA₁, -, -, hLπ⟩ :=
L.exists_fg_subalgebra_abelianSchemePropertyBundle_isPullback_of_isNoetherianRing
(A₀ := ℤ) hA ∅
obtain ⟨sT, hsT⟩ := hTfg
have : IsAffine ((U : X.Opens) : Scheme.{0}) := U.2
obtain ⟨T₂, hT2fg, hsT₂, X₁, g₁, u, hlfp, hqc, hqs, hu⟩ :=
AlgebraicGeometry.exists_fg_subalgebra_isPullback_of_locallyOfFinitePresentation (A₀ := ℤ) ((U
: X.Opens).ι ≫ g) sT
have hT12 : T ≤ T₂ := by rw [← hsT]; exact Algebra.adjoin_le hsT₂
have := hlfp
have := hqc
have := hqs
have hψ : (algebraMap ↥T₂ R).comp (Subalgebra.inclusion hT12).toRingHom = algebraMap ↥T R :=
RingHom.ext fun _ => rfl
obtain ⟨A₂, f₂, L₂, hA₂, a₂, ha₂, b, hb, hab, hLa₂, -⟩ :=
L.exists_isPullback_comp_eq_mul_eq_of_isPullback_of_comp_eq
(algebraMap ↥T R) (algebraMap ↥T₂ R) (Subalgebra.inclusion hT12).toRingHom hψ A₁ f₁ L₁ hA₁ π
hπ
(fun T' t P Q => hLπ t P Q)
exact exists_noetherian_descent_affineOpens_of_isPullback_of_isPullback
L g M U T₂ hT2fg A₂ f₂ L₂ hA₂ a₂ ha₂ hLa₂ X₁ g₁ u hu