SameDivisorDescent.lean

theorem bijective_pi_of_injective_characters
    (K : Type u) [Field K] (A : Type v) [CommRing A] [Algebra K A]
    [FiniteDimensional K A] {ι : Type w} [Fintype ι]
    (χ : ι → A →ₐ[K] K) (hχ : Function.Injective χ)
    (hrank : Fintype.card ι = Module.finrank K A) :
    Function.Bijective (AlgHom.pi χ)

theorem isIso_sigmaDesc_specMap_of_injective_characters
    (K A : Type u) [Field K] [CommRing A] [Algebra K A]
    [FiniteDimensional K A] {ι : Type u} [Fintype ι]
    (χ : ι → A →ₐ[K] K) (hχ : Function.Injective χ)
    (hrank : Fintype.card ι = Module.finrank K A) :
    IsIso (Sigma.desc fun i => Spec.map (CommRingCat.ofHom (χ i).toRingHom)) := by
  let e : A ≃ₐ[K] (ι → K) :=
    AlgEquiv.ofBijective (AlgHom.pi χ)
      (bijective_pi_of_injective_characters K A χ hχ hrank)
  have he : IsIso (Spec.map (CommRingCat.ofHom (AlgHom.pi χ).toRingHom)) := by
    change IsIso (Spec.map e.toRingEquiv.toCommRingCatIso.hom)
    infer_instance
  have hfac : (Sigma.desc fun i => Spec.map (CommRingCat.ofHom (χ i).toRingHom)) =
      sigmaSpec (fun _ : ι => CommRingCat.of K) ≫
        Spec.map (CommRingCat.ofHom (AlgHom.pi χ).toRingHom) := by
    apply Sigma.hom_ext
    intro i
    rw [Sigma.ι_comp_desc, ι_sigmaSpec_assoc, ← Spec.map_comp]
    rfl
  rw [hfac]
  infer_instance

theorem isIso_sigmaDesc_of_card_eq_finrank
    {K : Type u} [Field K] {Z : Scheme.{u}}
    (z : Z ⟶ Spec (CommRingCat.of K)) [IsFinite z]
    {ι : Type u} [Fintype ι] (a : ι → (Spec (CommRingCat.of K) ⟶ Z))
    (ha : ∀ i, a i ≫ z = 𝟙 _) (hinj : Function.Injective a)
    (t : Spec (CommRingCat.of K)) (hrank : Fintype.card ι = z.finrank t) :
    IsIso (Sigma.desc a)

theorem integral_finFibrePow
    {K : Type u} [Field K] {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) [Smooth c] [GeometricallyConnected c]
    (r : ℕ) : IsIntegral (finFibrePow c r)

theorem id_ne_basepoint_constant
    {K : Type u} [Field K] {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) [SmoothOfRelativeDimension 1 c]
    (s : Spec (CommRingCat.of K) ⟶ C) : 𝟙 C ≠ c ≫ s

theorem injective_finFibrePow_proj
    {K : Type u} [Field K] {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) [SmoothOfRelativeDimension 1 c]
    (s : Spec (CommRingCat.of K) ⟶ C) (hs : s ≫ c = 𝟙 _) (r : ℕ) :
    Function.Injective (finFibrePow.proj c r)

theorem injective_finFibrePow_permHom
    {K : Type u} [Field K] {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) [SmoothOfRelativeDimension 1 c]
    (s : Spec (CommRingCat.of K) ⟶ C) (hs : s ≫ c = 𝟙 _) (r : ℕ) :
    Function.Injective (finFibrePow.permHom c r)

