AffineSubmoduleLocalization.lean

theorem affineSubmoduleMap_toOpen
    (K : Submodule R ((moduleSpecΓFunctor (R := R)).obj F)) (U : (Spec R).Opens) :
    tilde.toOpen (ModuleCat.of R K) U ≫
        (modulesSpecToSheaf.map (affineSubmoduleMap F K)).hom.app (op U) =
      affineSubmoduleInclusion F K ≫ (modulesSpecToSheaf.obj F).obj.map U.leTop.op

theorem affineSubmoduleMap_basicOpen_range [F.IsQuasicoherent]
    (K : Submodule R ((moduleSpecΓFunctor (R := R)).obj F)) (r : R) :
    let P : (Spec R).Opensᵒᵖ ⥤ ModuleCat.{u} R := (modulesSpecToSheaf.obj F).obj
    let U : (Spec R).Opens := PrimeSpectrum.basicOpen (R := R) r
    let b : ((moduleSpecΓFunctor (R := R)).obj F) →ₗ[R] P.obj (op U) :=
      (P.map U.leTop.op).hom
    let : IsLocalizedModule (Submonoid.powers r) b :=
      ((isIso_fromTildeΓ_iff_isLocalizing F).mp inferInstance) r
    ((modulesSpecToSheaf.map (affineSubmoduleMap F K)).hom.app (op U)).hom.range =
      K.localized₀ (Submonoid.powers r) b := by
  intro P U b hb
  let A : ModuleCat.{u} R := ModuleCat.of R K
  let A' : ModuleCat.{u} R := (modulesSpecToSheaf.obj (tilde A)).obj.obj (op U)
  let a : A →ₗ[R] A' := (tilde.toOpen A U).hom
  let c : A' →ₗ[R] P.obj (op U) :=
    ((modulesSpecToSheaf.map (affineSubmoduleMap F K)).hom.app (op U)).hom
  have : IsLocalizedModule (Submonoid.powers r) a := by
    let Q : (Spec R).Opensᵒᵖ ⥤ ModuleCat.{u} R := (modulesSpecToSheaf.obj (tilde A)).obj
    let a₀ : Q.obj (op ⊤) →ₗ[R] A' := (Q.map U.leTop.op).hom
    let e : A ≅ Q.obj (op ⊤) := tilde.isoTop A
    have ha₀ : IsLocalizedModule (Submonoid.powers r) a₀ := isLocalizing_tilde A r
    have he : a₀.comp e.hom.hom = a :=
      congrArg ModuleCat.Hom.hom (tilde.toOpen_res A ⊤ U U.leTop)
    have hComp : IsLocalizedModule (Submonoid.powers r) (a₀.comp e.hom.hom) :=
      (IsLocalizedModule.comp_iff_of_bijective_right (Submonoid.powers r)
        e.hom.hom (ConcreteCategory.bijective_of_isIso e.hom)).mpr ha₀
    exact Eq.mp (congrArg (fun l : A →ₗ[R] A' =>
      IsLocalizedModule (Submonoid.powers r) l) he) hComp
  let i : A →ₗ[R] (moduleSpecΓFunctor (R := R)).obj F :=
    (affineSubmoduleInclusion F K).hom
  have hc : c = IsLocalizedModule.map (Submonoid.powers r) a b i := by
    apply IsLocalizedModule.linearMap_ext (Submonoid.powers r) a b
    exact (congrArg ModuleCat.Hom.hom (affineSubmoduleMap_toOpen F K U)).trans
      (IsLocalizedModule.map_comp (Submonoid.powers r) a b i).symm
  change c.range = K.localized₀ (Submonoid.powers r) b
  exact (congrArg LinearMap.range hc).trans
    ((LinearMap.range_localizedMap_eq_localized₀_range
      (Submonoid.powers r) a b i).trans
        (congrArg (fun L => L.localized₀ (Submonoid.powers r) b) K.range_subtype))