isNoetherian_prod — Mathlib

English

If M and P are Noetherian, then their product M × P (as a module) is Noetherian.

Русский

Если M и P — Noetherian, то их произведение M × P (как модуль) тоже Noetherian.

LaTeX

$$$[IsNoetherian R M] \wedge [IsNoetherian R P] \Rightarrow IsNoetherian R (M \times P)$$$

Lean4

instance isNoetherian_prod [IsNoetherian R M] [IsNoetherian R P] : IsNoetherian R (M × P) :=
  ⟨fun s =>
    Submodule.fg_of_fg_map_of_fg_inf_ker (LinearMap.snd R M P) (noetherian _) <|
      have : s ⊓ LinearMap.ker (LinearMap.snd R M P) ≤ LinearMap.range (LinearMap.inl R M P) := fun x ⟨_, hx2⟩ =>
        ⟨x.1, Prod.ext rfl <| Eq.symm <| LinearMap.mem_ker.1 hx2⟩
      Submodule.map_comap_eq_self this ▸ (noetherian _).map _⟩

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