tensorProduct — Mathlib

English

If R is a commutative semiring, A is a semiring with an R-algebra structure, and M,N are modules with M finite, then M ⊗R N is finite over R; in particular, tensoring preserves finiteness.

Русский

Если R коммутативно, A — R-алгебра, и M,N — модули с конечной базой, то M ⊗R N конечен над R; тензорное произведение сохраняет конечность.

LaTeX

$$$\text{Module.Finite } R (\,M \otimes_R N\,)$$$

Lean4

instance tensorProduct [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N]
    [hM : Module.Finite R M] [hN : Module.Finite R N] : Module.Finite R (TensorProduct R M N) where
  fg_top := (TensorProduct.map₂_mk_top_top_eq_top R M N).subst (hM.fg_top.map₂ _ hN.fg_top)

Похожие утверждения