fibrewiseAlgEquivZero_of_isAlgEquivZero_pullback_closedFibre_of_pullbackAlong_iso_tensorPow_poincare.lean

theorem isAlgEquivZero_fibre_of_isPullback {B B' X X' : Scheme.{u}} (x : X ⟶ B) (t : B' ⟶ B)
    (x' : X' ⟶ B') (g : X' ⟶ X)
    (H : IsPullback g x' x t) {k : Type u} [Field k] (s : Spec (CommRingCat.of k) ⟶ B') (N :
      X.Modules)
    (h : IsAlgEquivZero (pullback.snd x' s) ((Scheme.Modules.pullback (pullback.fst x' s)).obj
      ((Scheme.Modules.pullback g).obj N))) :
    IsAlgEquivZero (pullback.snd x (s ≫ t)) ((Scheme.Modules.pullback (pullback.fst x (s ≫ t))).obj
      N)

theorem ker_eq_bot_or_eq_maximalIdeal {O : Type*} [CommRing O] [IsDomain O]
    [IsDiscreteValuationRing O]
    {k : Type*} [Field k] (σ : O →+* k) : RingHom.ker σ = ⊥ ∨ RingHom.ker σ =
      IsLocalRing.maximalIdeal O

theorem exists_comp_eq_of_ker_le {O k k' : Type*} [CommRing O] [CommRing k] [CommRing k']
    (π : O →+* k) (hπ : Function.Surjective π)
    (σ : O →+* k') (h : RingHom.ker π ≤ RingHom.ker σ) : ∃ τ : k →+* k', τ.comp π = σ

theorem isAlgEquivZero_snd_comp_of_fibreAt {R : Type u} [CommRing R] {C T : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of R))
    (t : T ⟶ Spec (CommRingCat.of R)) {k : Type u} [Field k] (s : Spec (CommRingCat.of k) ⟶ T) (L :
      (pullback c t).Modules)
    (h : IsAlgEquivZero (fibreAt c t s) ((Scheme.Modules.pullback (pullback.fst (pullback.snd c t)
      s)).obj L)) :
    IsAlgEquivZero (pullback.snd c (s ≫ t)) ((Scheme.Modules.pullback (mapOnProdOver c s (rfl : s ≫
      t = s ≫ t))).obj L)

