Scheme_Modules_IsInvertible_nonempty_iso_unit_of_pullback_squareZero.lean

theorem proj_of_ringEquiv {R S : Type u} [CommRing R] [CommRing S] (e : R ≃+* S)
    (M : Type u) [AddCommGroup M] [Module S M] [Module.Projective S M] :
    letI : Module R M := Module.compHom M e.toRingHom
    Module.Projective R M := by
  let : Module R M := Module.compHom M e.toRingHom
  have : RingHomInvPair (e.symm : S →+* R) (e : R →+* S) := RingHomInvPair.of_ringEquiv e.symm
  have : RingHomInvPair (e : R →+* S) (e.symm : S →+* R) := RingHomInvPair.of_ringEquiv e
  have slEq : M ≃ₛₗ[(e.symm : S →+* R)] M :=
    { toFun := id, invFun := id, left_inv := fun _ => rfl, right_inv := fun _ => rfl,
      map_add' := fun _ _ => rfl,
      map_smul' := fun s m => by
        simp only [id]
        change s • m = (e (e.symm s)) • m
        rw [e.apply_symm_apply] }
  exact Module.Projective.of_equiv slEq

theorem fin_of_surj {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S)
    (hf : Function.Surjective f) (M : Type u) [AddCommGroup M] [Module S M]
    [Module.Finite S M] :
    letI : Module R M := Module.compHom M f
    Module.Finite R M := by
  let : Module R M := Module.compHom M f
  obtain ⟨s, hs⟩ := ‹Module.Finite S M›.1
  refine ⟨s, ?_⟩
  rw [eq_top_iff]; intro m _
  have hm : m ∈ Submodule.span S (↑s : Set M) := hs ▸ Submodule.mem_top
  refine Submodule.span_induction ?_ ?_ ?_ ?_ hm
  · intro x hx; exact Submodule.subset_span hx
  · exact Submodule.zero_mem _
  · intro x y _ _ hx hy; exact Submodule.add_mem _ hx hy
  · intro a x _ hx
    obtain ⟨r, hr⟩ := hf a
    have heq : a • x = r • x := by
      change a • x = f r • x; rw [hr]
    rw [heq]; exact Submodule.smul_mem _ r hx

theorem
    _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible.nonempty_iso_unit_of_pullback_squareZero
    {B : Type u} [CommRing B] (I : Ideal B) (hI : I ^ 2 = ⊥)
    (L : (Spec (CommRingCat.of B)).Modules) (hL : Scheme.Modules.IsInvertible L)
    (h : Nonempty ((Scheme.Modules.pullback
            (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))).obj L
          ≅ SheafOfModules.unit (Spec (CommRingCat.of (B ⧸ I))).ringCatSheaf)) :
    Nonempty (L ≅ SheafOfModules.unit (Spec (CommRingCat.of B)).ringCatSheaf)