instIsClosedUnderSubobjectsIsNoetherianObject

English

If Y is Noetherian and i: X → Y is mono, then X is Noetherian; equivalently Noetherian objects are closed under taking subobjects.

Русский

Если Y Нётеровский и i: X → Y моно, то X Нётеровский; то есть Нётеровость сохраняется при взятий подобъектов.

LaTeX

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

Lean4

instance : (isNoetherianObject (C := C)).IsClosedUnderSubobjects where
  prop_of_mono f _
    hY := by
    rw [← isNoetherianObject.is_iff] at hY ⊢
    exact isNoetherianObject_of_mono f

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