AlgebraicGeometry.RelPicard.RigidifiedLineBundle.exists_isNoetherianRing_model_of_locIsoOnBase_unit_faces
Descend the group law and the three face trivializations through finite generated models.
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 exists_isNoetherianRing_model_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) (𝟙_ _)) :
∃ (S₀ : Type) (_ : CommRing S₀) (_ : IsNoetherianRing S₀) (A₀ : Scheme) (f₀ : A₀ ⟶ Spec
(CommRingCat.of S₀))
(L₀ : RelativeGroupLaw S₀ f₀) (_ : AbelianSchemePropertyBundle S₀ f₀)
(M₀ : RigidifiedLineBundle (prodStr f₀ f₀) ((L₀.prod L₀).one (𝟙 (Spec (CommRingCat.of S₀))))
f₀),
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) (𝟙_ _) ∧
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) (𝟙_ _) ∧
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) →
Nonempty (M.L ≅ (RigidifiedLineBundle.unit (c := prodStr f f) (ε := (L.prod L).one (𝟙 (Spec
(CommRingCat.of S)))) f).L)) := by
obtain ⟨S₁, hS₁, A₁, f₁, L₁, _, hA₁, a, ha, hLa, M₁, hM⟩ :=
exists_fg_subalgebra_isPullback_prodStr_model L hA M
exact exists_isNoetherianRing_model_of_fg_subalgebra_model_of_locIsoOnBase_unit_faces
L M h₁ h₂ h₃ S₁ hS₁ A₁ f₁ L₁ hA₁ a ha hLa M₁ hM