AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_extension_of_diagonal_difference_extension_of_dense.GoodReductionJacobian.RelativeGroupLaw.WeilExtField.DESC.main
Source context 16 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_extension_of_diagonal_difference_extension_of_dense
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
namespace WeilExtField
namespace DESC
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian
Lean source · full declarationtheorem main
(k : Type u) [Field k]
{A T : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of k)} (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)
(hd : (∀ x : T, (pullback.diagonal t).base x ∈ 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]⟩)) :
∃ φ : SchemeHomOver t f, V.ι ≫ φ.1 = v.1 := by
set p := pZ t V W with hp
set r := rZ G t V v W d with hr
have hsurj : Function.Surjective p.base := pZ_surjective k t V W hV hd.1
have : Surjective p := ⟨hsurj⟩
let K := pullback p p
have hcompat : pullback.fst p p ≫ r.1 = pullback.snd p p ≫ r.1 := by
have : IsReduced K := isReduced_kernelPair k t V W
let KV : K.Opens := (pullback.fst p p ≫ p) ⁻¹ᵁ V
have : IsDominant KV.ι := by
rw [isDominant_iff, DenseRange, Scheme.Opens.range_ι]
exact dense_kernelPair_fstV k t V W hV
have hfg : (pullback.fst p p ≫ r.1) ≫ f = (pullback.snd p p ≫ r.1) ≫ f := by
rw [Category.assoc, Category.assoc, hr, rZ_base, ← hp, pullback.condition_assoc]
refine ext_of_isDominant_of_isSeparated f hfg KV.ι ?_
let b : (KV : Scheme.{u}) ⟶ (V : Scheme.{u}) := (pullback.fst p p ≫ p).resLE V KV le_rfl
have hb : b ≫ V.ι = KV.ι ≫ pullback.fst p p ≫ p := Scheme.Hom.resLE_comp_ι _ _
have h1 : (KV.ι ≫ pullback.fst p p) ≫ r.1 = b ≫ v.1 :=
comp_rZ_eq_of_fst G t V v W d hd.2 _ b (by rw [hb, Category.assoc])
have h2 : (KV.ι ≫ pullback.snd p p) ≫ r.1 = b ≫ v.1 :=
comp_rZ_eq_of_fst G t V v W d hd.2 _ b (by rw [hb, Category.assoc, ← pullback.condition])
rw [← Category.assoc, ← Category.assoc, h1, h2]
have hmem : Sieve.generate (Presieve.singleton p) ∈ Scheme.fppfTopology.{u} T := by
have h := (Scheme.Hom.cover.{u, 0} (P := @Flat ⊓ @LocallyOfFinitePresentation) p
⟨inferInstance, inferInstance⟩).mem_grothendieckTopology
dsimp only [Scheme.Hom.cover, Precoverage.ZeroHypercover.singleton,
PreZeroHypercover.singleton] at h
rw [Sieve.ofArrows, Presieve.ofArrows_pUnit] at h
exact h
have hSA : Presieve.IsSheaf Scheme.fppfTopology.{u} (yoneda.obj A) :=
GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable _
have hSB : Presieve.IsSheaf Scheme.fppfTopology.{u} (yoneda.obj (Spec (CommRingCat.of k))) :=
GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable _
have hsheafA : Presieve.IsSheafFor (yoneda.obj A) (Presieve.singleton p) := by
rw [Presieve.isSheafFor_iff_generate]
exact hSA _ hmem
have hsheafB : Presieve.IsSheafFor (yoneda.obj (Spec (CommRingCat.of k))) (Presieve.singleton p)
:= by
rw [Presieve.isSheafFor_iff_generate]
exact hSB _ hmem
rw [Presieve.isSheafFor_singleton] at hsheafA hsheafB
have hcompat' : ∀ {Z : Scheme.{u}} (p₁ p₂ : Z ⟶ ↑(Zop t V W)), p₁ ≫ p = p₂ ≫ p →
(yoneda.obj A).map p₁.op r.1 = (yoneda.obj A).map p₂.op r.1 := by
intro Z p₁ p₂ h12
change p₁ ≫ r.1 = p₂ ≫ r.1
rw [← pullback.lift_fst p₁ p₂ h12, Category.assoc, hcompat, ← Category.assoc, pullback.lift_snd]
obtain ⟨φ₁, hφ₁, huniq⟩ := hsheafA r.1 hcompat'
change p ≫ φ₁ = r.1 at hφ₁
have hover : φ₁ ≫ f = t := by
have hcB : ∀ {Z : Scheme.{u}} (p₁ p₂ : Z ⟶ ↑(Zop t V W)), p₁ ≫ p = p₂ ≫ p →
(yoneda.obj (Spec (CommRingCat.of k))).map p₁.op (p ≫ t) =
(yoneda.obj (Spec (CommRingCat.of k))).map p₂.op (p ≫ t) := by
intro Z p₁ p₂ h12
change p₁ ≫ p ≫ t = p₂ ≫ p ≫ t
rw [← Category.assoc, h12, Category.assoc]
obtain ⟨ψ, hψ, hψuniq⟩ := hsheafB (p ≫ t) hcB
have e1 : φ₁ ≫ f = ψ := hψuniq (φ₁ ≫ f) (by
change p ≫ φ₁ ≫ f = p ≫ t
rw [← Category.assoc, hφ₁, hr, rZ_base])
have e2 : t = ψ := hψuniq t rfl
rw [e1, ← e2]
refine ⟨⟨φ₁, hover⟩, ?_⟩
let e : (V : Scheme.{u}) ⟶ pullback t t := pullback.lift V.ι V.ι rfl
have he : e = V.ι ≫ pullback.diagonal t := by
apply pullback.hom_ext
· rw [pullback.lift_fst, Category.assoc, pullback.diagonal_fst, Category.comp_id]
· rw [pullback.lift_snd, Category.assoc, pullback.diagonal_snd, Category.comp_id]
have herange : Set.range e.base ⊆ Set.range (Zop t V W).ι.base := by
rw [Scheme.Opens.range_ι]
rintro _ ⟨y, rfl⟩
change e.base y ∈ Zop t V W
rw [Zop, TopologicalSpace.Opens.mem_inf]
refine ⟨?_, ?_⟩
· rw [he, Scheme.Hom.comp_apply]; exact hd.1 _
· rw [Scheme.Hom.mem_preimage, ← Scheme.Hom.comp_apply, pullback.lift_snd]; exact y.2
let δ : (V : Scheme.{u}) ⟶ ↑(Zop t V W) := IsOpenImmersion.lift (Zop t V W).ι e herange
have hδ : δ ≫ (Zop t V W).ι = e := IsOpenImmersion.lift_fac _ _ _
have hδp : δ ≫ p = 𝟙 _ ≫ V.ι := by
rw [hp, pZ_def, ← Category.assoc, hδ, pullback.lift_fst, Category.id_comp]
have hrec := comp_rZ_eq_of_fst G t V v W d hd.2 δ (𝟙 _) hδp
rw [Category.id_comp] at hrec
have hδp' : δ ≫ p = V.ι := by rw [hδp, Category.id_comp]
change V.ι ≫ φ₁ = v.1
calc V.ι ≫ φ₁ = (δ ≫ p) ≫ φ₁ := by rw [hδp']
_ = δ ≫ r.1 := by rw [Category.assoc, hφ₁]
_ = v.1 := hrec