IsClosedImmersion_app_curveChange_injective_and_exists_of_app_eq_of_isReduced.lean

def ExistsClause (U : X.Opens) : Prop

theorem iSup_affineOpens_le (U : X.Opens) :
    ⨆ (V : {V : X.Opens // IsAffineOpen V ∧ V ≤ U}), (V : X.Opens) = U

theorem app_apply_map_op {X' Y' : Scheme.{u}} (f : Y' ⟶ X') {U V : X'.Opens} (ι : V ⟶ U) (s : Γ(X',
  U)) :
    f.app V (X'.presheaf.map ι.op s) = Y'.presheaf.map ((Opens.map f.base).map ι).op (f.app U s)

theorem exists_of_forall_isAffineOpen (U : X.Opens)
    (hinj : ∀ V : X.Opens, V ≤ U → Function.Injective (fun f : Γ(X, V) => ((i₁.app V) f, (i₂.app V)
      f)))
    (hex : ∀ V : X.Opens, IsAffineOpen V → V ≤ U → ExistsClause i₁ i₂ j₁ j₂ hsq V) :
    ExistsClause i₁ i₂ j₁ j₂ hsq U := by
  classical
  intro g₁ g₂ hagree
  let ι : Type u := {V : X.Opens // IsAffineOpen V ∧ V ≤ U}
  let V : ι → X.Opens := fun j => j.1
  let r₁ : ∀ j : ι, Γ(Y₁, i₁ ⁻¹ᵁ V j) := fun j => Y₁.presheaf.map (homOfLE (i₁.preimage_mono
    j.2.2)).op g₁
  let r₂ : ∀ j : ι, Γ(Y₂, i₂ ⁻¹ᵁ V j) := fun j => Y₂.presheaf.map (homOfLE (i₂.preimage_mono
    j.2.2)).op g₂
  have hagreeV : ∀ j : ι,
      Z.presheaf.map
          (eqToHom (show j₂ ⁻¹ᵁ (i₂ ⁻¹ᵁ V j) = j₁ ⁻¹ᵁ (i₁ ⁻¹ᵁ V j) by
            rw [← Scheme.Hom.comp_preimage, ← Scheme.Hom.comp_preimage, hsq])).op
        (j₁.app (i₁ ⁻¹ᵁ V j) (r₁ j)) = j₂.app (i₂ ⁻¹ᵁ V j) (r₂ j) := by
    intro j
    simp only [r₁, r₂]
    rw [app_apply_map_op, app_apply_map_op, ← hagree]
    generalize j₁.app (i₁ ⁻¹ᵁ U) g₁ = t
    simp only [← CategoryTheory.ConcreteCategory.comp_apply, ← Functor.map_comp, ← op_comp]
    rfl
  choose fV hfV₁ hfV₂ using fun j : ι => hex (V j) j.2.1 j.2.2 (r₁ j) (r₂ j) (hagreeV j)
  have hcompat : TopCat.Presheaf.IsCompatible X.sheaf.1 V fV := by
    intro j j'
    apply hinj (V j ⊓ V j') (inf_le_left.trans j.2.2)
    change ((i₁.app _) (X.presheaf.map _ (fV j)), (i₂.app _) (X.presheaf.map _ (fV j))) =
      ((i₁.app _) (X.presheaf.map _ (fV j')), (i₂.app _) (X.presheaf.map _ (fV j')))
    simp only [Prod.mk.injEq]
    refine ⟨?_, ?_⟩
    · rw [app_apply_map_op, app_apply_map_op, hfV₁, hfV₁]
      simp only [r₁, ← CategoryTheory.ConcreteCategory.comp_apply, ← Functor.map_comp, ← op_comp]
      rfl
    · rw [app_apply_map_op, app_apply_map_op, hfV₂, hfV₂]
      simp only [r₂, ← CategoryTheory.ConcreteCategory.comp_apply, ← Functor.map_comp, ← op_comp]
      rfl
  obtain ⟨f, hf, -⟩ : ∃! f : Γ(X, U),
      ∀ j : ι, X.presheaf.map (homOfLE j.2.2).op f = fV j :=
    X.sheaf.existsUnique_gluing' V U (fun j => homOfLE j.2.2)
      (le_of_eq (iSup_affineOpens_le U).symm) fV hcompat
  refine ⟨f, ?_, ?_⟩
  · fapply Y₁.sheaf.eq_of_locally_eq' (fun j : ι => i₁ ⁻¹ᵁ V j) (i₁ ⁻¹ᵁ U)
      (fun j => homOfLE (i₁.preimage_mono j.2.2))
    · rw [← Scheme.Hom.preimage_iSup]
      exact i₁.preimage_mono (le_of_eq (iSup_affineOpens_le U).symm)
    · intro j
      have e1 : (i₁.app (V j)) (X.presheaf.map (homOfLE j.2.2).op f) = r₁ j := by
        have := hf j
        change X.presheaf.map (homOfLE j.2.2).op f = fV j at this
        rw [this, hfV₁]
      change Y₁.presheaf.map (homOfLE (i₁.preimage_mono j.2.2)).op
        (i₁.app U f) = r₁ j
      exact (app_apply_map_op i₁ (homOfLE j.2.2) f).symm.trans e1
  · fapply Y₂.sheaf.eq_of_locally_eq' (fun j : ι => i₂ ⁻¹ᵁ V j) (i₂ ⁻¹ᵁ U)
      (fun j => homOfLE (i₂.preimage_mono j.2.2))
    · rw [← Scheme.Hom.preimage_iSup]
      exact i₂.preimage_mono (le_of_eq (iSup_affineOpens_le U).symm)
    · intro j
      have e2 : (i₂.app (V j)) (X.presheaf.map (homOfLE j.2.2).op f) = r₂ j := by
        have := hf j
        change X.presheaf.map (homOfLE j.2.2).op f = fV j at this
        rw [this, hfV₂]
      change Y₂.presheaf.map (homOfLE (i₂.preimage_mono j.2.2)).op
        (i₂.app U f) = r₂ j
      exact (app_apply_map_op i₂ (homOfLE j.2.2) f).symm.trans e2

theorem ker_pullback_fst_comp [IsClosedImmersion i₁] [IsClosedImmersion i₂] :
    (pullback.fst i₁ i₂ ≫ i₁).ker = i₁.ker ⊔ i₂.ker

theorem exists_of_isAffineOpen [IsClosedImmersion i₁] [IsClosedImmersion i₂] (hZ : IsPullback j₁ j₂
  i₁ i₂)
    (U : X.Opens) (hU : IsAffineOpen U) : ExistsClause i₁ i₂ j₁ j₂ hZ.w U

theorem isPullback_curveChange_fst {R : Type u} [CommRing R] {C C' T : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)} (f : C' ⟶ C) (hf : f ≫ c
      = c')
    (t : T ⟶ Spec (CommRingCat.of R)) :
    IsPullback (curveChange f hf t) (pullback.fst c' t) (pullback.fst c t) f

instance isClosedImmersion_curveChange {R : Type u} [CommRing R] {C C' T : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)} (f : C' ⟶ C) (hf : f ≫ c
      = c')
    (t : T ⟶ Spec (CommRingCat.of R)) [IsClosedImmersion f] : IsClosedImmersion (curveChange f hf
      t)

theorem isPullback_curveChange (hZ : IsPullback j₁.1 j₂.1 i₁.1 i₂.1) :
    IsPullback (curveChange j₁.1 j₁.2 t) (curveChange j₂.1 j₂.2 t) (curveChange i₁.1 i₁.2 t)
      (curveChange i₂.1 i₂.2 t)

lemma map_eq_zero_of_app_eq_zero {P W : Scheme.{u}} (l : W ⟶ P) [IsOpenImmersion l] {V : P.Opens}
  (s : Γ(P, V))
    (hs : l.app V s = 0) :
    P.presheaf.map (homOfLE (show l ''ᵁ l ⁻¹ᵁ V ≤ V by
      rw [Scheme.Hom.image_preimage_eq_opensRange_inf]; exact inf_le_right)).op s = 0 := by
  have h := Scheme.Hom.appLE_appIso_inv l (U := V) (V := l ⁻¹ᵁ V) le_rfl
  have h' := congrArg (fun φ => (ConcreteCategory.hom φ) s) h
  simp only [CategoryTheory.comp_apply] at h'
  rw [← Scheme.Hom.app_eq_appLE] at h'
  rw [hs, map_zero] at h'
  rw [← h']

theorem app_curveChange_injective [IsClosedImmersion i₁.1] [IsClosedImmersion i₂.1] (hXred :
  IsReduced X)
    (hjs : ∀ p : X, p ∈ Set.range i₁.1.base ∨ p ∈ Set.range i₂.1.base) (U : (Limits.pullback x
      t).Opens) :
    Function.Injective (fun f : Γ(Limits.pullback x t, U) =>
      ((curveChange i₁.1 i₁.2 t).app U f, (curveChange i₂.1 i₂.2 t).app U f)) := by
  classical
  have : IsReduced X := hXred
  set f : Y₁ ⨿ Y₂ ⟶ X := coprod.desc i₁.1 i₂.1 with hf
  have : Surjective f := ⟨fun p => by
    rcases hjs p with ⟨y, hy⟩ | ⟨y, hy⟩
    · refine ⟨(coprod.inl : Y₁ ⟶ Y₁ ⨿ Y₂).base y, ?_⟩
      change (coprod.inl ≫ f).base y = p
      rw [hf, coprod.inl_desc]; exact hy
    · refine ⟨(coprod.inr : Y₂ ⟶ Y₁ ⨿ Y₂).base y, ?_⟩
      change (coprod.inr ≫ f).base y = p
      rw [hf, coprod.inr_desc]; exact hy⟩
  have : IsSchemeTheoreticallyDominant f := IsSchemeTheoreticallyDominant.of_isDominant f
  have : QuasiCompact f := by rw [hf]; infer_instance
  set p : Limits.pullback x t ⟶ X := pullback.fst x t with hp
  have : IsSchemeTheoreticallyDominant (pullback.snd f p) :=
    IsSchemeTheoreticallyDominant.pullbackSnd f p
  have hinjP : ∀ V, Function.Injective ((pullback.snd f p).app V) := fun V => (pullback.snd f
    p).app_injective V
  set l₁ : Limits.pullback y₁ t ⟶ Limits.pullback f p :=
    pullback.lift (pullback.fst y₁ t ≫ coprod.inl) (curveChange i₁.1 i₁.2 t)
      (by
        rw [Category.assoc, hf, coprod.inl_desc, hp]
        simp only [curveChange, pullback.lift_fst]) with hl₁
  set l₂ : Limits.pullback y₂ t ⟶ Limits.pullback f p :=
    pullback.lift (pullback.fst y₂ t ≫ coprod.inr) (curveChange i₂.1 i₂.2 t)
      (by
        rw [Category.assoc, hf, coprod.inr_desc, hp]
        simp only [curveChange, pullback.lift_fst]) with hl₂
  have hl₁snd : l₁ ≫ pullback.snd f p = curveChange i₁.1 i₁.2 t := by rw [hl₁, pullback.lift_snd]
  have hl₂snd : l₂ ≫ pullback.snd f p = curveChange i₂.1 i₂.2 t := by rw [hl₂, pullback.lift_snd]
  have hl₁fst : l₁ ≫ pullback.fst f p = pullback.fst y₁ t ≫ coprod.inl :=
    by rw [hl₁, pullback.lift_fst]
  have hl₂fst : l₂ ≫ pullback.fst f p = pullback.fst y₂ t ≫ coprod.inr :=
    by rw [hl₂, pullback.lift_fst]
  have sq₁ : IsPullback l₁ (pullback.fst y₁ t) (pullback.fst f p) coprod.inl := by
    refine IsPullback.of_right ?_ hl₁fst (IsPullback.of_hasPullback f p).flip
    rw [hl₁snd, hf, coprod.inl_desc]
    exact isPullback_curveChange_fst i₁.1 i₁.2 t
  have sq₂ : IsPullback l₂ (pullback.fst y₂ t) (pullback.fst f p) coprod.inr := by
    refine IsPullback.of_right ?_ hl₂fst (IsPullback.of_hasPullback f p).flip
    rw [hl₂snd, hf, coprod.inr_desc]
    exact isPullback_curveChange_fst i₂.1 i₂.2 t
  have : IsOpenImmersion l₁ := MorphismProperty.of_isPullback (P := @IsOpenImmersion) sq₁.flip
    inferInstance
  have : IsOpenImmersion l₂ := MorphismProperty.of_isPullback (P := @IsOpenImmersion) sq₂.flip
    inferInstance
  have hcov : ∀ q : ↥(Limits.pullback f p), q ∈ l₁.opensRange ∨ q ∈ l₂.opensRange := by
    intro q
    have hq : (pullback.fst f p).base q ∈ Set.range (coprod.inl : Y₁ ⟶ Y₁ ⨿ Y₂).base ⊔
        Set.range (coprod.inr : Y₂ ⟶ Y₁ ⨿ Y₂).base := by
      rw [(isCompl_range_inl_inr Y₁ Y₂).sup_eq_top]; trivial
    rcases hq with ⟨y, hy⟩ | ⟨y, hy⟩
    · left
      obtain ⟨w, hw, -⟩ := Scheme.Pullback.exists_preimage_pullback (f := pullback.fst f p) (g :=
        coprod.inl) q y
        hy.symm
      exact Scheme.Hom.mem_opensRange.mpr ⟨sq₁.isoPullback.inv.base w, by
        rw [← Scheme.Hom.comp_apply, sq₁.isoPullback_inv_fst]; exact hw⟩
    · right
      obtain ⟨w, hw, -⟩ := Scheme.Pullback.exists_preimage_pullback (f := pullback.fst f p) (g :=
        coprod.inr) q y
        hy.symm
      exact Scheme.Hom.mem_opensRange.mpr ⟨sq₂.isoPullback.inv.base w, by
        rw [← Scheme.Hom.comp_apply, sq₂.isoPullback_inv_fst]; exact hw⟩
  have hvan : ∀ (V : (Limits.pullback f p).Opens) (s : Γ(Limits.pullback f p, V)),
      l₁.app V s = 0 → l₂.app V s = 0 → s = 0 := by
    intro V s h₁ h₂
    let O : Bool → (Limits.pullback f p).Opens := fun b => bif b then l₁ ''ᵁ l₁ ⁻¹ᵁ V else l₂ ''ᵁ
      l₂ ⁻¹ᵁ V
    have hO : ∀ b, O b ≤ V := by
      intro b
      cases b
      · change l₂ ''ᵁ l₂ ⁻¹ᵁ V ≤ V
        rw [Scheme.Hom.image_preimage_eq_opensRange_inf]; exact inf_le_right
      · change l₁ ''ᵁ l₁ ⁻¹ᵁ V ≤ V
        rw [Scheme.Hom.image_preimage_eq_opensRange_inf]; exact inf_le_right
    have hVO : V ≤ ⨆ b, O b := by
      intro q hq
      rw [Opens.mem_iSup]
      rcases hcov q with h | h
      · refine ⟨true, ?_⟩
        change q ∈ l₁ ''ᵁ l₁ ⁻¹ᵁ V
        rw [Scheme.Hom.image_preimage_eq_opensRange_inf]; exact ⟨h, hq⟩
      · refine ⟨false, ?_⟩
        change q ∈ l₂ ''ᵁ l₂ ⁻¹ᵁ V
        rw [Scheme.Hom.image_preimage_eq_opensRange_inf]; exact ⟨h, hq⟩
    apply (Limits.pullback f p).sheaf.eq_of_locally_eq' O V (fun b => homOfLE (hO b)) hVO
    intro b
    change (Limits.pullback f p).presheaf.map (homOfLE (hO b)).op s =
      (Limits.pullback f p).presheaf.map (homOfLE (hO b)).op 0
    rw [map_zero]
    cases b
    · exact map_eq_zero_of_app_eq_zero l₂ s h₂
    · exact map_eq_zero_of_app_eq_zero l₁ s h₁
  intro u u' huu
  simp only [Prod.mk.injEq] at huu
  obtain ⟨h₁, h₂⟩ := huu
  rw [← sub_eq_zero]
  apply hinjP U
  rw [map_zero]
  apply hvan
  · have e := Scheme.Hom.congr_app hl₁snd U
    rw [Scheme.Hom.comp_app] at e
    have e' := CategoryTheory.ConcreteCategory.congr_hom e (u - u')
    rw [CategoryTheory.ConcreteCategory.comp_apply] at e'
    erw [CategoryTheory.ConcreteCategory.comp_apply] at e'
    rw [e', map_sub, h₁, sub_self, map_zero]
  · have e := Scheme.Hom.congr_app hl₂snd U
    rw [Scheme.Hom.comp_app] at e
    have e' := CategoryTheory.ConcreteCategory.congr_hom e (u - u')
    rw [CategoryTheory.ConcreteCategory.comp_apply] at e'
    erw [CategoryTheory.ConcreteCategory.comp_apply] at e'
    rw [e', map_sub, h₂, sub_self, map_zero]

theorem app_curveChange_injective_and_exists_of_app_eq_of_isReduced
    {k : Type u} [Field k] {X Y₁ Y₂ Z : Scheme.{u}} (x : X ⟶ Spec (CommRingCat.of k)) (hXred :
      IsReduced X)
    (y₁ : Y₁ ⟶ Spec (CommRingCat.of k)) (y₂ : Y₂ ⟶ Spec (CommRingCat.of k)) (z : Z ⟶ Spec
      (CommRingCat.of k))
    (i₁ : SchemeHomOver y₁ x) (i₂ : SchemeHomOver y₂ x) [IsClosedImmersion i₁.1] [IsClosedImmersion
      i₂.1]
    (hjs : ∀ p : X, p ∈ Set.range i₁.1.base ∨ p ∈ Set.range i₂.1.base)
    (j₁ : SchemeHomOver z y₁) (j₂ : SchemeHomOver z y₂) (hZ : IsPullback j₁.1 j₂.1 i₁.1 i₂.1)
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k))
    (hsq : curveChange j₁.1 j₁.2 t ≫ curveChange i₁.1 i₁.2 t = curveChange j₂.1 j₂.2 t ≫
      curveChange i₂.1 i₂.2 t)
    (U : (Limits.pullback x t).Opens) :
    Function.Injective (fun f : Γ(Limits.pullback x t, U) =>
      ((curveChange i₁.1 i₁.2 t).app U f, (curveChange i₂.1 i₂.2 t).app U f)) ∧
      ∀ (g₁ : Γ(Limits.pullback y₁ t, (curveChange i₁.1 i₁.2 t) ⁻¹ᵁ U))
        (g₂ : Γ(Limits.pullback y₂ t, (curveChange i₂.1 i₂.2 t) ⁻¹ᵁ U)),
        (Limits.pullback z t).presheaf.map
            (eqToHom (show (curveChange j₂.1 j₂.2 t) ⁻¹ᵁ ((curveChange i₂.1 i₂.2 t) ⁻¹ᵁ U) =
                (curveChange j₁.1 j₁.2 t) ⁻¹ᵁ ((curveChange i₁.1 i₁.2 t) ⁻¹ᵁ U) by
              rw [← Scheme.Hom.comp_preimage, ← Scheme.Hom.comp_preimage, hsq])).op
          ((curveChange j₁.1 j₁.2 t).app ((curveChange i₁.1 i₁.2 t) ⁻¹ᵁ U) g₁) =
          (curveChange j₂.1 j₂.2 t).app ((curveChange i₂.1 i₂.2 t) ⁻¹ᵁ U) g₂ →
        ∃ f : Γ(Limits.pullback x t, U),
          (curveChange i₁.1 i₁.2 t).app U f = g₁ ∧ (curveChange i₂.1 i₂.2 t).app U f = g₂ :=
  ⟨MilnorBC.app_curveChange_injective x y₁ y₂ i₁ i₂ t hXred hjs U,
    MilnorBC.exists_of_forall_isAffineOpen _ _ _ _ hsq U
      (fun V _ => MilnorBC.app_curveChange_injective x y₁ y₂ i₁ i₂ t hXred hjs V)
      (fun V hV _ => MilnorBC.exists_of_isAffineOpen _ _ _ _ (MilnorBC.isPullback_curveChange x y₁
        y₂ z i₁ i₂ j₁ j₂ t hZ)
        V hV)⟩