A criterion for finiteness given a right exact sequence

Stream: Is there code for X?

[Kenny Lau]

import Mathlib

variable {R M₁ M₂ M₃ : Type*} [CommRing R]
  [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃]
  [Module R M₁] [Module R M₂] [Module R M₃]
  (f : M₁ →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) (hfg : Function.Exact f g) (hg : Function.Surjective g)
  (fin₁ : Module.Finite R M₁) (fin₃ : Module.Finite R M₃)

include hfg hg fin₁ fin₃ in
theorem Module.Finite.of_exact_of_surjective : Module.Finite R M₂ := by
  sorry

[Kenny Lau]

if $M_1 \to M_2 \to M_3 \to 0$ is exact and $M_1$ and $M_3$ are module finite then $M_2$ is module finite

[Kenny Lau]

Context is my comment to @Anthony Fernandes's PR #28451

[Riccardo Brasca]

I vaguely remember something like that is there.

[Riccardo Brasca]

Submodule.fg_of_fg_map_of_fg_inf_ker

[Kenny Lau]

I deliberately omitted 0 -> here

[Riccardo Brasca]

ah sorry, you don't have injectivity on the left

[Riccardo Brasca]

Can't you replace the first map by the inclusion of the image?

[Kenny Lau]

yeah, but that's an extra step

[Kenny Lau]

like yes i think you can use your lemma to prove my sorry

[Riccardo Brasca]

yes, but it's maybe not a lot of work

[Kenny Lau]

yeah, but it's unfair for me to suggest this to a PR

[Kenny Lau]

but thanks for finding that lemma

[Anthony Fernandes]

I managed to make this very ugly proof of the claim but at least it compiles

import Mathlib

open Function Set Module Submodule

variable {L M N R S T : Type*}
  [AddCommGroup L] [Semiring R] [Module R L]
  [AddCommGroup M] [Ring S] [Module S M]
  [AddCommGroup N] [Semiring T] [Module T N]
  (σ : R →+* S) (τ : S →+* T) (f : L →ₛₗ[σ] M) (g : M →ₛₗ[τ] N)
  (surj_τ : Surjective τ) (surj_g : Surjective g) (exact_f_g : Exact (P := N) f g)
  (finite_L : Module.Finite R L) (finite_N : Module.Finite T N)
include surj_τ surj_g exact_f_g finite_L finite_N

theorem foo : Module.Finite S M := by
  obtain ⟨L', span_L'⟩ := finite_L
  obtain ⟨N', span_N'⟩ := finite_N
  refine ⟨Submodule.fg_def.2 ⟨f '' L' ∪ (surjInv surj_g) '' N', by use_finite_instance, top_le_iff.1 fun x _ ↦ ?_⟩⟩
  obtain ⟨α, n, n_subset_N', _, sum_α_eq_g_x⟩ := mem_span_iff_exists_finset_subset.1 (span_N' ▸ trivial : g x ∈ span T N')
  replace sum_α_eq_g_x : g (∑ x ∈ n, surjInv surj_τ (α x) • surjInv surj_g x - x) = 0 :=
    calc g (∑ x ∈ n, surjInv surj_τ (α x) • surjInv surj_g x - x)
      _ = ∑ x ∈ n, g (surjInv surj_τ (α x) • surjInv surj_g x) - g x := by rw [map_sub, map_sum]
      _ = ∑ x ∈ n, (α x) • x - g x := by simp [map_smulₛₗ, surjInv_eq]
      _ = g x - g x := by rw [sum_α_eq_g_x]
      _ = 0 := sub_self _
  obtain ⟨y, hfy⟩ := (exact_f_g _).1 sum_α_eq_g_x
  obtain ⟨β, l, l_subset_L', _, rfl⟩ := mem_span_iff_exists_finset_subset.1 (span_L' ▸ trivial : y ∈ span R L')
  replace hfy := eq_sub_of_add_eq' <| add_eq_of_eq_sub hfy
  rw [sub_eq_neg_add] at hfy
  rw [span_union, mem_sup]
  refine ⟨_, ?_, _, ?_, hfy.symm⟩
  · simp only [map_sum, LinearMap.map_smulₛₗ, neg_mem_iff]
    exact sum_smul_mem _ _ fun i i_mem_l ↦ mem_span_of_mem <| mem_image_of_mem _ (l_subset_L' i_mem_l)
  · exact sum_smul_mem _ _ fun i i_mem_n ↦ mem_span_of_mem <| mem_image_of_mem _ (n_subset_N' i_mem_n)

[Kenny Lau]

nice, thanks!

[Kenny Lau]

i didn't know you can change the ring too

[Anthony Fernandes]

I tried like this to experiment with the library and apparently yes, however I had to make tau surjective in order to complete the proof

[Riccardo Brasca]

Can't you use the image as a submodule? f '' L' looks suspiciously "by hand"

[Riccardo Brasca]

Anyway we surely want this in mathlib, since it is strictly stronger than the above result

[Anthony Fernandes]

Riccardo Brasca said:

Can't you use the image as a submodule? f '' L' looks suspiciously "by hand"

L' is not a submodule I can't feed it into Submodule.map (it's not like Ideal.map that does span (f '' I))

[Riccardo Brasca]

Ah, it's the spanning set, ok.

[Riccardo Brasca]

Anyway it seems too much by hand, without using the API for finite modules, but I should just try and see if I came up with a shorter proof

[Anthony Fernandes]

It certainly is, I just vibed my way through the proof a stopped when it compiled

[Riccardo Brasca]

@Anthony Fernandes I had a look at your proof. I think you are making your life more complicated than needed by trying to prove directly the semilinear version of the statement. The best idea is in my opinion to reduce your theorem to the linear version, and prove the linear version (with only one ring) using the lemma above. Indeed mathematically this is very easy, all modules are R-modules (this is docs#RestrictScalars), exactness is preserved by restriction of scalars and to prove that M is finite over S it is enough to prove that it is finite over R. Now, N is finite over T and this implies that it is finite over R (since T is a quotient of R). I am not 100% sure all these results are in mathlib, but the should, and this is almost surely the mathlib way of proving the theorem.

[Riccardo Brasca]

If you want to PR this approach feel free to ask my review, and if you are confused by the math feel free to come to my office :)

[Kevin Buzzard]

Ha ha it's great that this Zulip offers such a personalised help experience :-)

[Ruben Van de Velde]

Now all I need to figure out is where Riccardo's office is :)

[Antoine Chambert-Loir]

It's very close to mine!