Scheme_Modules_IsFrameOn_exists_basis_smul_pushforward.lean

theorem _root_.AlgebraicGeometry.Scheme.Modules.IsFrameOn.exists_basis_smul_pushforward
    {X Y : Scheme.{u}} (π : X ⟶ Y) {L : X.Modules} {V : Y.Opens} {d : ℕ}
    (e : Fin d → Γ((Scheme.Modules.pushforward π).obj (𝟙_ X.Modules), V))
    (he : ∀ (W : Y.Opens) (hW : W ≤ V),
      ∃ b : Module.Basis (Fin d) Γ(Y, W) Γ((Scheme.Modules.pushforward π).obj (𝟙_ X.Modules), W),
        ∀ i, b i = ((Scheme.Modules.pushforward π).obj (𝟙_ X.Modules)).presheaf.map (homOfLE
          hW).op (e i))
    {s : Γ(L, π ⁻¹ᵁ V)} (hs : Scheme.Modules.IsFrameOn s (π ⁻¹ᵁ V)) :
    ∀ (W : Y.Opens) (hW : W ≤ V),
      ∃ b : Module.Basis (Fin d) Γ(Y, W) Γ((Scheme.Modules.pushforward π).obj L, W),
        ∀ i, b i = ((Scheme.Modules.pushforward π).obj L).presheaf.map (homOfLE hW).op
          (show Γ((Scheme.Modules.pushforward π).obj L, V) from (show Γ(X, π ⁻¹ᵁ V) from e i) • s)
            := by
  intro W hW
  obtain ⟨b₀, hb₀⟩ := he W hW
  have hWV : π ⁻¹ᵁ W ≤ π ⁻¹ᵁ V := fun x hx => hW hx
  let sW : Γ(L, π ⁻¹ᵁ W) := L.presheaf.map (homOfLE hWV).op s
  have hbij : Function.Bijective fun g : Γ(X, π ⁻¹ᵁ W) => g • sW := hs hWV hWV
  let ψ : Γ((Scheme.Modules.pushforward π).obj (𝟙_ X.Modules), W) ≃ₗ[Γ(Y, W)]
      Γ((Scheme.Modules.pushforward π).obj L, W) :=
    { toFun := fun g => (show Γ((Scheme.Modules.pushforward π).obj L, W) from (show Γ(X, π ⁻¹ᵁ W)
      from g) • sW)
      map_add' := fun g g' => by
        change ((show Γ(X, π ⁻¹ᵁ W) from g) + (show Γ(X, π ⁻¹ᵁ W) from g')) • sW = _
        rw [add_smul]; rfl
      map_smul' := fun r g => by
        change ((π.app W).hom r * (show Γ(X, π ⁻¹ᵁ W) from g)) • sW =
          (π.app W).hom r • ((show Γ(X, π ⁻¹ᵁ W) from g) • sW)
        rw [mul_smul]
      invFun := fun m => (Equiv.ofBijective _ hbij).symm (show Γ(L, π ⁻¹ᵁ W) from m)
      left_inv := fun g => (Equiv.ofBijective _ hbij).symm_apply_apply (show Γ(X, π ⁻¹ᵁ W) from g)
      right_inv := fun m => (Equiv.ofBijective _ hbij).apply_symm_apply (show Γ(L, π ⁻¹ᵁ W) from
        m) }
  refine ⟨b₀.map ψ, fun i => ?_⟩
  rw [Module.Basis.map_apply, hb₀ i]
  simp only [Scheme.Modules.pushforward_obj_presheaf_map]
  set j : π ⁻¹ᵁ W ⟶ π ⁻¹ᵁ V := (TopologicalSpace.Opens.map π.base).map (homOfLE hW) with hj
  have hsW : sW = L.presheaf.map j.op s := congrArg (fun k => L.presheaf.map k s)
    (Subsingleton.elim _ _)
  have h1 : (𝟙_ X.Modules).presheaf.map j.op (e i) =
      (show Γ(𝟙_ X.Modules, π ⁻¹ᵁ W) from X.presheaf.map j.op (show Γ(X, π ⁻¹ᵁ V) from e i)) := by
    have h := Scheme.Modules.map_smul (𝟙_ X.Modules) j (show Γ(X, π ⁻¹ᵁ V) from e i)
      (Scheme.Modules.unitSection (π ⁻¹ᵁ V))
    rw [Scheme.Modules.smul_unitSection, Scheme.Modules.map_unitSection,
      Scheme.Modules.smul_unitSection] at h
    exact h
  change (show Γ(X, π ⁻¹ᵁ W) from (𝟙_ X.Modules).presheaf.map j.op (e i)) • sW =
    L.presheaf.map j.op ((show Γ(X, π ⁻¹ᵁ V) from e i) • s)
  rw [h1, Scheme.Modules.map_smul, hsW]