Span of a finite set over a finite ring

Stream: Is there code for X?

[Yaël Dillies]

Do we have that the span of a finite set over finite ring is finite? Alternatively, do we have that a module over a finite ring is finite-dimensional iff it is finite? I couldn't find either direction.

[Daniel Weber]

There's docs#FiniteDimensional.finite_of_finite for fields, I can't find it for rings

[Yaël Dillies]

Whoops sorry, my code block never sent. Here is my best attempt:

import Mathlib.RingTheory.Finiteness

variable {R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M}

/-- A finite module is finite-dimensional. -/
-- See note [lower instance priority]
instance (priority := 100) Module.Finite.of_finite [Finite M] : Module.Finite R M := by
  sorry

variable [Finite R]

/-- A module over a finite ring has finite dimension iff it is finite. -/
lemma Module.finite_iff_finite : Module.Finite R M ↔ Finite M := by
  refine ⟨fun _ ↦ ?_, fun _ ↦ .of_finite⟩
  · sorry

lemma Set.Finite.submoduleSpan (hs : s.Finite) : (Submodule.span R s : Set M).Finite := by
  lift s to Finset M using hs
  rw [Set.Finite, ← Module.finite_iff_finite (R := R)]
  dsimp
  infer_instance

[Yaël Dillies]

Daniel, well spotted. I'll try generalising it

[Yaël Dillies]

Ah! docs#Module.Finite.span_of_finite Nevermind

[Yaël Dillies]

#17707