AlgebraicGeometry.RelPicard.HasChartSections.of_iso
Transporting sections by an isomorphism of curves preserves the actual Riemann--Roch point-removal condition on all geometric fibres.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open AlgebraicGeometry.SmoothProperCurve NeronModelInfra AlgebraicCurve
namespace AlgebraicGeometry.RelPicardLean source · full declaration
theorem HasChartSections.of_iso
{R : Type u} [CommRing R] {C D : Scheme.{u}}
{c : C ⟶ Spec (CommRingCat.of R)} {d : D ⟶ Spec (CommRingCat.of R)}
(a : C ≅ D) (ha : a.hom ≫ d = c) {n g r : ℕ}
(γ : Fin n → Fin (r - g) → SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
(hγ : HasChartSections c γ) :
HasChartSections d (fun i j =>
⟨(γ i j).1 ≫ a.hom, by rw [Category.assoc, ha]; exact (γ i j).2⟩) := by
intro k _ _ s
obtain ⟨L, hL, hKL, M, e, he, hRR, hdim⟩ := hγ k s
let p : pullback c s ⟶ pullback d s :=
pullback.map c s d s a.hom (𝟙 _) (𝟙 _)
(by rw [Category.comp_id, ha]) (by rw [Category.comp_id, Category.id_comp])
have hp : IsIso p := inferInstance
let E : pullback c s ≅ pullback d s := asIso p
let e' : M.C ≅ pullback d s := e ≪≫ E
have hEsnd : E.hom ≫ pullback.snd d s = pullback.snd c s := by
change p ≫ pullback.snd d s = _
simp only [p, pullback.lift_snd, Category.comp_id]
have he' : e'.hom ≫ pullback.snd d s = M.toBase := by
change (e.hom ≫ E.hom) ≫ pullback.snd d s = M.toBase
rw [Category.assoc, hEsnd, he]
refine ⟨L, hL, hKL, M, e', he', hRR, ?_⟩
intro Z hZ hdeg
obtain ⟨i, hi⟩ := hdim Z hZ hdeg
refine ⟨i, ?_⟩
have hpoints (j : Fin (r - g)) :
(⟨(sectionFibrePoint
⟨(γ i j).1 ≫ a.hom, by rw [Category.assoc, ha]; exact (γ i j).2⟩ s).1 ≫
e'.inv,
by rw [Category.assoc, ← he', e'.inv_hom_id_assoc]
exact (sectionFibrePoint
⟨(γ i j).1 ≫ a.hom, by rw [Category.assoc, ha]; exact (γ i j).2⟩ s).2⟩ :
SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) M.toBase) =
⟨(sectionFibrePoint (γ i j) s).1 ≫ e.inv,
by rw [Category.assoc, ← he, e.inv_hom_id_assoc]
exact (sectionFibrePoint (γ i j) s).2⟩ := by
have hpoint : (sectionFibrePoint (γ i j) s).1 ≫ E.hom =
(sectionFibrePoint
⟨(γ i j).1 ≫ a.hom, by rw [Category.assoc, ha]; exact (γ i j).2⟩ s).1 := by
apply pullback.hom_ext
· simp only [E, asIso_hom, p, Category.assoc, pullback.lift_fst,
pullback.lift_fst_assoc, sectionFibrePoint]
· simp only [Category.assoc, hEsnd, sectionFibrePoint, pullback.lift_snd]
apply Subtype.ext
change _ ≫ (E.inv ≫ e.inv) = _
rw [← hpoint, Category.assoc, E.hom_inv_id_assoc]
have hsum : (∑ j : Fin (r - g), Finsupp.single
(M.pointEquivPlace
⟨(sectionFibrePoint
⟨(γ i j).1 ≫ a.hom, by rw [Category.assoc, ha]; exact (γ i j).2⟩ s).1 ≫
e'.inv,
by rw [Category.assoc, ← he', e'.inv_hom_id_assoc]
exact (sectionFibrePoint
⟨(γ i j).1 ≫ a.hom, by rw [Category.assoc, ha]; exact (γ i j).2⟩ s).2⟩)
(1 : ℤ)) = ∑ j : Fin (r - g), Finsupp.single
(M.pointEquivPlace
⟨(sectionFibrePoint (γ i j) s).1 ≫ e.inv,
by rw [Category.assoc, ← he, e.inv_hom_id_assoc]
exact (sectionFibrePoint (γ i j) s).2⟩) (1 : ℤ) := by
apply Finset.sum_congr rfl
intro j _
rw [hpoints]
rw [hsum]
exact hi