FinitePresentation.lean

/-
Copyright (c) 2024 Andrew Yang. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Andrew Yang
-/
module

public import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
public import Mathlib.LinearAlgebra.Isomorphisms
public import Mathlib.LinearAlgebra.TensorProduct.RightExactness
public import Mathlib.RingTheory.Finiteness.Projective
public import Mathlib.RingTheory.Localization.BaseChange
public import Mathlib.RingTheory.Noetherian.Basic
public import Mathlib.RingTheory.TensorProduct.Finite

/-!
# Finitely Presented Modules

## Main definition

- `Module.FinitePresentation`: A module is finitely presented if it is generated by some
  finite set `s` and the kernel of the presentation `Rˢ → M` is also finitely generated.

## Main results

- `Module.finitePresentation_iff_finite`: If `R` is Noetherian, then f.p. iff f.g. on `R`-modules.

Suppose `0 → K → M → N → 0` is an exact sequence of `R`-modules.

- `Module.finitePresentation_of_surjective`: If `M` is f.p., `K` is f.g., then `N` is f.p.

- `Module.FinitePresentation.fg_ker`: If `M` is f.g., `N` is f.p., then `K` is f.g.

- `Module.finitePresentation_of_ker`: If `N` and `K` is f.p., then `M` is also f.p.

- `Module.FinitePresentation.isLocalizedModule_map`: If `M` and `N` are `R`-modules and `M` is f.p.,
  and `S` is a submonoid of `R`, then `Hom(Mₛ, Nₛ)` is the localization of `Hom(M, N)`.

Also the instances finite + free => f.p. => finite are also provided

## TODO
Suppose `S` is an `R`-algebra, `M` is an `S`-module. Then
1. If `S` is f.p., then `M` is `R`-f.p. implies `M` is `S`-f.p.
2. If `S` is both f.p. (as an algebra) and finite (as a module),
   then `M` is `S`-fp implies that `M` is `R`-f.p.
3. If `S` is f.p. as a module, then `S` is f.p. as an algebra.

In particular,
4. `S` is f.p. as an `R`-module iff it is f.p. as an algebra and is finite as a module.

For finitely presented algebras, see `Algebra.FinitePresentation`
in file `Mathlib/RingTheory/FinitePresentation.lean`.
-/

@[expose] public section

open Finsupp

section Semiring
variable (R M) [Semiring R] [AddCommMonoid M] [Module R M]

/--
A module is finitely presented if it is finitely generated by some set `s`
and the kernel of the presentation `Rˢ → M` is also finitely generated.
-/
class Module.FinitePresentation : Prop where
  out : ∃ (s : Finset M), Submodule.span R (s : Set M) = ⊤ ∧
    (LinearMap.ker (Finsupp.linearCombination R ((↑) : s → M))).FG

instance (priority := 100) [h : Module.FinitePresentation R M] : Module.Finite R M := by
  obtain ⟨s, hs₁, _⟩ := h
  exact ⟨s, hs₁⟩

end Semiring

section Ring

section

universe u v
variable (R : Type u) (M : Type*) [Ring R] [AddCommGroup M] [Module R M]

theorem Module.FinitePresentation.exists_fin [fp : Module.FinitePresentation R M] :
    ∃ (n : ℕ) (K : Submodule R (Fin n → R)) (_ : M ≃ₗ[R] (Fin n → R) ⧸ K), K.FG := by
  have ⟨ι, ⟨hι₁, hι₂⟩⟩ := fp
  refine ⟨_, LinearMap.ker (linearCombination R Subtype.val ∘ₗ
    (lcongr ι.equivFin (.refl ..) ≪≫ₗ linearEquivFunOnFinite R R _).symm.toLinearMap),
    (LinearMap.quotKerEquivOfSurjective _ <| LinearMap.range_eq_top.mp ?_).symm, ?_⟩
  · simpa [range_linearCombination] using hι₁
  · simpa [LinearMap.ker_comp, Submodule.comap_equiv_eq_map_symm] using hι₂.map _

/-- A finitely presented module is isomorphic to the quotient of a finite free module by a finitely
generated submodule. -/
theorem Module.FinitePresentation.equiv_quotient [Module.FinitePresentation R M] [Small.{v} R] :
    ∃ (L : Type v) (_ : AddCommGroup L) (_ : Module R L) (K : Submodule R L)
      (_ : M ≃ₗ[R] L ⧸ K), Module.Free R L ∧ Module.Finite R L ∧ K.FG :=
  have ⟨_n, _K, e, fg⟩ := Module.FinitePresentation.exists_fin R M
  let es := Shrink.linearEquiv
  ⟨_, inferInstance, inferInstance, _, e ≪≫ₗ Submodule.Quotient.equiv _ _ (es ..).symm rfl,
    .of_equiv (es ..).symm, .equiv (es ..).symm, fg.map (es ..).symm.toLinearMap⟩

end

variable (R M N) [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]

-- Ideally this should be an instance but it makes mathlib much slower.
lemma Module.finitePresentation_of_finite [IsNoetherianRing R] [h : Module.Finite R M] :
    Module.FinitePresentation R M := by
  obtain ⟨s, hs⟩ := h
  exact ⟨s, hs, IsNoetherian.noetherian _⟩

lemma Module.finitePresentation_iff_finite [IsNoetherianRing R] :
    Module.FinitePresentation R M ↔ Module.Finite R M :=
  ⟨fun _ ↦ inferInstance, fun _ ↦ finitePresentation_of_finite R M⟩

variable {R M N}

