module finite if localizations are finite

Stream: Is there code for X?

[Christian Merten]

Do we have something like:

import Mathlib

theorem finite_ofLocalizationSpanTarget {R M : Type*} [CommRing R] [AddCommMonoid M]
    [Module R M] (t : Finset R) (ht : Ideal.span (t : Set R) = ⊤)
    (H : ∀ (g : t), Module.Finite (Localization.Away g.val)
      (LocalizedModule (Submonoid.powers g.val) M)) :
    Module.Finite R M := by
  sorry

Probably @Andrew Yang knows this?

[Andrew Yang]

We have docs#finite_ofLocalizationSpan, but I'm not sure how easy it is to massage it into this.

[Christian Merten]

Ah thanks, I was looking in RingTheory/RingHom/Finite.

[Christian Merten]

To mimic docs#finite_ofLocalizationSpan, I probably have to mimic docs#IsLocalization.finsetIntegerMultiple first.

[Andrew Yang]

Yeah we should move them into RingTheory/RingHom/Finite.

[Andrew Yang]

It should follow easily once the localisation refactors land, but currently they are a performance hazard and I've yet to try all the suggestions by Matthew.

[Christian Merten]

Andrew Yang said:

It should follow easily once the localisation refactors land, but currently they are a performance hazard and I've yet to try all the suggestions by Matthew.

To unxy: This is the last step to show that finite presentation is a local ring hom property. So I think I'll try to finish it for the time being.

[Andrew Yang]

Sounds good!
In case it wasn't clear, that comment wasn't meant to block new development, and instead just another reason for me to resume the refactor work.