English
Finiteness is transitive along scalar towers: if R → A and A → M with M finite over A and A finite over R then M is finite over R.
Русский
Финитность переносится по каскадам скаляров: если R→A и A→M, и M конечен над A, а A конечен над R, то M конечен над R.
LaTeX
$$$\\forall R\\, A\\, M\\; [\\text{Semiring } R][\\text{Semiring } A][\\text{Module } A M]\\ [\\text{IsScalarTower } R A M]\\ [Module.Finite R A]\\ [Module.Finite A M]\\; \\Rightarrow\\; Module.Finite R M$$
Lean4
theorem trans {R : Type*} (A M : Type*) [Semiring R] [Semiring A] [Module R A] [AddCommMonoid M] [Module R M]
[Module A M] [IsScalarTower R A M] : ∀ [Module.Finite R A] [Module.Finite A M], Module.Finite R M
| ⟨⟨s, hs⟩⟩, ⟨⟨t, ht⟩⟩ =>
⟨Submodule.fg_def.2
⟨Set.image2 (· • ·) (↑s : Set A) (↑t : Set M), Set.Finite.image2 _ s.finite_toSet t.finite_toSet, by
rw [Set.image2_smul, Submodule.span_smul_of_span_eq_top hs (↑t : Set M), ht, Submodule.restrictScalars_top]⟩⟩
