AffineSectionLocalizationFinite.lean

def actualSpecSectionModule {R : CommRingCat.{u}}
    (M : (Spec R).Modules) (U : (Spec R).Opens) : ModuleCat.{u} R

instance actualSpecSectionModule_sectionAction {R : CommRingCat.{u}}
    (M : (Spec R).Modules) (U : (Spec R).Opens) :
    Module Γ(Spec R, U) (actualSpecSectionModule M U)

instance actualSpecSectionModule_tower {R : CommRingCat.{u}}
    (M : (Spec R).Modules) (U : (Spec R).Opens) :
    IsScalarTower R Γ(Spec R, U) (actualSpecSectionModule M U)

theorem finite_actualSpecSectionModule {R : CommRingCat.{u}}
    (M : (Spec R).Modules) (U : (Spec R).Opens)
    (h : Module.Finite ((Spec R).ringCatSheaf.obj.obj (op U)) (M.val.obj (op U))) :
    Module.Finite Γ(Spec R, U) (actualSpecSectionModule M U)

theorem moduleFinite_localizedModule_of_finite_basicOpen
    {R : CommRingCat.{u}} (M : (Spec R).Modules) [M.IsQuasicoherent]
    (r : R) :
    let U : (Spec R).Opens := PrimeSpectrum.basicOpen r
    Module.Finite ((Spec R).ringCatSheaf.obj.obj (op U)) (M.val.obj (op U)) →
      Module.Finite (Localization.Away r)
        (LocalizedModule.Away r ((moduleSpecΓFunctor (R := R)).obj M)) := by
  intro U hFinite
  let S : Submonoid R := Submonoid.powers r
  let A : CommRingCat.{u} := Γ(Spec R, U)
  let B : ModuleCat.{u} R := actualSpecSectionModule M U
  let : Algebra R A := inferInstanceAs (Algebra R Γ(Spec R, U))
  let : Module A B := actualSpecSectionModule_sectionAction M U
  have : IsScalarTower R A B := actualSpecSectionModule_tower M U
  have : IsLocalization.Away r A :=
    inferInstanceAs (IsLocalization.Away r Γ(Spec R, PrimeSpectrum.basicOpen r))
  let C : ModuleCat.{u} R := (moduleSpecΓFunctor (R := R)).obj M
  let L : Type u := Localization.Away r
  let a : L ≃ₐ[R] A := IsLocalization.algEquiv S L A
  let : Module L B := Module.compHom B a.toRingHom
  have : IsScalarTower R L B := IsScalarTower.of_algebraMap_smul fun c x => by
    change a (algebraMap R L c) • x = c • x
    rw [a.commutes]
    exact IsScalarTower.algebraMap_smul A c x
  let idSemilinear : B →ₛₗ[a.symm.toRingHom] B :=
    { toFun := fun x => x
      map_add' := fun _ _ => rfl
      map_smul' := by
        intro c x
        change c • x = a (a.symm c) • x
        rw [a.apply_symm_apply] }
  have : Module.Finite A B := finite_actualSpecSectionModule M U hFinite
  have : Module.Finite L B :=
    Module.Finite.of_surjective idSemilinear (fun x => ⟨x, rfl⟩)
  let f : C →ₗ[R] B :=
    ((modulesSpecToSheaf.obj M).obj.map U.leTop.op).hom
  have hLocalizing : IsLocalizing (modulesSpecToSheaf.obj M) :=
    (isIso_fromTildeΓ_iff_isLocalizing M).mp
      (isIso_fromTildeΓ_of_isQuasicoherent (R := R) M)
  have : IsLocalizedModule S f := hLocalizing r
  let e : LocalizedModule S C ≃ₗ[R] B := IsLocalizedModule.iso S f
  let eL : LocalizedModule S C ≃ₗ[L] B := e.extendScalarsOfIsLocalization S L
  exact Module.Finite.equiv eL.symm

theorem fg_localized_top_of_finite_basicOpen
    {R : CommRingCat.{u}} (M : (Spec R).Modules) [M.IsQuasicoherent]
    (r : R) :
    let U : (Spec R).Opens := PrimeSpectrum.basicOpen r
    Module.Finite ((Spec R).ringCatSheaf.obj.obj (op U)) (M.val.obj (op U)) →
      ((⊤ : Submodule R ((moduleSpecΓFunctor (R := R)).obj M)).localized
        (Submonoid.powers r)).FG := by
  intro U hFinite
  have : Module.Finite (Localization.Away r)
      (LocalizedModule.Away r ((moduleSpecΓFunctor (R := R)).obj M)) :=
    moduleFinite_localizedModule_of_finite_basicOpen M r hFinite
  rw [Submodule.localized, Submodule.localized'_top]
  exact Module.Finite.fg_top