Scheme_TwoAffineOpenCover_HomOver_exists_isFrameOn_pullback_of_map_eq_smul.lean

theorem pullbackLocalSection_openImmersion (j : X ⟶ Y) [IsOpenImmersion j] (L : Y.Modules) (U :
  Y.Opens)
    (s : Γ(L, U)) :
    Scheme.Modules.pullbackLocalSection j s =
      ((Scheme.Modules.restrictFunctorIsoPullback j).hom.app L).app (j ⁻¹ᵁ U)
        (((Scheme.Modules.restrictAdjunction j).unit.app L).app U s)

theorem pullbackComp_hom_app_app_pullbackLocalSection (f : X ⟶ Y) (g : Y ⟶ Z) (L : Z.Modules) (U :
  Z.Opens)
    (s : Γ(L, U)) :
    ((Scheme.Modules.pullbackComp f g).hom.app L).app (f ⁻¹ᵁ (g ⁻¹ᵁ U))
        (Scheme.Modules.pullbackLocalSection f (Scheme.Modules.pullbackLocalSection g s)) =
      Scheme.Modules.pullbackLocalSection (f ≫ g) s

theorem isFrameOn_of_map {M : X.Modules} {U U' W : X.Opens} (h : U' ≤ U) (hW : W ≤ U') {t : Γ(M, U)}
    (ht : Scheme.Modules.IsFrameOn (M.presheaf.map (homOfLE h).op t) W) : Scheme.Modules.IsFrameOn
      t W

theorem bijective_smul_congr {M : Y.Modules} {U₀ W₁ W₂ : Y.Opens} (h : W₁ = W₂) (h₁ : W₁ ≤ U₀) (h₂
  : W₂ ≤ U₀)
    (r : Γ(M, U₀)) (hb : Function.Bijective fun g : Γ(Y, W₁) => g • M.presheaf.map (homOfLE h₁).op
      r) :
    Function.Bijective fun g : Γ(Y, W₂) => g • M.presheaf.map (homOfLE h₂).op r := by
  subst h; exact hb

theorem isFrameOn_pullbackLocalSection_congr {f f' : X ⟶ Y} (h : f = f') {L : Y.Modules} {U V :
  Y.Opens}
    (s : Γ(L, U)) (hs : Scheme.Modules.IsFrameOn (Scheme.Modules.pullbackLocalSection f s) (f ⁻¹ᵁ
      V)) :
    Scheme.Modules.IsFrameOn (Scheme.Modules.pullbackLocalSection f' s) (f' ⁻¹ᵁ V)

theorem restrict_map_unit {U : Y.Opens} {W : X.Opens} (hW : W ≤ j ⁻¹ᵁ U) (s : Γ(L, U)) :
    (L.restrict j).presheaf.map (homOfLE hW).op
      (show Γ(L.restrict j, j ⁻¹ᵁ U) from ((Scheme.Modules.restrictAdjunction j).unit.app L).app U
        s) =
      (show Γ(L.restrict j, W) from
        L.presheaf.map (homOfLE ((j.image_mono hW).trans (j.image_preimage_le U))).op s) := by
  rw [Scheme.Modules.restrictAdjunction_unit_app_app]
  change (L.presheaf.map _ ≫ L.presheaf.map _) s = _
  rw [← Functor.map_comp]
  rfl

theorem isFrameOn_restrict_unit {U V : Y.Opens} {s : Γ(L, U)} (hs : Scheme.Modules.IsFrameOn s V) :
    Scheme.Modules.IsFrameOn
      (show Γ(L.restrict j, j ⁻¹ᵁ U) from ((Scheme.Modules.restrictAdjunction j).unit.app L).app U
        s) (j ⁻¹ᵁ V) := by
  intro W hWU hWV
  rw [restrict_map_unit j L hWU s]
  have hb := hs ((j.image_mono hWU).trans (j.image_preimage_le U))
    ((j.image_mono hWV).trans (j.image_preimage_le V))
  have : (fun g : Γ(X, W) => g • (show Γ(L.restrict j, W) from
      L.presheaf.map (homOfLE ((j.image_mono hWU).trans (j.image_preimage_le U))).op s)) =
      (fun g' : Γ(Y, j ''ᵁ W) => g' • L.presheaf.map
        (homOfLE ((j.image_mono hWU).trans (j.image_preimage_le U))).op s) ∘
        (fun g => (j.appIso W).inv.hom g) := rfl
  rw [this]
  exact hb.comp (ConcreteCategory.bijective_of_isIso (j.appIso W).inv)

theorem image_preimage_eq_of_le {W : X.Opens} {W' : Y.Opens} (h : W' ≤ j ''ᵁ W) : j ''ᵁ (j ⁻¹ᵁ W')
  = W'

theorem isFrameOn_of_restrict_unit {U₀ : Y.Opens} (r : Γ(M, U₀)) {W : X.Opens}
    (h : Scheme.Modules.IsFrameOn
      (show Γ(M.restrict j, j ⁻¹ᵁ U₀) from ((Scheme.Modules.restrictAdjunction j).unit.app M).app
        U₀ r) W) :
    Scheme.Modules.IsFrameOn r (j ''ᵁ W) := by
  intro W' hW'U hW'W
  have hW''U : j ⁻¹ᵁ W' ≤ j ⁻¹ᵁ U₀ := fun _ hx => hW'U hx
  have hW''W : j ⁻¹ᵁ W' ≤ W := by
    intro x hx
    have : x ∈ j ⁻¹ᵁ (j ''ᵁ W) := hW'W hx
    rwa [j.preimage_image_eq] at this
  have hb := h hW''U hW''W
  rw [restrict_map_unit j M hW''U r] at hb
  have e : (fun g : Γ(X, j ⁻¹ᵁ W') => g • (show Γ(M.restrict j, j ⁻¹ᵁ W') from
      M.presheaf.map (homOfLE ((j.image_mono hW''U).trans (j.image_preimage_le U₀))).op r)) =
      (fun g' : Γ(Y, j ''ᵁ (j ⁻¹ᵁ W')) => g' • M.presheaf.map
        (homOfLE ((j.image_mono hW''U).trans (j.image_preimage_le U₀))).op r) ∘
        (fun g => (j.appIso (j ⁻¹ᵁ W')).inv.hom g) := rfl
  rw [e] at hb
  have hb' : Function.Bijective (fun g' : Γ(Y, j ''ᵁ (j ⁻¹ᵁ W')) => g' • M.presheaf.map
      (homOfLE ((j.image_mono hW''U).trans (j.image_preimage_le U₀))).op r) := by
    exact (Function.Bijective.of_comp_iff
      (fun g' : Γ(Y, j ''ᵁ (j ⁻¹ᵁ W')) => g' • M.presheaf.map
        (homOfLE ((j.image_mono hW''U).trans (j.image_preimage_le U₀))).op r)
      (ConcreteCategory.bijective_of_isIso (j.appIso (j ⁻¹ᵁ W')).inv)).mp hb
  exact bijective_smul_congr (image_preimage_eq_of_le j (W := W) hW'W) _ hW'U r hb'

theorem iso_inv_hom_app_apply {M N : X.Modules} (e : M ≅ N) (U : X.Opens) (x : Γ(M, U)) :
    e.inv.app U (e.hom.app U x) = x

theorem isFrameOn_of_map_iso {M N : X.Modules} (e : M ≅ N) {U V : X.Opens} {s : Γ(M, U)}
    (h : Scheme.Modules.IsFrameOn (e.hom.app U s) V) : Scheme.Modules.IsFrameOn s V

theorem isFrameOn_pullbackLocalSection_congr' {f f' : X ⟶ Y} (h : f = f') {L : Y.Modules} {U :
  Y.Opens}
    {W : X.Opens} (s : Γ(L, U)) (hs : Scheme.Modules.IsFrameOn (Scheme.Modules.pullbackLocalSection
      f s) W) :
    Scheme.Modules.IsFrameOn (Scheme.Modules.pullbackLocalSection f' s) W

theorem exists_iso_of_isFrameOn_self (hs : Scheme.Modules.IsFrameOn s U) :
    ∃ e : (𝟙_ (U : Scheme.{u}).Modules) ≅ (Scheme.Modules.pullback U.ι).obj L,
      e.hom.app ⊤ (Scheme.Modules.unitSection ⊤) =
        ((Scheme.Modules.pullback U.ι).obj L).presheaf.map
          (homOfLE (show (⊤ : (U : Scheme.{u}).Opens) ≤ U.ι ⁻¹ᵁ U
            by rw [Scheme.Opens.ι_preimage_self])).op
          (Scheme.Modules.pullbackLocalSection U.ι s) := by
  have ht : Scheme.Modules.IsFrameOn (Scheme.Modules.pullbackLocalSection U.ι s) (U.ι ⁻¹ᵁ U) := by
    rw [pullbackLocalSection_openImmersion]
    exact (isFrameOn_restrict_unit U.ι L hs).map_iso ((Scheme.Modules.restrictFunctorIsoPullback
      U.ι).app L)
  have hle : ∀ W : (U : Scheme.{u}).Opens, W ≤ U.ι ⁻¹ᵁ U := fun W => by
    rw [Scheme.Opens.ι_preimage_self]; exact le_top
  let fam : ((Scheme.Modules.pullback U.ι).obj L).sections :=
    PresheafOfModules.sectionsMk
      (fun W => ((Scheme.Modules.pullback U.ι).obj L).presheaf.map (homOfLE (hle W.unop)).op
        (Scheme.Modules.pullbackLocalSection U.ι s))
      (fun W W' i => by
        change (((Scheme.Modules.pullback U.ι).obj L).presheaf.map _ ≫
          ((Scheme.Modules.pullback U.ι).obj L).presheaf.map i) _ = _
        rw [← Functor.map_comp]
        rfl)
  obtain ⟨μ, hμdef⟩ : ∃ μ : (𝟙_ (U : Scheme.{u}).Modules) ⟶ (Scheme.Modules.pullback U.ι).obj L,
      μ = (((Scheme.Modules.pullback U.ι).obj L).unitHomEquiv).symm fam := ⟨_, rfl⟩
  have hμ : ∀ W : (U : Scheme.{u}).Opens, μ.app W (Scheme.Modules.unitSection W) =
      ((Scheme.Modules.pullback U.ι).obj L).presheaf.map (homOfLE (hle W)).op
        (Scheme.Modules.pullbackLocalSection U.ι s) := by
    intro W
    have h1 := SheafOfModules.unitHomEquiv_apply_coe _ μ (op W)
    rw [hμdef] at h1
    erw [Equiv.apply_symm_apply] at h1
    rw [hμdef]
    exact h1.symm
  have : IsIso μ := Scheme.Modules.isIso_of_isFrameOn_of_iSup_eq_top μ (fun _ : Unit => ⊤)
    (iSup_const)
    (fun _ => Scheme.Modules.unitSection ⊤)
    (fun _ => ((Scheme.Modules.pullback U.ι).obj L).presheaf.map (homOfLE (hle ⊤)).op
      (Scheme.Modules.pullbackLocalSection U.ι s))
    (fun _ => Scheme.Modules.isFrameOn_unitSection _)
    (fun _ => by
      have := ht.map (homOfLE (hle ⊤))
      intro W hW _
      exact this hW (hle W))
    (fun _ => hμ ⊤)
  exact ⟨asIso μ, hμ ⊤⟩

theorem isFrameOn_pullbackLocalSection_self (φ : X ⟶ Y) {L : Y.Modules} (U : Y.Opens) (s : Γ(L, U))
    (hs : Scheme.Modules.IsFrameOn s U) :
    Scheme.Modules.IsFrameOn (Scheme.Modules.pullbackLocalSection φ s) (φ ⁻¹ᵁ U)

theorem _root_.AlgebraicGeometry.Scheme.Modules.IsFrameOn.pullbackLocalSection' {X Y :
  Scheme.{u}} (φ : X ⟶ Y)
    {L : Y.Modules} {U V : Y.Opens} {s : Γ(L, U)} (hs : Scheme.Modules.IsFrameOn s V) :
    Scheme.Modules.IsFrameOn (Scheme.Modules.pullbackLocalSection φ s) (φ ⁻¹ᵁ V)

theorem mres_res {U V W : X.Opens} (h₁ : V ≤ U) (h₂ : W ≤ V) (s : Γ(M, U)) :
    M.presheaf.map (homOfLE h₂).op (M.presheaf.map (homOfLE h₁).op s) = M.presheaf.map (homOfLE
      (h₂.trans h₁)).op s

theorem res_congr {U W : X.Opens} (h h' : W ≤ U) (s : Γ(M, U)) :
    M.presheaf.map (homOfLE h).op s = M.presheaf.map (homOfLE h').op s

theorem Scheme.TwoAffineOpenCover.HomOver.exists_isFrameOn_pullback_of_map_eq_smul
    {R : Type u} [CommRing R] {S : Type u} [CommRing S] {τ : R →+* S}
    {X : Scheme.{u}} {𝒱 : X.TwoAffineOpenCover} {c : X ⟶ Spec (.of R)}
    {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover} {c' : Y ⟶ Spec (.of S)}
    (f : HomOver τ 𝒱 c 𝒲 c') (M : X.Modules)
    (s₀ : Γ(M, 𝒱.U0)) (s₁ : Γ(M, 𝒱.U1))
    (hs₀ : Scheme.Modules.IsFrameOn s₀ 𝒱.U0) (hs₁ : Scheme.Modules.IsFrameOn s₁ 𝒱.U1)
    (t : Γ(X, 𝒱.U0 ⊓ 𝒱.U1))
    (ht : M.presheaf.map (homOfLE inf_le_right).op s₁ = t • M.presheaf.map (homOfLE inf_le_left).op
      s₀) :
    ∃ (s₀' : Γ((Scheme.Modules.pullback f.hom).obj M, 𝒲.U0))
      (s₁' : Γ((Scheme.Modules.pullback f.hom).obj M, 𝒲.U1)),
      Scheme.Modules.IsFrameOn s₀' 𝒲.U0 ∧ Scheme.Modules.IsFrameOn s₁' 𝒲.U1 ∧
      ((Scheme.Modules.pullback f.hom).obj M).presheaf.map (homOfLE inf_le_right).op s₁' =
        (show Γ(Y, 𝒲.U0 ⊓ 𝒲.U1) from f.map01 t) •
        ((Scheme.Modules.pullback f.hom).obj M).presheaf.map (homOfLE inf_le_left).op s₀' := by
  refine ⟨((Scheme.Modules.pullback f.hom).obj M).presheaf.map
      (homOfLE f.U0_le).op (Scheme.Modules.pullbackLocalSection f.hom s₀),
    ((Scheme.Modules.pullback f.hom).obj M).presheaf.map
      (homOfLE f.U1_le).op (Scheme.Modules.pullbackLocalSection f.hom s₁), ?_, ?_, ?_⟩
  · exact ((hs₀.pullbackLocalSection' f.hom).map _).mono f.U0_le
  · exact ((hs₁.pullbackLocalSection' f.hom).map _).mono f.U1_le
  · rw [mres_res, mres_res]
    have e1 : ((Scheme.Modules.pullback f.hom).obj M).presheaf.map
        (homOfLE ((inf_le_right : 𝒲.U0 ⊓ 𝒲.U1 ≤ _).trans f.U1_le)).op
          (Scheme.Modules.pullbackLocalSection f.hom s₁) =
      ((Scheme.Modules.pullback f.hom).obj M).presheaf.map (homOfLE f.inf_le).op
        (((Scheme.Modules.pullback f.hom).obj M).presheaf.map
          (homOfLE (show f.hom ⁻¹ᵁ (𝒱.U0 ⊓ 𝒱.U1) ≤ f.hom ⁻¹ᵁ 𝒱.U1 from fun _ hx =>
              (inf_le_right : 𝒱.U0 ⊓ 𝒱.U1 ≤ 𝒱.U1) hx)).op
          (Scheme.Modules.pullbackLocalSection f.hom s₁)) := by
      rw [mres_res]
    have e0 : ((Scheme.Modules.pullback f.hom).obj M).presheaf.map
        (homOfLE ((inf_le_left : 𝒲.U0 ⊓ 𝒲.U1 ≤ _).trans f.U0_le)).op
          (Scheme.Modules.pullbackLocalSection f.hom s₀) =
      ((Scheme.Modules.pullback f.hom).obj M).presheaf.map (homOfLE f.inf_le).op
        (((Scheme.Modules.pullback f.hom).obj M).presheaf.map
          (homOfLE (show f.hom ⁻¹ᵁ (𝒱.U0 ⊓ 𝒱.U1) ≤ f.hom ⁻¹ᵁ 𝒱.U0 from fun _ hx =>
              (inf_le_left : 𝒱.U0 ⊓ 𝒱.U1 ≤ 𝒱.U0) hx)).op
          (Scheme.Modules.pullbackLocalSection f.hom s₀)) := by
      rw [mres_res]
    rw [e1, e0,
      Scheme.Modules.map_homOfLE_pullbackLocalSection f.hom (inf_le_right : 𝒱.U0 ⊓ 𝒱.U1 ≤ 𝒱.U1),
      Scheme.Modules.map_homOfLE_pullbackLocalSection f.hom (inf_le_left : 𝒱.U0 ⊓ 𝒱.U1 ≤ 𝒱.U0),
      ht, Scheme.Modules.pullbackLocalSection_smul, Scheme.Modules.map_smul]
    rfl