AlgebraicGeometry.RelPicard.RigidifiedLineBundle.nonempty_iso_unit_of_locIsoOnBase_unit_faces_of_isNoetherianRing
Infinitesimal lifting makes the closed triviality locus open, then connected fibres make it all.
Source context 11 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_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.Polarisation
open _root_.AlgebraicGeometry.RelPicard
open IsLocalRing
namespace AlgebraicGeometry.RelPicard.RigidifiedLineBundleLean source · full declaration
theorem nonempty_iso_unit_of_locIsoOnBase_unit_faces_of_isNoetherianRing
{S : Type} [CommRing S] [IsNoetherianRing S] {A : Scheme} {f : A ⟶ Spec (CommRingCat.of S)}
(L : RelativeGroupLaw S f) (hA : AbelianSchemePropertyBundle S f)
(M : RigidifiedLineBundle (prodStr f f) ((L.prod L).one (𝟙 (Spec (CommRingCat.of S)))) f)
(h₁ : LocIsoOnBase (prodStr f f)
((Scheme.Modules.pullback
(pullback.lift
(pullback.lift (L.one (prodStr f f)).1 (pullback.fst f f) (by rw [(L.one _).2]))
(pullback.snd f f)
(by
rw [pullback.lift_fst_assoc, (L.one _).2]
exact pullback.condition))).obj M.L) (𝟙_ _))
(h₂ : LocIsoOnBase (prodStr f f)
((Scheme.Modules.pullback
(pullback.lift
(pullback.lift (pullback.fst f f) (L.one (prodStr f f)).1 (by rw [(L.one _).2]))
(pullback.snd f f)
(by rw [pullback.lift_fst_assoc]; exact pullback.condition))).obj M.L) (𝟙_ _))
(h₃ : LocIsoOnBase (prodStr f f)
((Scheme.Modules.pullback
(pullback.lift (𝟙 _) (L.one (prodStr f f)).1
(by rw [Category.id_comp, (L.one _).2]))).obj M.L) (𝟙_ _)) :
Nonempty (M.L ≅ (RigidifiedLineBundle.unit (c := prodStr f f) (ε := (L.prod L).one (𝟙 (Spec
(CommRingCat.of S)))) f).L) := by
classical
have : Smooth f := hA.smooth
obtain ⟨Z, ι, hcl, hlfp, hZ⟩ :=
exists_isClosedImmersion_locallyOfFinitePresentation_forall_iff_of_locallyOfFinitePresentation
(L.prod L) (GoodReductionJacobian.AbelianSchemePropertyBundle.prodStr_commRing hA hA) f M
have := hcl
have := hlfp
have : IsLocallyNoetherian A := LocallyOfFiniteType.isLocallyNoetherian f
have hopen : IsOpenImmersion ι := by
refine isOpenImmersion_of_mono_of_forall_exists_lift_of_isArtinianRing_of_isLocallyNoetherian ι
(fun T' T _ _ _ _ _ p hp hsmall s m hm => ?_)
have hT : Nonempty ((M.pullbackAlong
(⟨Spec.map (CommRingCat.ofHom p) ≫ s, rfl⟩ : SchemeHomOver ((Spec.map (CommRingCat.ofHom p)
≫ s) ≫ f) f)).L ≅
(RigidifiedLineBundle.unit (c := prodStr f f) (ε := (L.prod L).one (𝟙 (Spec
(CommRingCat.of S)))) _).L) :=
(hZ _ _).mpr ⟨m, hm⟩
obtain ⟨m', hm'⟩ := (hZ _ _).mp
(nonempty_pullbackAlong_iso_unit_of_smallExtension_of_locIsoOnBase_faces L hA M h₁ h₂ T' T p
hp hsmall s hT)
refine ⟨m', hm', ?_⟩
rw [← cancel_mono ι, Category.assoc, hm', hm]
have := hopen
have hiso : IsIso ι :=
isIso_of_isOpenImmersion_of_isClosedImmersion_of_section_of_isConnected_fibres f
hA.connectedFibres (L.one (𝟙 _)).1 (L.one (𝟙 _)).2 ι ((hZ _ (L.one (𝟙 _))).mp
(nonempty_pullbackAlong_one_iso_unit_of_locIsoOnBase_face L hA M h₃))
obtain ⟨eI⟩ := (hZ f ⟨𝟙 A, Category.id_comp f⟩).mpr ⟨inv ι, IsIso.inv_hom_id ι⟩
exact ⟨((Scheme.Modules.pullbackCongr (baseChangeSnd_id (prodStr f f) f)).app M.L ≪≫
(Scheme.Modules.pullbackId _).app M.L).symm ≪≫ eI⟩