AlgebraicGeometry.RelPicard.RigidifiedLineBundle.nonempty_iso_unit_of_locIsoOnBase_unit_faces
Descend to a noetherian model and pull the resulting trivialization back to the original bundle.
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_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.Polarisation
open _root_.AlgebraicGeometry.RelPicard
namespace AlgebraicGeometry.RelPicard.RigidifiedLineBundleLean source · full declaration
theorem nonempty_iso_unit_of_locIsoOnBase_unit_faces
{S : Type} [CommRing 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
obtain ⟨S₀, _, _, A₀, f₀, L₀, hA₀, M₀, k₁, k₂, k₃, back⟩ :=
exists_isNoetherianRing_model_of_locIsoOnBase_unit_faces L hA M h₁ h₂ h₃
exact back (nonempty_iso_unit_of_locIsoOnBase_unit_faces_of_isNoetherianRing L₀ hA₀ M₀ k₁ k₂ k₃)