instContainsZeroIsNoetherianObjectOfHasZeroObject

English

If the category has a zero object, there is a zero subobject of any X that witnesses the Noetherian property; hence X is Noetherian.

Русский

Если в категории есть нулевой объект, существует нулевой подобъект X, который свидетельствует о свойстве Нётеровости; следовательно, X — нёйтеровский.

LaTeX

$$$\text{HasZeroObject}(\mathcal{C}) \Rightarrow \forall X, \text{IsNoetherianObject}(X).$$$

Lean4

instance [HasZeroObject C] : (isNoetherianObject (C := C)).ContainsZero where
  exists_zero :=
    ⟨0, isZero_zero _, by
      rw [← isNoetherianObject.is_iff]
      exact isNoetherianObject_of_isZero (isZero_zero C)⟩

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