theorem isAlgEquivZero_fibre_of_factor
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
    {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
    (ψ : SchemeHomOver t' t) (M : RigidifiedLineBundle c ε t)
    (N' : (pullback c t').Modules)
    (hN' : ∀ (k : Type u) [Field k] [IsAlgClosed k] (s' : Spec (CommRingCat.of k) ⟶ T'),
      IsAlgEquivZero (fibreAt c t' s') ((Scheme.Modules.pullback (pullback.fst (pullback.snd c t')
        s')).obj N'))
    (e : (M.pullbackAlong ψ).L ≅ N')
    (k : Type u) [Field k] [IsAlgClosed k] (s' : Spec (CommRingCat.of k) ⟶ T')
    (s : Spec (CommRingCat.of k) ⟶ T) (hs : s = s' ≫ ψ.1) :
    IsAlgEquivZero (fibreAt c t s) ((Scheme.Modules.pullback (pullback.fst (pullback.snd c t)
      s)).obj M.L)

theorem
fibrewiseAlgEquivZero_of_isAlgEquivZero_pullback_closedFibre_of_pullbackAlong_iso_tensorPow_poincare
    {A : Type u} [CommRing A] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of A))
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of A))) c)
    (D : RelativePic0Designation A c) (hrep : Nonempty (RepresentsRelSubPic c ε (algEquivZeroCut c
      ε) D))
    (k : Type u) [Field k] [Algebra A k]
    (O : Type u) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O] (ρO : A →+* O)
    (toκ : O →+* k) (htoκ : toκ.comp ρO = algebraMap A k) (htoκs : Function.Surjective toκ)
    (bc : pullback c (specMap A k) ⟶ pullback c (Spec.map (CommRingCat.ofHom ρO)))
    (hbc₁ : bc ≫ pullback.fst _ _ = pullback.fst _ _)
    (hbc₂ : bc ≫ pullback.snd _ _ = pullback.snd _ _ ≫ Spec.map (CommRingCat.ofHom toκ))
    (T' : Type u) [Field T'] [Algebra O T'] [IsFractionRing O T']
    (y : SchemeHomOver (Spec.map (CommRingCat.ofHom ((algebraMap O T').comp ρO))) D.toBase) (n : ℕ)
    (M : RigidifiedLineBundle c ε (Spec.map (CommRingCat.ofHom ρO)))
    (hclosed : IsAlgEquivZero (pullback.snd c (specMap A k)) ((Scheme.Modules.pullback bc).obj M.L))
    (hgen : Nonempty ((M.pullbackAlong
        (⟨Spec.map (CommRingCat.ofHom (algebraMap O T')),
          by rw [← Spec.map_comp, ← CommRingCat.ofHom_comp]⟩ :
          SchemeHomOver (Spec.map (CommRingCat.ofHom ((algebraMap O T').comp ρO))) (Spec.map
            (CommRingCat.ofHom ρO)))).L ≅
      (hrep.some.poincare.pullbackAlong y).L.tensorPow n)) :
    FibrewiseAlgEquivZero M := by
  classical
  intro k' _ _ s
  let tO : Spec (CommRingCat.of O) ⟶ Spec (CommRingCat.of A) := Spec.map (CommRingCat.ofHom ρO)
  let gT : SchemeHomOver (Spec.map (CommRingCat.ofHom ((algebraMap O T').comp ρO))) tO :=
    ⟨Spec.map (CommRingCat.ofHom (algebraMap O T')),
      by rw [← Spec.map_comp, ← CommRingCat.ofHom_comp]⟩
  obtain ⟨σ, rfl⟩ : ∃ σ : CommRingCat.of O ⟶ CommRingCat.of k', s = Spec.map σ := ⟨Spec.preimage s,
    (Spec.map_preimage s).symm⟩
  rcases GlueKit.ker_eq_bot_or_eq_maximalIdeal σ.hom with hker | hker
  · have hinj : Function.Injective σ.hom := (RingHom.injective_iff_ker_eq_bot _).mpr hker
    let σ' : T' →+* k' := IsFractionRing.lift hinj
    have hσ : σ = CommRingCat.ofHom (σ'.comp (algebraMap O T')) := by
      ext x
      exact (IsFractionRing.lift_algebraMap hinj x).symm
    have hs : Spec.map σ = Spec.map (CommRingCat.ofHom σ') ≫ gT.1 := by
      rw [hσ, CommRingCat.ofHom_comp, Spec.map_comp]
    have hP : FibrewiseAlgEquivZero hrep.some.poincare := hrep.some.poincare_mem
    have hPy : FibrewiseAlgEquivZero (hrep.some.poincare.pullbackAlong y) := hP.pullback y
    have hN' : ∀ (k₁ : Type u) [Field k₁] [IsAlgClosed k₁] (s' : Spec (CommRingCat.of k₁) ⟶ Spec
      (CommRingCat.of T')),
        IsAlgEquivZero (fibreAt c (Spec.map (CommRingCat.ofHom ((algebraMap O T').comp ρO))) s')
          ((Scheme.Modules.pullback (pullback.fst (pullback.snd c _) s')).obj
            ((hrep.some.poincare.pullbackAlong y).L.tensorPow n)) := by
      intro k₁ _ _ s'
      exact ((hPy k₁ s').tensorPow n).of_iso
        (AlgebraicGeometry.Scheme.Modules.nonempty_pullback_tensorPow_iso _ _ n).some.symm
    exact GenericLeg.isAlgEquivZero_fibre_of_factor c gT M _ hN' hgen.some k' (Spec.map
      (CommRingCat.ofHom σ')) (Spec.map σ) hs
  · have hkert : RingHom.ker toκ = IsLocalRing.maximalIdeal O :=
      IsLocalRing.eq_maximalIdeal (RingHom.ker_isMaximal_of_surjective toκ htoκs)
    obtain ⟨τ, hτ⟩ := GlueKit.exists_comp_eq_of_ker_le toκ htoκs σ.hom (by rw [hkert, hker])
    have hs : Spec.map σ = Spec.map (CommRingCat.ofHom τ) ≫ Spec.map (CommRingCat.ofHom toκ) := by
      rw [← Spec.map_comp, ← CommRingCat.ofHom_comp, hτ]; rfl
    have hspec : Spec.map (CommRingCat.ofHom toκ) ≫ tO = specMap A k := by
      change Spec.map _ ≫ Spec.map _ = Spec.map _
      rw [← Spec.map_comp, ← CommRingCat.ofHom_comp, htoκ]
    have H : IsPullback bc (pullback.snd c (specMap A k)) (pullback.snd c tO) (Spec.map
      (CommRingCat.ofHom toκ)) := by
      refine IsPullback.of_right (h₁₂ := pullback.fst c tO) (v₁₃ := c) (h₂₂ := tO) ?_ hbc₂
        (IsPullback.of_hasPullback c tO)
      rw [hbc₁, hspec]
      exact IsPullback.of_hasPullback c (specMap A k)
    let : Algebra k k' := τ.toAlgebra
    have hbc' := AlgebraicGeometry.RelPicard.IsAlgEquivZero.baseChange k' (pullback.snd c (specMap
      A k)) hclosed
    have key := GlueKit.isAlgEquivZero_fibre_of_isPullback (pullback.snd c tO) (Spec.map
      (CommRingCat.ofHom toκ))
      (pullback.snd c (specMap A k)) bc H (Spec.map (CommRingCat.ofHom (algebraMap k k'))) M.L hbc'
    have : ∀ s'' : Spec (CommRingCat.of k') ⟶ Spec (CommRingCat.of O),
        s'' = Spec.map (CommRingCat.ofHom (algebraMap k k')) ≫ Spec.map (CommRingCat.ofHom toκ) →
        IsAlgEquivZero (fibreAt c tO s'') ((Scheme.Modules.pullback (pullback.fst (pullback.snd c
          tO) s'')).obj M.L) := by
      rintro _ rfl; exact key
    exact this _ hs