isWeaklyRegular_congr — Mathlib

English

If two modules M and M₂ are connected by an additive equivalence e that respects the action of corresponding ring elements as prescribed by a list correspondence as bs, then IsWeaklyRegular M as holds exactly when IsWeaklyRegular M₂ bs holds.

Русский

Пусть модули M и M₂ связаны добавочно-эквивариентной перестановкой e так, что для соответствующих элементов списков as, bs выполняется совместимость действия: ∀ x, e(r•x) = s•e(x). Тогда IsWeaklyRegular(M, as) эквивалентно IsWeaklyRegular(M₂, bs).

LaTeX

$$$\\forall e:\\, M \\simeq_+ M_2,\\; \\forall as\\; bs,\\;\\big(\\forall x, e(r\\cdot x) = s\\cdot e(x) \\text{ for corresponding } r,s \\big) \\Rightarrow IsWeaklyRegular(M, as) \\iff IsWeaklyRegular(M_2, bs)$$$

Lean4

theorem _root_.AddEquiv.isWeaklyRegular_congr {e : M ≃+ M₂} {as bs}
    (h : List.Forall₂ (fun (r : R) (s : S) => ∀ x, e (r • x) = s • e x) as bs) :
    IsWeaklyRegular M as ↔ IsWeaklyRegular M₂ bs :=
  by
  conv => congr <;> rw [isWeaklyRegular_iff_Fin]
  let e' i :
    (M ⧸ (Ideal.ofList (as.take i) • ⊤ : Submodule R M)) ≃+ M₂ ⧸ (Ideal.ofList (bs.take i) • ⊤ : Submodule S M₂) :=
    QuotientAddGroup.congr _ _ e <|
      AddHom.map_smul_top_toAddSubgroup_of_surjective e.surjective <| List.forall₂_take i h
  refine (finCongr h.length_eq).forall_congr @fun _ => (e' _).isSMulRegular_congr ?_
  exact (mkQ_surjective _).forall.mpr fun _ => congrArg (mkQ _) (h.get _ _ _)

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