AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isGreatest_opens_difference_extension_of_dense.GoodReductionJacobian.RelativeGroupLaw.WeilExtField.DOM.main
Source context 19 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isGreatest_opens_difference_extension_of_dense
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
noncomputable section
namespace GoodReductionJacobian
namespace RelativeGroupLaw
namespace WeilExtField
namespace DOM
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
section Main2
variable {k : Type u} [Field k] {T : Scheme.{u}}
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of k)}
Lean source · full declarationtheorem main (G : RelativeGroupLaw k f) [IsSeparated f]
(t : T ⟶ Spec (CommRingCat.of k)) [Smooth t]
(V : T.Opens) (hV : Dense (V : Set T))
(v : SchemeHomOver (V.ι ≫ t) f) :
∃ (W : (pullback t t).Opens) (d : SchemeHomOver (W.ι ≫ pullback.fst t t ≫ t) f),
(∀ p : ↑(pullback t t), (pullback.fst t t).base p ∈ V → (pullback.snd t t).base p ∈ V → p ∈
W) ∧
(∀ (S : Scheme.{u}) (a : S ⟶ ↑W) (b c : S ⟶ ↑V)
(hb : a ≫ W.ι ≫ pullback.fst t t = b ≫ V.ι) (hc : a ≫ W.ι ≫ pullback.snd t t = c ≫ V.ι),
G.mul (a ≫ W.ι ≫ pullback.fst t t ≫ t)
⟨a ≫ d.1, by rw [Category.assoc, d.2]⟩
⟨c ≫ v.1, by rw [Category.assoc, v.2, ← Category.assoc, ← hc, Category.assoc,
Category.assoc,
← pullback.condition]⟩ =
⟨b ≫ v.1, by rw [Category.assoc, v.2, ← Category.assoc, ← hb, Category.assoc,
Category.assoc]⟩) ∧
(∀ (W' : (pullback t t).Opens) (d' : SchemeHomOver (W'.ι ≫ pullback.fst t t ≫ t) f)
(W₀ : (pullback t t).Opens) (h₀ : W₀ ≤ W ⊓ W'),
((W' : Set ↑(pullback t t)) ⊆ closure (W₀ : Set ↑(pullback t t))) →
(pullback t t).homOfLE (h₀.trans inf_le_left) ≫ d.1 =
(pullback t t).homOfLE (h₀.trans inf_le_right) ≫ d'.1 →
W' ≤ W ∧ ∀ (S : Scheme.{u}) (a' : S ⟶ ↑W') (a : S ⟶ ↑W), a' ≫ W'.ι = a ≫ W.ι →
a' ≫ d'.1 = a ≫ d.1) := by
have : IsReduced (pullback t t) := isReduced_pullback t
have : A.IsSeparated := isSeparated_of_isSeparated_over f
let : (pullback t t).Over (Spec (CommRingCat.of k)) := ⟨pullback.fst t t ≫ t⟩
let : A.Over (Spec (CommRingCat.of k)) := ⟨f⟩
have hDd : Dense ((prodOpen t V : (pullback t t).Opens) : Set ↑(pullback t t)) := dense_prodOpen
t V hV
let pΦ : (pullback t t).PartialMap A := ⟨prodOpen t V, hDd, (diffMap G t V v).1⟩
have hpΦ : pΦ.IsOver (Spec (CommRingCat.of k)) := by
rw [Scheme.PartialMap.isOver_iff, Scheme.PartialMap.compHom_hom]
exact (diffMap G t V v).2
let u := pΦ.toRationalMap
have hu : u.IsOver (Spec (CommRingCat.of k)) := ⟨⟨pΦ, hpΦ, rfl⟩⟩
let dW := u.toPartialMap
have hdWover : dW.IsOver (Spec (CommRingCat.of k)) :=
Scheme.PartialMap.isOver_toRationalMap_iff_of_isSeparated.mp
(by rw [Scheme.RationalMap.toRationalMap_toPartialMap]; exact hu)
have hdW : dW.hom ≫ f = dW.domain.ι ≫ pullback.fst t t ≫ t := by
have h := Scheme.PartialMap.isOver_iff.mp hdWover
rwa [Scheme.PartialMap.compHom_hom] at h
have hDW : prodOpen t V ≤ u.domain := pΦ.le_domain_toRationalMap
have hres : (pullback t t).homOfLE hDW ≫ dW.hom = (diffMap G t V v).1 := by
have h := Scheme.PartialMap.toPartialMap_toRationalMap_restrict pΦ
erw [Scheme.PartialMap.restrict_hom] at h
exact h
refine ⟨u.domain, ⟨dW.hom, hdW⟩, ?_, ?_, ?_⟩
· intro p h1 h2
exact hDW (show p ∈ prodOpen t V from ⟨h1, h2⟩)
· intro S a b c hb hc
have hrange : Set.range (a ≫ u.domain.ι).base ⊆ Set.range (prodOpen t V).ι.base := by
rintro _ ⟨s, rfl⟩
rw [Scheme.Opens.range_ι]
change (a ≫ u.domain.ι).base s ∈ prodOpen t V
rw [mem_prodOpen_iff]
constructor
· have e : (pullback.fst t t).base (u.domain.ι.base (a.base s)) = V.ι.base (b.base s) := by
have e0 := congrArg (fun k => k.base s) hb
simpa using e0
change (pullback.fst t t).base (u.domain.ι.base (a.base s)) ∈ V
rw [e]; exact mem_opens_of_base V _
· have e : (pullback.snd t t).base (u.domain.ι.base (a.base s)) = V.ι.base (c.base s) := by
have e0 := congrArg (fun k => k.base s) hc
simpa using e0
change (pullback.snd t t).base (u.domain.ι.base (a.base s)) ∈ V
rw [e]; exact mem_opens_of_base V _
let a' := IsOpenImmersion.lift (prodOpen t V).ι (a ≫ u.domain.ι) hrange
have ha' : a' ≫ (prodOpen t V).ι = a ≫ u.domain.ι := IsOpenImmersion.lift_fac _ _ _
have haa : a' ≫ (pullback t t).homOfLE hDW = a := by
rw [← cancel_mono u.domain.ι, Category.assoc, Scheme.homOfLE_ι, ha']
refine recovery_core G t V v _ _ _ _ a' b c ?_ ?_ rfl rfl ?_ ?_
· rw [← Category.assoc a', ha', Category.assoc]
· change a ≫ dW.hom = a' ≫ (diffMap G t V v).1
calc
a ≫ dW.hom = (a' ≫ (pullback t t).homOfLE hDW) ≫ dW.hom :=
congrArg (fun z : S ⟶ ↑u.domain => z ≫ dW.hom) haa.symm
_ = a' ≫ ((pullback t t).homOfLE hDW ≫ dW.hom) := Category.assoc _ _ _
_ = a' ≫ (diffMap G t V v).1 :=
congrArg (fun z : ↑(prodOpen t V) ⟶ A => a' ≫ z) hres
· rw [← cancel_mono V.ι, Category.assoc, bD_ι, ← Category.assoc, ha', Category.assoc]
exact hb
· rw [← cancel_mono V.ι, Category.assoc, cD_ι, ← Category.assoc, ha', Category.assoc]
exact hc
· intro W' d' W₀ h₀ hcl hagree
have hdense' : ((u.domain ⊓ W' : (pullback t t).Opens) : Set ↑(pullback t t)) ⊆ closure (W₀ :
Set _) :=
fun p hp => hcl hp.2
obtain ⟨g, hg₁, hg₂⟩ := exists_glue_of_eq_on_dense
(pullback.fst t t ≫ t) f u.domain W' dW.hom d'.1 hdW d'.2 W₀ h₀ hdense' hagree
have hDsup : prodOpen t V ≤ u.domain ⊔ W' := hDW.trans le_sup_left
let q : (pullback t t).PartialMap A := ⟨u.domain ⊔ W', hDd.mono (fun p hp => hDsup hp), g⟩
have hq : q.toRationalMap = u := by
rw [show u = pΦ.toRationalMap from rfl, Scheme.PartialMap.toRationalMap_eq_iff]
refine ⟨prodOpen t V, hDd, hDsup, le_rfl, ?_⟩
rw [Scheme.PartialMap.restrict_hom, Scheme.PartialMap.restrict_hom]
change (pullback t t).homOfLE hDsup ≫ g = (pullback t t).homOfLE le_rfl ≫ (diffMap G t V v).1
rw [← hres, ← hg₁]
simp only [← Category.assoc, Scheme.homOfLE_homOfLE]
have hle : u.domain ⊔ W' ≤ u.domain := by
have h := q.le_domain_toRationalMap
rwa [hq] at h
refine ⟨le_sup_right.trans hle, ?_⟩
intro S a' a haa'
have e : a' ≫ (pullback t t).homOfLE (le_sup_right : W' ≤ u.domain ⊔ W') =
a ≫ (pullback t t).homOfLE (le_sup_left : u.domain ≤ u.domain ⊔ W') := by
rw [← cancel_mono (u.domain ⊔ W').ι, Category.assoc, Scheme.homOfLE_ι, Category.assoc,
Scheme.homOfLE_ι]
exact haa'
change a' ≫ d'.1 = a ≫ dW.hom
rw [← hg₂, ← hg₁, ← Category.assoc, e, Category.assoc]