ChartSectionsBaseChange.lean

theorem sectionFibrePoint_sectionBaseChange_comp
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    (γ : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    {k : Type u} [Field k] (s : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of S)) :
    (sectionFibrePoint (sectionBaseChange S γ) s).1 ≫
        (pullbackLeftPullbackSndIso c (specMap R S) s).hom =
      (sectionFibrePoint γ (s ≫ specMap R S)).1

theorem HasChartSections.baseChange
    {R : Type u} [CommRing R] {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of R)) {n g r : ℕ}
    (γ : Fin n → Fin (r - g) → SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (hγ : HasChartSections c γ) (S : Type u) [CommRing S] [Algebra R S] :
    HasChartSections (SmoothProperCurve.baseChange R c S)
      (fun i j => sectionBaseChange S (γ i j)) := by
  intro k _ _ s
  obtain ⟨L, hL, hKL, M, e, he, hRR, hdim⟩ := hγ k (s ≫ specMap R S)
  let a := pullbackLeftPullbackSndIso c (specMap R S) s
  let e' := e ≪≫ a.symm
  have he' : e'.hom ≫ pullback.snd (SmoothProperCurve.baseChange R c S) s = M.toBase := by
    change (e.hom ≫ a.inv) ≫
      pullback.snd (SmoothProperCurve.baseChange R c S) s = M.toBase
    rw [Category.assoc, pullbackLeftPullbackSndIso_inv_snd_snd]
    exact he
  refine ⟨L, hL, hKL, M, e', he', hRR, ?_⟩
  intro D hD hdeg
  obtain ⟨i, hi⟩ := hdim D hD hdeg
  refine ⟨i, ?_⟩
  have hpoints (j : Fin (r - g)) :
      (⟨(sectionFibrePoint (sectionBaseChange S (γ i j)) s).1 ≫ e'.inv,
        by rw [Category.assoc, ← he', e'.inv_hom_id_assoc]
           exact (sectionFibrePoint (sectionBaseChange S (γ i j)) s).2⟩ :
          SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) M.toBase) =
      ⟨(sectionFibrePoint (γ i j) (s ≫ specMap R S)).1 ≫ e.inv,
        by rw [Category.assoc, ← he, e.inv_hom_id_assoc]
           exact (sectionFibrePoint (γ i j) (s ≫ specMap R S)).2⟩ := by
    apply Subtype.ext
    change (sectionFibrePoint (sectionBaseChange S (γ i j)) s).1 ≫ (a.hom ≫ e.inv) = _
    rw [← Category.assoc, sectionFibrePoint_sectionBaseChange_comp]
  have hsum : (∑ j : Fin (r - g), Finsupp.single
      (M.pointEquivPlace
        ⟨(sectionFibrePoint (sectionBaseChange S (γ i j)) s).1 ≫ e'.inv,
          by rw [Category.assoc, ← he', e'.inv_hom_id_assoc]
             exact (sectionFibrePoint (sectionBaseChange S (γ i j)) s).2⟩) (1 : ℤ)) =
      ∑ j : Fin (r - g), Finsupp.single
      (M.pointEquivPlace
        ⟨(sectionFibrePoint (γ i j) (s ≫ specMap R S)).1 ≫ e.inv,
          by rw [Category.assoc, ← he, e.inv_hom_id_assoc]
             exact (sectionFibrePoint (γ i j) (s ≫ specMap R S)).2⟩) (1 : ℤ) := by
    apply Finset.sum_congr rfl
    intro j _
    rw [hpoints]
  rw [hsum]
  exact hi