isWeaklyRegular_lTensor — Mathlib

English

If M is weakly regular and M2 is flat (or M2 is a flat R-module), then M2 ⊗R M is weakly regular with respect to the same index list rs.

Русский

Если M слабо регулярен, а M2 является плоским модулем над R, то M2 ⊗R M также слабо регулярен по тем же индексам rs.

LaTeX

$$$IsWeaklyRegular\\ M\\ rs \\Rightarrow IsWeaklyRegular\\ (M_2 \\otimes_R M)\\ rs$$$

Lean4

theorem isWeaklyRegular_lTensor [Module.Flat R M₂] {rs : List R} (h : IsWeaklyRegular M rs) :
    IsWeaklyRegular (M₂ ⊗[R] M) rs := by
  induction h with
  | nil N => exact nil R (M₂ ⊗[R] N)
  | @cons N _ _ r rs' h1 _ ih =>
    let e := tensorQuotSMulTopEquivQuotSMulTop r M₂ N
    exact ((e.isWeaklyRegular_congr rs').mp ih).cons (h1.lTensor M₂)

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