isNoetherianObject_of_mono — Mathlib

English

If i: X → Y is mono and Y is Noetherian, then X is Noetherian.

Русский

Если i: X → Y моно и Y Нётеровский, тогда X — Нётеровский.

LaTeX

$$$\forall (i:X\to Y),\ Mono(i) \Rightarrow \text{IsNoetherianObject}(Y) \Rightarrow \text{IsNoetherianObject}(X).$$$

Lean4

theorem isNoetherianObject_of_mono (i : X ⟶ Y) [Mono i] [IsNoetherianObject Y] : IsNoetherianObject X :=
  by
  rw [isNoetherianObject_iff_monotone_chain_condition]
  intro f
  obtain ⟨n, hn⟩ := monotone_chain_condition_of_isNoetherianObject ⟨_, (Subobject.map i).monotone.comp f.2⟩
  exact ⟨n, fun m hm ↦ Subobject.map_obj_injective i (hn m hm)⟩

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