isWeaklyRegular_map_algebraMap_iff

English

If M is an R-module and S is an algebra over R, then IsWeaklyRegular M (rs.map (algebraMap R S)) iff IsWeaklyRegular M rs.

Русский

Пусть M — модуль над R, а S алгебра над R. Тогда IsWeaklyRegular M (rs.map (algebraMap R S)) эквивалентно IsWeaklyRegular M rs.

LaTeX

$$$IsWeaklyRegular(M, \\mathrm{map}(\\mathrm{algebraMap}_{R}^{S})(rs)) \\iff IsWeaklyRegular(M, rs)$$$

Lean4

theorem isWeaklyRegular_map_algebraMap_iff [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup M] [Module R M]
    [Module S M] [IsScalarTower R S M] (rs : List R) :
    IsWeaklyRegular M (rs.map (algebraMap R S)) ↔ IsWeaklyRegular M rs :=
  (AddEquiv.refl M).isWeaklyRegular_congr <|
    List.forall₂_map_left_iff.mpr <| List.forall₂_same.mpr fun r _ => algebraMap_smul S r

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