theorem exists_finiteSumMap_desc
    {K : Type u} [Field K] {C B Y : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) [IsSeparated c]
    [SmoothOfRelativeDimension 1 c] [GeometricallyConnected c]
    (s : Spec (CommRingCat.of K) ⟶ C) (hs : s ≫ c = 𝟙 _)
    {b : B ⟶ Spec (CommRingCat.of K)} [IsProper b] [GeometricallyIntegral b]
    (G : RelativeGroupLaw K b) (q : SchemeHomOver c b)
    {r : ℕ} {y : Y ⟶ Spec (CommRingCat.of K)} {D : RelEffCartierDiv c r y}
    (hU : D.IsUniversal) :
    ∃ (σ : finFibrePow c r ⟶ Y) (hσ : σ ≫ y = finFibrePow.toBase c r)
      (sum : SchemeHomOver y b),
      D.I.comap (mapOnProdOver c σ hσ) = fibrePowOver.tautIdeal c r ∧
      IsFinite σ ∧ Flat σ ∧ Surjective σ ∧
      σ ≫ sum.1 = (G.finiteSumMap c q r).1 ∧
      ∀ {T : Scheme.{u}} (g : T ⟶ Spec (CommRingCat.of K))
        (v w : T ⟶ finFibrePow c r)
        (hv : v ≫ finFibrePow.toBase c r = g)
        (hw : w ≫ finFibrePow.toBase c r = g),
        v ≫ σ = w ≫ σ ↔
          SameDivisor c (fun i => v ≫ finFibrePow.proj c r i)
            (fun i => by rw [Category.assoc, finFibrePow.proj_comp, hv])
            (fun i => w ≫ finFibrePow.proj c r i)
            (fun i => by rw [Category.assoc, finFibrePow.proj_comp, hw]) := by
  classical
  have : Smooth c := SmoothOfRelativeDimension.smooth 1 c
  let X : Scheme.{u} := finFibrePow c r
  have : IsIntegral X := integral_finFibrePow c r
  have : IsSeparated (finFibrePow.toBase c r) :=
    MorphismProperty.widePullback_base (P := @IsSeparated)
      (fun _ : Fin r => C) (fun _ => c) (fun _ => inferInstance)
  obtain ⟨σ, hσ, hI, hfin, hflat, hlfp, hsurj, hrank, hkernel⟩ :=
    hU.exists_sumMap_with_sameDivisor_kernel
  let η : Spec (X.residueField (genericPoint X)) ⟶ X :=
    X.fromSpecResidueField (genericPoint X)
  have : QuasiCompact η :=
    ⟨fun U _ _ => (Set.toFinite (η ⁻¹' U)).isCompact⟩
  have : IsDominant η := ⟨by
    rw [denseRange_iff_closure_range]
    change closure (Set.range (X.fromSpecResidueField (genericPoint X))) = Set.univ
    rw [X.range_fromSpecResidueField]
    exact (genericPoint_spec X).def⟩
  have : IsSchemeTheoreticallyDominant η :=
    IsSchemeTheoreticallyDominant.of_isDominant η
  have hperm (τ : Equiv.Perm (Fin r)) : finFibrePow.permHom c r τ ≫ σ = σ := by
    have h := (hkernel (finFibrePow.toBase c r)
      (finFibrePow.permHom c r τ) (𝟙 X)
      (finFibrePow.permHom_toBase c r τ) (Category.id_comp _)).mpr
    refine (h ?_).trans (Category.id_comp σ)
    change prodKerGraph c _ _ = prodKerGraph c _ _
    simp only [finFibrePow.permHom_proj]
    exact prodKerGraph_comp_equiv c τ⁻¹ (finFibrePow.proj c r)
      (finFibrePow.proj_comp c r)
  let R : Scheme.{u} := pullback σ σ
  let p : R ⟶ X := pullback.fst σ σ
  have : IsFinite p := inferInstanceAs (IsFinite (pullback.fst σ σ))
  have : Flat p := inferInstanceAs (Flat (pullback.fst σ σ))
  let Z : Scheme.{u} := pullback p η
  let z : Z ⟶ Spec (X.residueField (genericPoint X)) := pullback.snd p η
  have : IsFinite z := inferInstanceAs (IsFinite (pullback.snd p η))
  let I : Type u := ULift.{u} (Equiv.Perm (Fin r))
  let a (i : I) : Spec (X.residueField (genericPoint X)) ⟶ Z :=
    pullback.lift
      (pullback.lift η (η ≫ finFibrePow.permHom c r i.down)
        (by rw [Category.assoc, hperm]))
      (𝟙 _) (by rw [pullback.lift_fst, Category.id_comp])
  have ha (i : I) : a i ≫ z = 𝟙 _ := pullback.lift_snd _ _ _
  have ha₁ (i : I) : a i ≫ pullback.fst p η ≫ pullback.fst σ σ = η := by
    rw [pullback.lift_fst_assoc, pullback.lift_fst]
  have ha₂ (i : I) : a i ≫ pullback.fst p η ≫ pullback.snd σ σ =
      η ≫ finFibrePow.permHom c r i.down := by
    rw [pullback.lift_fst_assoc, pullback.lift_snd]
  have hainj : Function.Injective a := by
    intro i j hij
    apply ULift.ext
    apply injective_finFibrePow_permHom c s hs r
    apply ext_of_isDominant_of_isSeparated (finFibrePow.toBase c r)
      ((finFibrePow.permHom_toBase c r i.down).trans
        (finFibrePow.permHom_toBase c r j.down).symm) η
    rw [← ha₂ i, ← ha₂ j, hij]
  have hcard : Fintype.card I = z.finrank (Classical.arbitrary _) := by
    rw [Scheme.Hom.finrank_pullback_snd, Scheme.Hom.finrank_pullback_fst, hrank]
    simp only [I, Fintype.card_ulift, Fintype.card_perm, Fintype.card_fin]
  have : IsIso (Sigma.desc a) := isIso_sigmaDesc_of_card_eq_finrank
    (K := X.residueField (genericPoint X)) (Z := Z)
    z a ha hainj (Classical.arbitrary _) hcard
  have : IsReduced (∐ fun _ : I => Spec (X.residueField (genericPoint X))) := by
    apply (IsReduced.iff_of_openCover _ (sigmaOpenCover _)).mpr
    intro i
    change IsReduced (Spec (X.residueField (genericPoint X)))
    infer_instance
  have : IsReduced Z := isReduced_of_isOpenImmersion (inv (Sigma.desc a))
  have : IsReduced R := IsSchemeTheoreticallyDominant.isReduced (pullback.fst p η)
  let e : X ⟶ B := (G.finiteSumMap c q r).1
  have hpair : pullback.fst σ σ ≫ e = pullback.snd σ σ ≫ e := by
    refine ext_of_isDominant_of_isSeparated b ?_ (pullback.fst p η) ?_
    · rw [Category.assoc, Category.assoc, (G.finiteSumMap c q r).2]
      change pullback.fst σ σ ≫ fibrePowOver.toBase c r =
        pullback.snd σ σ ≫ fibrePowOver.toBase c r
      rw [← hσ, ← Category.assoc, ← Category.assoc, pullback.condition]
    · rw [← cancel_epi (Sigma.desc a)]
      apply Sigma.hom_ext
      intro i
      simp only [Sigma.ι_comp_desc_assoc]
      have hleft := congrArg (· ≫ e) (ha₁ i)
      have hright := congrArg (· ≫ e) (ha₂ i)
      have hinv : (η ≫ finFibrePow.permHom c r i.down) ≫ e = η ≫ e := by
        rw [Category.assoc]
        exact congrArg (η ≫ ·) (G.finiteSumMap_permute c q i.down)
      simpa only [Category.assoc] using hleft.trans (hright.trans hinv).symm
  have hequal : ∀ {T : Scheme.{u}} (v w : T ⟶ X), v ≫ σ = w ≫ σ → v ≫ e = w ≫ e := by
    intro T v w hvw
    have h := congrArg (pullback.lift v w hvw ≫ ·) hpair
    simpa only [pullback.lift_fst_assoc, pullback.lift_snd_assoc] using h
  let d : Y ⟶ B := EffectiveEpi.desc σ e hequal
  have hd : σ ≫ d = e := EffectiveEpi.fac σ e hequal
  have hdb : d ≫ b = y := by
    apply (cancel_epi σ).mp
    rw [← Category.assoc, hd]
    exact (G.finiteSumMap c q r).2.trans hσ.symm
  exact ⟨σ, hσ, ⟨d, hdb⟩, hI, hfin, hflat, hsurj, hd, hkernel⟩

theorem sumList_eq_of_sameDivisor
    {K : Type u} [Field K] {C B Y : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) [IsSeparated c]
    [SmoothOfRelativeDimension 1 c] [GeometricallyConnected c]
    (s : Spec (CommRingCat.of K) ⟶ C) (hs : s ≫ c = 𝟙 _)
    {b : B ⟶ Spec (CommRingCat.of K)} [IsProper b] [GeometricallyIntegral b]
    (G : RelativeGroupLaw K b) (q : SchemeHomOver c b)
    {r : ℕ} {y : Y ⟶ Spec (CommRingCat.of K)} {D : RelEffCartierDiv c r y}
    (hU : D.IsUniversal) {T : Scheme.{u}} (g : T ⟶ Spec (CommRingCat.of K))
    (a a' : Fin r → SchemeHomOver g c)
    (h : SameDivisor c (fun i => (a i).1) (fun i => (a i).2)
      (fun i => (a' i).1) (fun i => (a' i).2)) :
    G.sumList g (List.ofFn fun i => NeronModelInfra.schemeHomOverComp (a i) q) =
      G.sumList g (List.ofFn fun i => NeronModelInfra.schemeHomOverComp (a' i) q) := by
  obtain ⟨σ, -, sum, -, -, -, -, hfac, hkernel⟩ :=
    exists_finiteSumMap_desc c s hs G q hU
  let v : T ⟶ finFibrePow c r :=
    WidePullback.lift g (fun i => (a i).1) (fun i => (a i).2)
  let w : T ⟶ finFibrePow c r :=
    WidePullback.lift g (fun i => (a' i).1) (fun i => (a' i).2)
  have hσvw : v ≫ σ = w ≫ σ := by
    apply (hkernel g v w (WidePullback.lift_base _ _ _ _)
      (WidePullback.lift_base _ _ _ _)).mpr
    simpa only [v, w, WidePullback.lift_π] using h
  rw [← G.finiteSumMap_evaluate c q g a, ← G.finiteSumMap_evaluate c q g a']
  apply Subtype.ext
  change v ≫ (G.finiteSumMap c q r).1 = w ≫ (G.finiteSumMap c q r).1
  rw [← hfac, ← Category.assoc, ← Category.assoc, hσvw]