lemma Module.finitePresentation_of_free_of_surjective [Module.Free R M] [Module.Finite R M]
    (l : M →ₗ[R] N)
    (hl : Function.Surjective l) (hl' : (LinearMap.ker l).FG) :
    Module.FinitePresentation R N := by
  classical
  let b := Module.Free.chooseBasis R M
  let π : Free.ChooseBasisIndex R M → (Set.finite_range (l ∘ b)).toFinset :=
    fun i ↦ ⟨l (b i), by simp⟩
  have : π.Surjective := fun ⟨x, hx⟩ ↦ by
    obtain ⟨y, rfl⟩ : ∃ a, l (b a) = x := by simpa using hx
    exact ⟨y, rfl⟩
  choose σ hσ using this
  have hπ : Subtype.val ∘ π = l ∘ b := rfl
  have hσ₁ : π ∘ σ = id := by ext i; exact congr_arg Subtype.val (hσ i)
  have hσ₂ : l ∘ b ∘ σ = Subtype.val := by ext i; exact congr_arg Subtype.val (hσ i)
  refine ⟨(Set.finite_range (l ∘ b)).toFinset,
    by simpa [Set.range_comp, LinearMap.range_eq_top], ?_⟩
  let f : M →ₗ[R] (Set.finite_range (l ∘ b)).toFinset →₀ R :=
    Finsupp.lmapDomain _ _ π ∘ₗ b.repr.toLinearMap
  convert! hl'.map f
  ext x; simp only [LinearMap.mem_ker, Submodule.mem_map]
  constructor
  · intro hx
    refine ⟨b.repr.symm (x.mapDomain σ), ?_, ?_⟩
    · simp [Finsupp.apply_linearCombination, hσ₂, hx]
    · simp only [f, LinearMap.comp_apply, b.repr.apply_symm_apply,
        LinearEquiv.coe_toLinearMap, Finsupp.lmapDomain_apply]
      rw [← Finsupp.mapDomain_comp, hσ₁, Finsupp.mapDomain_id]
  · rintro ⟨y, hy, rfl⟩
    simp [f, hπ, ← Finsupp.apply_linearCombination, hy]

-- Ideally this should be an instance but it makes mathlib much slower.
variable (R M) in
lemma Module.finitePresentation_of_projective [Projective R M] [Module.Finite R M] :
    FinitePresentation R M :=
  have ⟨_n, _f, _g, surj, _, hfg⟩ := Finite.exists_comp_eq_id_of_projective R M
  Module.finitePresentation_of_free_of_surjective _ surj
    (LinearMap.ker_eq_range_of_comp_eq_id hfg ▸ .of_finite)

variable {ι} [Finite ι]

instance : Module.FinitePresentation R R := Module.finitePresentation_of_projective _ _
instance : Module.FinitePresentation R (ι →₀ R) := Module.finitePresentation_of_projective _ _
instance : Module.FinitePresentation R (ι → R) := Module.finitePresentation_of_projective _ _

lemma Module.finitePresentation_of_surjective [h : Module.FinitePresentation R M] (l : M →ₗ[R] N)
    (hl : Function.Surjective l) (hl' : (LinearMap.ker l).FG) :
    Module.FinitePresentation R N := by
  classical
  obtain ⟨s, hs, hs'⟩ := h
  obtain ⟨t, ht⟩ := hl'
  have H : Function.Surjective (Finsupp.linearCombination R ((↑) : s → M)) :=
    LinearMap.range_eq_top.mp
      (by rw [range_linearCombination, Subtype.range_val, ← hs])
  apply Module.finitePresentation_of_free_of_surjective (l ∘ₗ linearCombination R Subtype.val)
    (hl.comp H)
  choose σ hσ using (show _ from H)
  have : Finsupp.linearCombination R Subtype.val '' σ '' t = t := by
    simp only [Set.image_image, hσ, Set.image_id']
  rw [LinearMap.ker_comp, ← ht, ← this, ← Submodule.map_span, Submodule.comap_map_eq,
    ← Finset.coe_image]
  exact Submodule.FG.sup ⟨_, rfl⟩ hs'

lemma Module.FinitePresentation.fg_ker [Module.Finite R M]
    [h : Module.FinitePresentation R N] (l : M →ₗ[R] N) (hl : Function.Surjective l) :
    (LinearMap.ker l).FG := by
  classical
  obtain ⟨s, hs, hs'⟩ := h
  have H : Function.Surjective (Finsupp.linearCombination R ((↑) : s → N)) :=
    LinearMap.range_eq_top.mp
      (by rw [range_linearCombination, Subtype.range_val, ← hs])
  obtain ⟨f, hf⟩ : ∃ f : (s →₀ R) →ₗ[R] M, l ∘ₗ f = (Finsupp.linearCombination R Subtype.val) := by
    choose f hf using show _ from hl
    exact ⟨Finsupp.linearCombination R (fun i ↦ f i), by ext; simp [hf]⟩
  have : (LinearMap.ker l).map (LinearMap.range f).mkQ = ⊤ := by
    rw [← top_le_iff]
    rintro x -
    obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective _ x
    obtain ⟨y, hy⟩ := H (l x)
    rw [← hf, LinearMap.comp_apply, eq_comm, ← sub_eq_zero, ← map_sub] at hy
    exact ⟨_, hy, by simp⟩
  apply Submodule.fg_of_fg_map_of_fg_inf_ker (LinearMap.range f).mkQ
  · rw [this]
    exact Module.Finite.fg_top
  · rw [Submodule.ker_mkQ, inf_comm, ← Submodule.map_comap_eq, ← LinearMap.ker_comp, hf]
    exact hs'.map f

lemma Module.FinitePresentation.fg_ker_iff [Module.FinitePresentation R M]
    (l : M →ₗ[R] N) (hl : Function.Surjective l) :
    Submodule.FG (LinearMap.ker l) ↔ Module.FinitePresentation R N :=
  ⟨finitePresentation_of_surjective l hl, fun _ ↦ fg_ker l hl⟩

lemma Module.finitePresentation_of_ker [Module.FinitePresentation R N]
    (l : M →ₗ[R] N) (hl : Function.Surjective l) [Module.FinitePresentation R (LinearMap.ker l)] :
    Module.FinitePresentation R M := by
  obtain ⟨s, hs⟩ : (⊤ : Submodule R M).FG := by
    apply Submodule.fg_of_fg_map_of_fg_inf_ker l
    · rw [Submodule.map_top, LinearMap.range_eq_top.mpr hl]; exact Module.Finite.fg_top
    · rw [top_inf_eq, ← Module.Finite.iff_fg]; infer_instance
  refine ⟨s, hs, ?_⟩
  let π := Finsupp.linearCombination R ((↑) : s → M)
  have H : Function.Surjective π :=
    LinearMap.range_eq_top.mp
      (by rw [range_linearCombination, Subtype.range_val, ← hs])
  have inst : Module.Finite R (LinearMap.ker (l ∘ₗ π)) :=
    .of_fg <| Module.FinitePresentation.fg_ker _ (hl.comp H)
  let f : LinearMap.ker (l ∘ₗ π) →ₗ[R] LinearMap.ker l := LinearMap.restrict π (fun x ↦ id)
  have e : π ∘ₗ Submodule.subtype _ = Submodule.subtype _ ∘ₗ f := by ext; rfl
  have hf : Function.Surjective f := by
    rw [← LinearMap.range_eq_top]
    apply Submodule.map_injective_of_injective (Submodule.injective_subtype _)
    rw [Submodule.map_top, Submodule.range_subtype, ← LinearMap.range_comp, ← e,
      LinearMap.range_comp, Submodule.range_subtype, LinearMap.ker_comp,
      Submodule.map_comap_eq_of_surjective H]
  change (LinearMap.ker π).FG
  have : LinearMap.ker π ≤ LinearMap.ker (l ∘ₗ π) :=
    Submodule.comap_mono (f := π) (bot_le (a := LinearMap.ker l))
  rw [← inf_eq_right.mpr this, ← Submodule.range_subtype (LinearMap.ker _),
    ← Submodule.map_comap_eq, ← LinearMap.ker_comp, e, LinearMap.ker_comp f,
    LinearMap.ker_eq_bot.mpr (Submodule.injective_subtype (LinearMap.ker l)), Submodule.comap_bot]
  exact (Module.FinitePresentation.fg_ker f hf).map (Submodule.subtype _)

/-- Given a split exact sequence `0 → M → N → P → 0` with `N` finitely presented,
then `M` is also finitely presented. -/
lemma Module.finitePresentation_of_split_exact
    {P : Type*} [AddCommGroup P] [Module R P]
    [Module.FinitePresentation R N]
    (f : M →ₗ[R] N) (g : N →ₗ[R] P) (l : P →ₗ[R] N) (hl : g ∘ₗ l = .id)
    (hf : Function.Injective f) (H : Function.Exact f g) :
    Module.FinitePresentation R M := by
  have hg : Function.Surjective g := Function.LeftInverse.surjective (DFunLike.congr_fun hl)
  have := Module.Finite.of_surjective g hg
  obtain ⟨e, rfl, rfl⟩ := ((Function.Exact.split_tfae' H).out 0 2 rfl rfl).mp
    ⟨hf, l, hl⟩
  refine Module.finitePresentation_of_surjective (LinearMap.fst _ _ _ ∘ₗ e.toLinearMap)
    (Prod.fst_surjective.comp e.surjective) ?_
  rw [LinearMap.ker_comp, Submodule.comap_equiv_eq_map_symm,
    LinearMap.exact_iff.mp Function.Exact.inr_fst, ← LinearMap.range_comp]
  exact Submodule.fg_range _

/-- Given an exact sequence `0 → M → N → P → 0`
with `N` finitely presented and `P` projective, then `M` is also finitely presented. -/
lemma Module.finitePresentation_of_projective_of_exact
    {P : Type*} [AddCommGroup P] [Module R P]
    [Module.FinitePresentation R N] [Module.Projective R P]
    (f : M →ₗ[R] N) (g : N →ₗ[R] P)
    (hf : Function.Injective f) (hg : Function.Surjective g) (H : Function.Exact f g) :
    Module.FinitePresentation R M :=
  have ⟨l, hl⟩ := Module.projective_lifting_property g .id hg
  Module.finitePresentation_of_split_exact f g l hl hf H

lemma Module.FinitePresentation.of_equiv (e : M ≃ₗ[R] N) [Module.FinitePresentation R M] :
    Module.FinitePresentation R N := by
  simp [← Module.FinitePresentation.fg_ker_iff e.toLinearMap e.surjective, Submodule.fg_bot]

lemma LinearEquiv.finitePresentation_iff (e : M ≃ₗ[R] N) :
    Module.FinitePresentation R M ↔ Module.FinitePresentation R N :=
  ⟨fun _ ↦ .of_equiv e, fun _ ↦ .of_equiv e.symm⟩

namespace Module.FinitePresentation

variable (M) in
instance (priority := 900) of_subsingleton [Subsingleton M] :
    Module.FinitePresentation R M :=
  .of_equiv (default : (Fin 0 → R) ≃ₗ[R] M)

variable (M N) in
instance prod [Module.FinitePresentation R M] [Module.FinitePresentation R N] :
    Module.FinitePresentation R (M × N) := by
  have hf : Function.Surjective (LinearMap.fst R M N) := LinearMap.fst_surjective
  have : FinitePresentation R ↥(LinearMap.ker (LinearMap.fst R M N)) := by
    rw [LinearMap.ker_fst]
    exact .of_equiv (LinearEquiv.ofInjective (LinearMap.inr R M N) LinearMap.inr_injective)
  apply Module.finitePresentation_of_ker (.fst R M N) hf

instance pi {ι : Type*} (M : ι → Type*)
    [∀ i, AddCommGroup (M i)] [∀ i, Module R (M i)] [∀ i, Module.FinitePresentation R (M i)]
    [Finite ι] : Module.FinitePresentation R (∀ i, M i) := by
  refine Module.pi_induction' (motive := fun N _ _ ↦ Module.FinitePresentation R N)
      (motive' := fun N _ _ ↦ Module.FinitePresentation R N) R ?_ ?_ ?_ ?_ M inferInstance
  · exact fun e (hN : Module.FinitePresentation _ _) ↦ .of_equiv e
  · exact fun e (hN : Module.FinitePresentation _ _) ↦ .of_equiv e
  · infer_instance
  · introv hN hN'
    infer_instance

end Module.FinitePresentation

end Ring

section CommRing

variable {R M N N'} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
variable [AddCommGroup N'] [Module R N'] (S : Submonoid R) (f : N →ₗ[R] N') [IsLocalizedModule S f]

variable (R M) in
lemma Module.FinitePresentation.trans (S : Type*) [CommRing S] [Algebra R S]
    [Module S M] [IsScalarTower R S M] [Module.FinitePresentation R S]
    [Module.FinitePresentation S M] : Module.FinitePresentation R M := by
  obtain ⟨n, K, e, hK⟩ := Module.FinitePresentation.exists_fin S M
  let f : (Fin n → S) →ₗ[R] M := (e.symm ∘ₗ K.mkQ).restrictScalars R
  refine Module.finitePresentation_of_surjective f (fun m ↦ ?_) ?_
  · obtain ⟨a, ha⟩ := K.mkQ_surjective (e m)
    exact ⟨a, by simp [f, ha]⟩
  · have : Module.Finite S
        (Submodule.restrictScalars R (LinearMap.ker (e.symm.toLinearMap ∘ₗ K.mkQ))) :=
      .of_fg <| show (LinearMap.ker (e.symm.toLinearMap ∘ₗ K.mkQ)).FG by simpa
    simp only [f, LinearMap.ker_restrictScalars, ← Module.Finite.iff_fg]
    exact Module.Finite.trans S _

open TensorProduct in
instance {A} [CommRing A] [Algebra R A] [Module.FinitePresentation R M] :
    Module.FinitePresentation A (A ⊗[R] M) := by
  classical
  obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R M
  have inst := Module.finitePresentation_of_projective A (A ⊗[R] (Fin n → R))
  apply Module.finitePresentation_of_surjective (f.baseChange A)
    (LinearMap.lTensor_surjective A hf)
  have : Function.Exact ((LinearMap.ker f).subtype.baseChange A) (f.baseChange A) :=
    lTensor_exact A f.exact_subtype_ker_map hf
  rw [LinearMap.exact_iff] at this
  rw [this]
  have : Module.Finite R (LinearMap.ker f) :=
    .of_fg (Module.FinitePresentation.fg_ker f hf)
  exact Submodule.fg_range _

open TensorProduct in
lemma FinitePresentation.of_isBaseChange
    {A} [CommRing A] [Algebra R A] [Module A N] [IsScalarTower R A N]
    (f : M →ₗ[R] N) (h : IsBaseChange A f) [Module.FinitePresentation R M] :
    Module.FinitePresentation A N :=
  Module.finitePresentation_of_surjective
    h.equiv.toLinearMap h.equiv.surjective (by simpa using Submodule.fg_bot)

open TensorProduct in
instance (S : Submonoid R) [Module.FinitePresentation R M] :
    Module.FinitePresentation (Localization S) (LocalizedModule S M) :=
  FinitePresentation.of_isBaseChange (LocalizedModule.mkLinearMap S M)
    ((isLocalizedModule_iff_isBaseChange S _ _).mp inferInstance)

lemma Module.FinitePresentation.exists_lift_of_isLocalizedModule
    [h : Module.FinitePresentation R M] (g : M →ₗ[R] N') :
    ∃ (h : M →ₗ[R] N) (s : S), f ∘ₗ h = s • g := by
  obtain ⟨σ, hσ, τ, hτ⟩ := h
  let π := Finsupp.linearCombination R ((↑) : σ → M)
  have hπ : Function.Surjective π :=
    LinearMap.range_eq_top.mp
      (by rw [range_linearCombination, Subtype.range_val, ← hσ])
  classical
  choose s hs using IsLocalizedModule.surj S f
  let i : σ → N :=
    fun x ↦ (∏ j ∈ σ.erase x.1, (s (g j)).2) • (s (g x)).1
  let s₀ := ∏ j ∈ σ, (s (g j)).2
  have hi : f ∘ₗ Finsupp.linearCombination R i = (s₀ • g) ∘ₗ π := by
    ext j
    simp only [LinearMap.coe_comp, Function.comp_apply, Finsupp.lsingle_apply,
      linearCombination_single, one_smul, LinearMap.map_smul_of_tower, ← hs, LinearMap.smul_apply,
      i, s₀, π]
    rw [← mul_smul, Finset.prod_erase_mul]
    exact j.prop
  have : ∀ x : τ, ∃ s : S, s • (Finsupp.linearCombination R i x) = 0 := by
    intro x
    convert_to ∃ s : S, s • (Finsupp.linearCombination R i x) = s • 0
    · simp only [smul_zero]
    apply IsLocalizedModule.exists_of_eq (S := S) (f := f)
    rw [← LinearMap.comp_apply, map_zero, hi, LinearMap.comp_apply]
    convert! map_zero (s₀ • g)
    rw [← LinearMap.mem_ker, ← hτ]
    exact Submodule.subset_span x.prop
  choose s' hs' using this
  let s₁ := ∏ i : τ, s' i
  have : LinearMap.ker π ≤ LinearMap.ker (s₁ • Finsupp.linearCombination R i) := by
    rw [← hτ, Submodule.span_le]
    intro x hxσ
    simp only [s₁]
    rw [SetLike.mem_coe, LinearMap.mem_ker, LinearMap.smul_apply,
      ← Finset.prod_erase_mul _ _ (Finset.mem_univ ⟨x, hxσ⟩), mul_smul]
    convert! smul_zero _
    exact hs' ⟨x, hxσ⟩
  refine ⟨Submodule.liftQ _ _ this ∘ₗ
    (LinearMap.quotKerEquivOfSurjective _ hπ).symm.toLinearMap, s₁ * s₀, ?_⟩
  ext x
  obtain ⟨x, rfl⟩ := hπ x
  rw [← LinearMap.comp_apply, ← LinearMap.comp_apply, mul_smul, LinearMap.smul_comp, ← hi,
    ← LinearMap.comp_smul, LinearMap.comp_assoc, LinearMap.comp_assoc]
  simp

/-- Let `M` be a finitely presented `R`-module, `N` be an `R`-module, `S` be a submonoid of `R`,
`Mₚ` be the localization of `M` at `S`, `Nₚ` be the localization of `N` at `S`. Then any surjective
linear map `ϕ : Mₚ →ₗ[R] Nₚ` lifts to a linear map `φ : M →ₗ[R] N` that is surjective after
localization at `S`. -/
lemma Module.exists_localizedMap_surjective_of_surjective [Module.FinitePresentation R M]
    (S : Submonoid R) {Mₚ : Type*} [AddCommGroup Mₚ] [Module R Mₚ]
    (f : M →ₗ[R] Mₚ) [IsLocalizedModule S f] {Nₚ : Type*} [AddCommGroup Nₚ] [Module R Nₚ]
    (g : N →ₗ[R] Nₚ) [IsLocalizedModule S g] {ϕ : Mₚ →ₗ[R] Nₚ} (hϕ : Function.Surjective ϕ) :
    ∃ (φ : M →ₗ[R] N) (s : S) (_ : IsLocalizedModule.map S f g φ = s • ϕ),
      Function.Surjective (IsLocalizedModule.map S f g φ) := by
  obtain ⟨φ, s, hφ⟩ := FinitePresentation.exists_lift_of_isLocalizedModule S g (ϕ ∘ₗ f)
  have hmap : IsLocalizedModule.map S f g φ = s • ϕ := by
    apply IsLocalizedModule.linearMap_ext S f g
    simp [IsLocalizedModule.map_comp, hφ, LinearMap.smul_comp]
  refine ⟨φ, s, hmap, ?_⟩
  simpa only [hmap] using! ((End.isUnit_iff _).mp (IsLocalizedModule.map_units g s)).2.comp hϕ

lemma Module.Finite.exists_smul_of_comp_eq_of_isLocalizedModule
    [hM : Module.Finite R M] (g₁ g₂ : M →ₗ[R] N) (h : f.comp g₁ = f.comp g₂) :
    ∃ (s : S), s • g₁ = s • g₂ := by
  classical
  have : ∀ x, ∃ s : S, s • g₁ x = s • g₂ x := fun x ↦
    IsLocalizedModule.exists_of_eq (S := S) (f := f) (LinearMap.congr_fun h x)
  choose s hs using this
  obtain ⟨σ, hσ⟩ := hM
  use σ.prod s
  rw [← sub_eq_zero, ← LinearMap.ker_eq_top, ← top_le_iff, ← hσ, Submodule.span_le]
  intro x hx
  simp only [SetLike.mem_coe, LinearMap.mem_ker, LinearMap.sub_apply, LinearMap.smul_apply,
    sub_eq_zero, ← Finset.prod_erase_mul σ s hx, mul_smul, hs]

variable {M' : Type*} [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f]
variable {N' : Type*} [AddCommGroup N'] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g]

/--
Let `M` be a finite `R`-module, and `N` be a finitely presented `R`-module.
If `l : M →ₗ[R] N` is a linear map whose localization at `S : Submonoid R` is bijective,
then `l` is already bijective under the localization at some `r ∈ S`.
-/
lemma exists_bijective_map_powers [Module.Finite R M] [Module.FinitePresentation R N]
    (l : M →ₗ[R] N) (hf : Function.Bijective (IsLocalizedModule.map S f g l)) :
    ∃ r, r ∈ S ∧ ∀ t, r ∣ t → Function.Bijective (LocalizedModule.map (.powers t) l) := by
  let e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective _ hf
  obtain ⟨l', s₀, H⟩ := Module.FinitePresentation.exists_lift_of_isLocalizedModule S f
    (e.symm.toLinearMap.comp g)
  have H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ (s₀ • LinearMap.id) := by
    ext a; simpa [-EmbeddingLike.apply_eq_iff_eq, e] using congr(e ($H a))
  obtain ⟨s₁, hs₁⟩ := Module.Finite.exists_smul_of_comp_eq_of_isLocalizedModule S g _ _ H₁
  have H₂ : f ∘ₗ l' ∘ₗ l = f ∘ₗ (s₀ • LinearMap.id) := by
    rw [← LinearMap.comp_assoc, H, LinearMap.smul_comp, LinearMap.comp_assoc,
      ← IsLocalizedModule.map_comp S f g l, ← LinearMap.comp_assoc]
    change s₀ • (e.symm.toLinearMap ∘ₗ e.toLinearMap) ∘ₗ _ = _
    simp [LinearMap.comp_smul]
  obtain ⟨s₂, hs₂⟩ := Module.Finite.exists_smul_of_comp_eq_of_isLocalizedModule S f _ _ H₂
  refine ⟨s₀ * s₁ * s₂, (s₀ * s₁ * s₂).2, fun t ht ↦ ?_⟩
  let Rₛ := Localization (.powers t)
  let lₛ := LocalizedModule.map (.powers t) l
  have hu := IsLocalization.map_units (M := .powers t) Rₛ ⟨t, Submonoid.mem_powers t⟩
  have hu₀ : IsUnit (algebraMap R Rₛ s₀) := isUnit_of_dvd_unit
      (map_dvd (algebraMap R Rₛ) (dvd_trans ⟨s₁ * s₂, by simp [mul_assoc]⟩ ht)) hu
  have hu₁ : IsUnit (algebraMap R Rₛ s₁) := isUnit_of_dvd_unit
      (map_dvd (algebraMap R Rₛ) (dvd_trans ⟨s₀ * s₂, by ring⟩ ht)) hu
  have hu₂ : IsUnit (algebraMap R Rₛ s₂) := isUnit_of_dvd_unit
      (map_dvd (algebraMap R Rₛ) (dvd_trans ⟨s₀ * s₁, by ring⟩ ht)) hu
  let lₛ' := LocalizedModule.map (.powers t) l'
  have H_left : ((hu₀.unit⁻¹).1 • lₛ') ∘ₗ lₛ = LinearMap.id := by
    apply ((Module.End.isUnit_iff _).mp (hu₂.map (algebraMap Rₛ (Module.End Rₛ _)))).1
    apply ((Module.End.isUnit_iff _).mp (hu₀.map (algebraMap Rₛ (Module.End Rₛ _)))).1
    simp only [Module.algebraMap_end_apply, algebraMap_smul, LinearMap.map_smul_of_tower]
    rw [LinearMap.smul_comp, ← smul_assoc s₀.1, Algebra.smul_def s₀.1, IsUnit.mul_val_inv, one_smul]
    apply LinearMap.restrictScalars_injective R
    apply IsLocalizedModule.ext (.powers t) (LocalizedModule.mkLinearMap (.powers t) M)
      (IsLocalizedModule.map_units (LocalizedModule.mkLinearMap (.powers t) M))
    ext x
    have : s₂.1 • l' (l x) = s₂.1 • s₀.1 • x := congr($hs₂ x)
    simp [lₛ, lₛ', LocalizedModule.smul'_mk, this]
  have H_right : lₛ ∘ₗ ((hu₀.unit⁻¹).1 • lₛ') = LinearMap.id := by
    apply ((Module.End.isUnit_iff _).mp (hu₁.map (algebraMap Rₛ (Module.End Rₛ _)))).1
    apply ((Module.End.isUnit_iff _).mp (hu₀.map (algebraMap Rₛ (Module.End Rₛ _)))).1
    simp only [Module.algebraMap_end_apply, algebraMap_smul, LinearMap.map_smul_of_tower]
    rw [LinearMap.comp_smul, ← smul_assoc s₀.1, Algebra.smul_def s₀.1, IsUnit.mul_val_inv, one_smul]
    apply LinearMap.restrictScalars_injective R
    apply IsLocalizedModule.ext (.powers t) (LocalizedModule.mkLinearMap (.powers t) N)
      (IsLocalizedModule.map_units (LocalizedModule.mkLinearMap (.powers t) N))
    ext x
    have : s₁.1 • l (l' x) = s₁.1 • s₀.1 • x := congr($hs₁ x)
    simp [lₛ, lₛ', LocalizedModule.smul'_mk, this]
  let eₛ : LocalizedModule.Away t M ≃ₗ[Rₛ] LocalizedModule.Away t N :=
    { __ := lₛ,
      invFun := ((hu₀.unit⁻¹).1 • lₛ'),
      left_inv := fun x ↦ congr($H_left x),
      right_inv := fun x ↦ congr($H_right x) }
  exact eₛ.bijective

/-- Let `M` be a finite `R`-module and `N` be a finitely presented `R`-module. If `f : M →ₗ[R] N`
is a linear map whose localization at a prime ideal `p` is bijective, then there exists
`g ∉ p` such that `f` is already bijective under the localization away from `g`. -/
lemma Module.FinitePresentation.exists_notMem_bijective [Module.Finite R M]
    [Module.FinitePresentation R N] (f : M →ₗ[R] N) (p : Ideal R) [p.IsPrime] {Mₚ Nₚ : Type*}
    [AddCommGroup Mₚ] [AddCommGroup Nₚ] [Module R Mₚ] [Module R Nₚ]
    (fM : M →ₗ[R] Mₚ) (fN : N →ₗ[R] Nₚ)
    [IsLocalizedModule p.primeCompl fM] [IsLocalizedModule p.primeCompl fN]
    (hf : Function.Bijective (IsLocalizedModule.map p.primeCompl fM fN f)) :
    ∃ (g : R), g ∉ p ∧ Function.Bijective (LocalizedModule.map (Submonoid.powers g) f) := by
  obtain ⟨g, hg, h⟩ := exists_bijective_map_powers p.primeCompl fM fN f hf
  exact ⟨g, hg, h g dvd_rfl⟩

open IsLocalizedModule in
/--
Let `M` `N` be a finitely presented `R`-modules.
Any `Mₛ ≃ₗ[R] Nₛ` between the localizations at `S : Submonoid R` can be lifted to an
isomorphism between `Mᵣ ≃ₗ[R] Nᵣ` for some `r ∈ S`.
-/
lemma Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule
    [Module.FinitePresentation R M] [Module.FinitePresentation R N]
    (l : M' ≃ₗ[R] N') :
    ∃ (r : R) (hr : r ∈ S)
      (l' : LocalizedModule.Away r M ≃ₗ[Localization (.powers r)]
        LocalizedModule.Away r N),
      (LocalizedModule.lift (.powers r) g fun s ↦ map_units g ⟨s.1, SetLike.le_def.mp
        (Submonoid.powers_le.mpr hr) s.2⟩) ∘ₗ l'.toLinearMap =
        l ∘ₗ (LocalizedModule.lift (.powers r) f fun s ↦ map_units f ⟨s.1, SetLike.le_def.mp
        (Submonoid.powers_le.mpr hr) s.2⟩) := by
  obtain ⟨l', s, H⟩ := Module.FinitePresentation.exists_lift_of_isLocalizedModule S g (l ∘ₗ f)
  have : Function.Bijective (IsLocalizedModule.map S f g l') := by
    have : IsLocalizedModule.map S f g l' = (s • LinearMap.id) ∘ₗ l := by
      apply IsLocalizedModule.ext S f (IsLocalizedModule.map_units g)
      apply LinearMap.ext fun x ↦ ?_
      simp only [LinearMap.coe_comp, Function.comp_apply, IsLocalizedModule.map_apply]
      rw [← LinearMap.comp_apply, H]
      simp
    rw [this]
    exact ((Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units g s)).comp l.bijective
  obtain ⟨r, hr, hr'⟩ := exists_bijective_map_powers S f g _ this
  let rs : Submonoid R := (.powers <| r * s)
  let Rᵣₛ := Localization rs
  have hsu : IsUnit (algebraMap R Rᵣₛ s) := isUnit_of_dvd_unit
      (hu := IsLocalization.map_units (M := rs) Rᵣₛ ⟨_, Submonoid.mem_powers _⟩)
      (map_dvd (algebraMap R Rᵣₛ) ⟨r, mul_comm _ _⟩)
  have : Function.Bijective ((hsu.unit⁻¹).1 • LocalizedModule.map rs l') :=
    ((Module.End.isUnit_iff _).mp ((hsu.unit⁻¹).isUnit.map (algebraMap _ (End Rᵣₛ
      (LocalizedModule rs N))))).comp (hr' (r * s) (dvd_mul_right _ _))
  refine ⟨r * s, mul_mem hr s.2, LinearEquiv.ofBijective _ this, ?_⟩
  apply IsLocalizedModule.ext rs (LocalizedModule.mkLinearMap rs M) fun x ↦ map_units g
    ⟨x.1, SetLike.le_def.mp (Submonoid.powers_le.mpr (mul_mem hr s.2)) x.2⟩
  ext x
  apply ((Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units g s)).1
  have : ∀ x, g (l' x) = s.1 • (l (f x)) := LinearMap.congr_fun H
  simp only [rs, LinearMap.coe_comp, LinearMap.coe_restrictScalars, LinearEquiv.coe_coe,
    Function.comp_apply, LocalizedModule.mkLinearMap_apply, LinearEquiv.ofBijective_apply,
    LinearMap.smul_apply, LocalizedModule.map_mk, algebraMap_end_apply]
  rw [← map_smul, ← smul_assoc, Algebra.smul_def s.1, hsu.mul_val_inv, one_smul]
  simp only [LocalizedModule.lift_mk, OneMemClass.coe_one, map_one, IsUnit.unit_one,
    inv_one, Units.val_one, Module.End.one_apply, this]

instance Module.FinitePresentation.isLocalizedModule_map [Module.FinitePresentation R M] :
    IsLocalizedModule S (IsLocalizedModule.map S f g) := by
  constructor
  · intro s
    rw [Module.End.isUnit_iff]
    have := (Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units (S := S) (f := g) s)
    constructor
    · exact fun _ _ e ↦ LinearMap.ext fun m ↦ this.left (LinearMap.congr_fun e m)
    · intro h
      use ((IsLocalizedModule.map_units (S := S) (f := g) s).unit⁻¹).1 ∘ₗ h
      ext x
      exact Module.End.isUnit_apply_inv_apply_of_isUnit
        (IsLocalizedModule.map_units (S := S) (f := g) s) (h x)
  · intro h
    obtain ⟨h', s, e⟩ := Module.FinitePresentation.exists_lift_of_isLocalizedModule S g (h ∘ₗ f)
    refine ⟨⟨h', s⟩, ?_⟩
    apply IsLocalizedModule.ext S f (IsLocalizedModule.map_units g)
    refine e.symm.trans (by ext; simp)
  · intro h₁ h₂ e
    apply Module.Finite.exists_smul_of_comp_eq_of_isLocalizedModule S g
    ext x
    simpa using LinearMap.congr_fun e (f x)

instance Module.FinitePresentation.isLocalizedModule_mapExtendScalars
    (Rₛ) [CommRing Rₛ] [Algebra R Rₛ] [Module Rₛ M'] [Module Rₛ N']
    [IsScalarTower R Rₛ M'] [IsScalarTower R Rₛ N'] [IsLocalization S Rₛ]
    [Module.FinitePresentation R M] :
    IsLocalizedModule S (IsLocalizedModule.mapExtendScalars S f g Rₛ) :=
  IsLocalizedModule.of_linearEquiv _ _ _

instance [Module.FinitePresentation R M] :
    IsLocalizedModule S (LocalizedModule.map S (M := M) (N := N)) :=
  Module.FinitePresentation.isLocalizedModule_mapExtendScalars _ _ _ _

/-- If `M` is a finite `R`-module, and the localization `Mₛ` at some submonoid `S` of `R`
is finitely presented, then `Mₛ = M[1/r]` for some `r ∈ S`. -/
lemma IsLocalizedModule.exists_isLocalizedModule_powers_of_finitePresentation
    [Module.Finite R M] [Module.FinitePresentation R M'] :
    ∃ r ∈ S, IsLocalizedModule.Away r f := by
  have : IsLocalizedModule S (.id (R := R) (M := M')) :=
    ⟨IsLocalizedModule.map_units f, fun y ↦ ⟨⟨y, 1⟩, by simp⟩, by simpa using ⟨1, S.one_mem⟩⟩
  obtain ⟨r, hrp, H⟩ := exists_bijective_map_powers S
      f (.id (R := R) (M := M')) f <| by
    convert! show Function.Bijective LinearMap.id from Function.bijective_id
    apply IsLocalizedModule.ext S f
    · exact IsLocalizedModule.map_units f
    · simp [IsLocalizedModule.map_comp]
  have hrp' : .powers r ≤ S := by simpa [Submonoid.powers_le]
  refine ⟨r, hrp, ⟨fun x ↦ IsLocalizedModule.map_units f ⟨x, hrp' x.2⟩, ?_, ?_⟩⟩
  · intro y
    obtain ⟨x, hx⟩ := (H _ dvd_rfl).2 (LocalizedModule.mkLinearMap _ _ y)
    obtain ⟨⟨x, ⟨_, n, rfl⟩⟩, rfl⟩ := IsLocalizedModule.mk'_surjective
      (.powers r) (LocalizedModule.mkLinearMap _ _) x
    obtain ⟨m, hm⟩ : ∃ m, r ^ (m + n) • y = f (r ^ m • x) := by
      simpa [LocalizedModule.map, IsLocalizedModule.mk_eq_mk', -IsLocalizedModule.mk'_one,
        pow_add, mul_smul, IsLocalizedModule.mk'_eq_mk'_iff, Submonoid.mem_powers_iff,
        Submonoid.smul_def] using hx
    exact ⟨⟨_, ⟨_, _, rfl⟩⟩, hm⟩
  · exact fun {x₁ x₂} hx ↦ IsLocalizedModule.exists_of_eq (f := LocalizedModule.mkLinearMap
      (.powers r) _) ((H _ dvd_rfl).1 (by simp [hx]))

/--
Let `M` be a finitely presented `R`-module, `N` an `R`-module, `S : Submonoid R`.
The linear equivalence between the `M →ₗ[R] N` localized at `S` and
`LocalizedModule S M →ₗ[R] LocalizedModule S N`
-/
noncomputable def Module.FinitePresentation.linearEquivMap [Module.FinitePresentation R M] :=
  IsLocalizedModule.linearEquiv S (LocalizedModule.mkLinearMap S (M →ₗ[R] N))
  (IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N))

lemma Module.FinitePresentation.linearEquivMap_apply [Module.FinitePresentation R M]
    (f : M →ₗ[R] N) : Module.FinitePresentation.linearEquivMap S
    ((LocalizedModule.mkLinearMap S (M →ₗ[R] N)) f) = (IsLocalizedModule.map S
    (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N)) f :=
  IsLocalizedModule.linearEquiv_apply S _ _ f

@[simp]
lemma Module.FinitePresentation.linearEquivMap_symm_apply [Module.FinitePresentation R M]
    (f : M →ₗ[R] N) : (Module.FinitePresentation.linearEquivMap S).symm ((IsLocalizedModule.map S
    (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N)) f) =
    (LocalizedModule.mkLinearMap S (M →ₗ[R] N)) f :=
  IsLocalizedModule.linearEquiv_symm_apply S _ _ f

/--
Let `M` be a finitely presented `R`-module, `N` an `R`-module, `S : Submonoid R`.
The linear equivalence between the `M →ₗ[R] N` localized at `S` and
`LocalizedModule S M →ₗ[Localization S] LocalizedModule S N`
-/
noncomputable def Module.FinitePresentation.linearEquivMapExtendScalars
    [Module.FinitePresentation R M] :=
  IsLocalizedModule.linearEquiv S (LocalizedModule.mkLinearMap S (M →ₗ[R] N))
  (IsLocalizedModule.mapExtendScalars S (LocalizedModule.mkLinearMap S M)
    (LocalizedModule.mkLinearMap S N) (Localization S))

lemma Module.FinitePresentation.linearEquivMapExtendScalars_apply [Module.FinitePresentation R M]
    (f : M →ₗ[R] N) : Module.FinitePresentation.linearEquivMapExtendScalars S
    ((LocalizedModule.mkLinearMap S (M →ₗ[R] N)) f) = (IsLocalizedModule.mapExtendScalars S
    (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N) (Localization S)) f :=
  IsLocalizedModule.linearEquiv_apply S _ _ f

@[simp]
lemma Module.FinitePresentation.linearEquivMapExtendScalars_symm_apply
    [Module.FinitePresentation R M] (f : M →ₗ[R] N) :
    (Module.FinitePresentation.linearEquivMapExtendScalars S).symm
    ((IsLocalizedModule.mapExtendScalars S (LocalizedModule.mkLinearMap S M)
    (LocalizedModule.mkLinearMap S N) (Localization S)) f) =
    (LocalizedModule.mkLinearMap S (M →ₗ[R] N)) f :=
  IsLocalizedModule.linearEquiv_symm_apply S _ _ f

end CommRing