isArtinianObject_of_mono — Mathlib

English

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

Русский

Если i: X → Y моно, и Y артинян, то X тоже артинян.

LaTeX

$$$(i: X\\to Y)$ моно and $\\mathrm{IsArtinianObject}(Y) \\Rightarrow \\mathrm{IsArtinianObject}(X)$$$

Lean4

theorem isArtinianObject_of_mono (i : X ⟶ Y) [Mono i] [IsArtinianObject Y] : IsArtinianObject X :=
  by
  rw [isArtinianObject_iff_antitone_chain_condition]
  intro f
  obtain ⟨n, hn⟩ :=
    antitone_chain_condition_of_isArtinianObject
      ⟨fun n ↦ (Subobject.map i).obj (f n), fun _ _ h ↦ (Subobject.map i).monotone (f.2 h)⟩
  exact ⟨n, fun m hm ↦ Subobject.map_obj_injective i (hn m hm)⟩

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