AlgebraicGeometry.RelPicard.RigidifiedLineBundle.exists_isNoetherianRing_model_of_fg_subalgebra_model_of_locIsoOnBase_unit_faces
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry.RelPicard.RigidifiedLineBundle
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open NeronModelInfra GoodReductionJacobian AlgebraicGeometry.Polarisation
open scoped JacobianVarieties.Picard.Proofs.NoetherianUnitFaceModel.CFDStages
open _root_.JacobianVarieties.Picard.Proofs.NoetherianUnitFaceModel in
open CFDStages CFDAsm in
Lean source · full declarationtheorem
exists_isNoetherianRing_model_of_fg_subalgebra_model_of_locIsoOnBase_unit_faces
{S : Type} [CommRing S] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of S)}
(L : RelativeGroupLaw 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₁ : Subalgebra ℤ S) (hS₁ : S₁.FG)
(A₁ : Scheme.{0}) (f₁ : A₁ ⟶ Spec (CommRingCat.of ↥S₁)) (L₁ : RelativeGroupLaw ↥S₁ f₁)
(hA₁ : AbelianSchemePropertyBundle ↥S₁ f₁)
(a : A ⟶ A₁) (ha : IsPullback a f f₁ (Spec.map (CommRingCat.ofHom S₁.val.toRingHom)))
(hLa : ∀ (T : Scheme.{0}) (t : T ⟶ Spec (CommRingCat.of S)) (P Q : SchemeHomOver t f),
(L.mul t P Q).1 ≫ a = (L₁.mul (t ≫ Spec.map (CommRingCat.ofHom S₁.val.toRingHom))
⟨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)
(M₁ : RigidifiedLineBundle (prodStr f₁ f₁) ((L₁.prod L₁).one (𝟙 (Spec (CommRingCat.of ↥S₁))))
f₁)
(hM : Nonempty (M.L ≅ (Scheme.Modules.pullback
(pullback.map (prodStr f f) f (prodStr f₁ f₁) f₁
(pullback.map f f f₁ f₁ a a (Spec.map (CommRingCat.ofHom S₁.val.toRingHom)) ha.w.symm
ha.w.symm)
a (Spec.map (CommRingCat.ofHom S₁.val.toRingHom))
(by
have h1 : pullback.map f f f₁ f₁ a a (Spec.map (CommRingCat.ofHom S₁.val.toRingHom))
ha.w.symm ha.w.symm ≫
pullback.fst f₁ f₁ = pullback.fst f f ≫ a := pullback.lift_fst _ _ _
change (pullback.fst f f ≫ f) ≫ Spec.map (CommRingCat.ofHom S₁.val.toRingHom) =
pullback.map f f f₁ f₁ a a (Spec.map (CommRingCat.ofHom S₁.val.toRingHom)) ha.w.symm
ha.w.symm ≫
pullback.fst f₁ f₁ ≫ f₁
rw [Category.assoc, ← Category.assoc (pullback.map _ _ _ _ _ _ _ _ _), h1,
Category.assoc, ha.w])
ha.w.symm)).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
classical
obtain ⟨eM⟩ := hM
have : IsProper f₁ := hA₁.proper
have : QuasiCompact (prodStr f₁ f₁) := inferInstance
have : QuasiSeparated (prodStr f₁ f₁) := inferInstance
have hne : Nonempty (Idx S₁) := nonempty S₁ hS₁
have hDL := isDirectLimit S₁ hS₁
let i₀ : Idx S₁ := ⟨S₁, hS₁, le_rfl⟩
have hF := AlgebraicGeometry.Polarisation.locIsoOnBase_faces_pullback_cube_iff_of_isPullback L₁
S₁.val.toRingHom L a ha hLa M₁.L
have EQ := AlgebraicGeometry.Polarisation.LocIsoOnBase.equivalence (prodStr f f)
have d₁ := hF.1.mp (EQ.trans (ofIso _ ((Scheme.Modules.pullback _).mapIso eM).symm) h₁)
have d₂ := hF.2.1.mp (EQ.trans (ofIso _ ((Scheme.Modules.pullback _).mapIso eM).symm) h₂)
have d₃ := hF.2.2.mp (EQ.trans (ofIso _ ((Scheme.Modules.pullback _).mapIso eM).symm) h₃)
obtain ⟨k₁, hk₁, e₁⟩ :=
exists_locIsoOnBase_pullback_unit_stage_of_locIsoOnBase_pullback_unit_of_isDirectLimit
(φ S₁) (g S₁) hDL i₀ (prodStr f₁ f₁) _ ((M₁.isInvertible).pullback _) d₁
obtain ⟨k₂, hk₂, e₂⟩ :=
exists_locIsoOnBase_pullback_unit_stage_of_locIsoOnBase_pullback_unit_of_isDirectLimit
(φ S₁) (g S₁) hDL i₀ (prodStr f₁ f₁) _ ((M₁.isInvertible).pullback _) d₂
obtain ⟨k₃, hk₃, e₃⟩ :=
exists_locIsoOnBase_pullback_unit_stage_of_locIsoOnBase_pullback_unit_of_isDirectLimit
(φ S₁) (g S₁) hDL i₀ (prodStr f₁ f₁) _ ((M₁.isInvertible).pullback _) d₃
obtain ⟨k₁₂, h₁, h₂'⟩ := exists_ge_ge k₁ k₂
obtain ⟨k, h₁₂, h₃'⟩ := exists_ge_ge k₁₂ k₃
have hk : i₀ ≤ k := hk₁.trans (h₁.trans h₁₂)
have r₁ := rebase (prodStr f₁ f₁) (φ S₁ i₀ k₁ hk₁) (φ S₁ i₀ k hk) (φ S₁ k₁ k (h₁.trans h₁₂)) rfl
_ e₁
have r₂ := rebase (prodStr f₁ f₁) (φ S₁ i₀ k₂ hk₂) (φ S₁ i₀ k hk) (φ S₁ k₂ k (h₂'.trans h₁₂)) rfl
_ e₂
have r₃ := rebase (prodStr f₁ f₁) (φ S₁ i₀ k₃ hk₃) (φ S₁ i₀ k hk) (φ S₁ k₃ k h₃') rfl _ e₃
let S₀ : Type := G S₁ k
have : IsNoetherianRing S₀ := by
have : Algebra.FiniteType ℤ ↥k.1 := (Subalgebra.fg_iff_finiteType _).mp k.2.1
exact Algebra.FiniteType.isNoetherianRing ℤ ↥k.1
let σ : Spec (CommRingCat.of S₀) ⟶ Spec (CommRingCat.of ↥S₁) := Spec.map (CommRingCat.ofHom (φ S₁
i₀ k hk))
let f₀ : pullback f₁ σ ⟶ Spec (CommRingCat.of S₀) := pullback.snd f₁ σ
let L₀ : RelativeGroupLaw S₀ f₀ := L₁.baseChange σ
have ha₀ : IsPullback (pullback.fst f₁ σ) f₀ f₁ σ := IsPullback.of_hasPullback f₁ σ
have hA₀ : AbelianSchemePropertyBundle S₀ f₀ :=
GoodReductionJacobian.AbelianSchemePropertyBundle.of_isPullback hA₁ ha₀
have hLa₀ : ∀ (T : Scheme.{0}) (t : T ⟶ Spec (CommRingCat.of S₀)) (P Q : SchemeHomOver t f₀),
(L₀.mul t P Q).1 ≫ pullback.fst f₁ σ = (L₁.mul (t ≫ σ)
⟨P.1 ≫ pullback.fst f₁ σ, by rw [Category.assoc, ha₀.w, ← Category.assoc, P.2]⟩
⟨Q.1 ≫ pullback.fst f₁ σ, by rw [Category.assoc, ha₀.w, ← Category.assoc, Q.2]⟩).1 :=
fun T t P Q => congrArg Subtype.val (L₁.baseChangePointToBase_mul σ t P Q)
obtain ⟨M₀, hM₀⟩ := exists_rigidified_cube_pullback_of_isPullback
L₁ (φ S₁ i₀ k hk) L₀ (pullback.fst f₁ σ) ha₀ hLa₀ M₁
have hF₀ := AlgebraicGeometry.Polarisation.locIsoOnBase_faces_pullback_cube_iff_of_isPullback
L₁ (φ S₁ i₀ k hk) L₀ (pullback.fst f₁ σ) ha₀ hLa₀ M₁.L
refine ⟨S₀, inferInstance, inferInstance, pullback f₁ σ, f₀, L₀, hA₀, M₀, ?_, ?_, ?_, ?_⟩
· rw [hM₀]; exact hF₀.1.mpr r₁
· rw [hM₀]; exact hF₀.2.1.mpr r₂
· rw [hM₀]; exact hF₀.2.2.mpr r₃
· rintro ⟨e₀⟩
have hσ : Spec.map (CommRingCat.ofHom (g S₁ k)) ≫ σ = Spec.map (CommRingCat.ofHom
S₁.val.toRingHom) := by
change Spec.map (CommRingCat.ofHom (g S₁ k)) ≫ Spec.map (CommRingCat.ofHom (φ S₁ i₀ k hk)) = _
rw [← Spec.map_comp, ← CommRingCat.ofHom_comp]
rfl
let ψ : Spec (CommRingCat.of S) ⟶ Spec (CommRingCat.of S₀) := Spec.map (CommRingCat.ofHom (g S₁
k))
let c : A ⟶ pullback f₁ σ := pullback.lift a (f ≫ ψ) (by rw [Category.assoc, hσ]; exact ha.w)
have hc₁ : c ≫ pullback.fst f₁ σ = a := pullback.lift_fst _ _ _
have hc₂ : c ≫ f₀ = f ≫ ψ := pullback.lift_snd _ _ _
let cc : pullback f f ⟶ pullback f₀ f₀ := pullback.map f f f₀ f₀ c c ψ hc₂.symm hc₂.symm
have hcc₁ : cc ≫ pullback.fst f₀ f₀ = pullback.fst f f ≫ c := pullback.lift_fst _ _ _
have hcc₂ : cc ≫ pullback.snd f₀ f₀ = pullback.snd f f ≫ c := pullback.lift_snd _ _ _
let γ : pullback (prodStr f f) f ⟶ pullback (prodStr f₀ f₀) f₀ :=
pullback.map (prodStr f f) f (prodStr f₀ f₀) f₀ cc c ψ
(by
change (pullback.fst f f ≫ f) ≫ ψ = cc ≫ pullback.fst f₀ f₀ ≫ f₀
rw [← Category.assoc, hcc₁, Category.assoc, Category.assoc, hc₂])
hc₂.symm
have hγ₁ : γ ≫ pullback.fst (prodStr f₀ f₀) f₀ = pullback.fst (prodStr f f) f ≫ cc :=
pullback.lift_fst _ _ _
have hγ₂ : γ ≫ pullback.snd (prodStr f₀ f₀) f₀ = pullback.snd (prodStr f f) f ≫ c :=
pullback.lift_snd _ _ _
let aa := pullback.map f f f₁ f₁ a a (Spec.map (CommRingCat.ofHom S₁.val.toRingHom)) ha.w.symm
ha.w.symm
have haa₁ : aa ≫ pullback.fst f₁ f₁ = pullback.fst f f ≫ a := pullback.lift_fst _ _ _
have haa₂ : aa ≫ pullback.snd f₁ f₁ = pullback.snd f f ≫ a := pullback.lift_snd _ _ _
let bb := pullback.map f₀ f₀ f₁ f₁ (pullback.fst f₁ σ) (pullback.fst f₁ σ) σ ha₀.w.symm
ha₀.w.symm
have hbb₁ : bb ≫ pullback.fst f₁ f₁ = pullback.fst f₀ f₀ ≫ pullback.fst f₁ σ :=
pullback.lift_fst _ _ _
have hbb₂ : bb ≫ pullback.snd f₁ f₁ = pullback.snd f₀ f₀ ≫ pullback.fst f₁ σ :=
pullback.lift_snd _ _ _
have hccbb : cc ≫ bb = aa := by
apply pullback.hom_ext
· rw [Category.assoc, hbb₁, ← Category.assoc, hcc₁, Category.assoc, hc₁, haa₁]
· rw [Category.assoc, hbb₂, ← Category.assoc, hcc₂, Category.assoc, hc₁, haa₂]
obtain ⟨AAA, hAAA₁, hAAA₂, ⟨hAAA⟩⟩ : ∃ AAA : pullback (prodStr f f) f ⟶ pullback (prodStr f₁
f₁) f₁,
AAA ≫ pullback.fst _ _ = pullback.fst _ _ ≫ aa ∧ AAA ≫ pullback.snd _ _ = pullback.snd _ _
≫ a ∧
Nonempty (M.L ≅ (Scheme.Modules.pullback AAA).obj M₁.L) :=
⟨_, pullback.lift_fst _ _ _, pullback.lift_snd _ _ _, ⟨eM⟩⟩
obtain ⟨BBB, hBBB, hBBB₁, hBBB₂⟩ : ∃ BBB : pullback (prodStr f₀ f₀) f₀ ⟶ pullback (prodStr f₁
f₁) f₁,
M₀.L = (Scheme.Modules.pullback BBB).obj M₁.L ∧ BBB ≫ pullback.fst _ _ = pullback.fst _ _ ≫
bb ∧
BBB ≫ pullback.snd _ _ = pullback.snd _ _ ≫ pullback.fst f₁ σ :=
⟨_, hM₀, pullback.lift_fst _ _ _, pullback.lift_snd _ _ _⟩
have key : γ ≫ BBB = AAA := by
apply pullback.hom_ext
· rw [Category.assoc, hBBB₁, ← Category.assoc, hγ₁, Category.assoc, hccbb, hAAA₁]
· rw [Category.assoc, hBBB₂, ← Category.assoc, hγ₂, Category.assoc, hc₁, hAAA₂]
refine ⟨hAAA ≪≫ (Scheme.Modules.pullbackCongr key.symm).app M₁.L ≪≫
((Scheme.Modules.pullbackComp γ BBB).app M₁.L).symm ≪≫
(Scheme.Modules.pullback γ).mapIso (eqToIso hBBB.symm ≪≫ e₀) ≪≫
Scheme.Modules.pullbackUnitIso γ⟩