English
For a ring homomorphism f: α →+* β, the codomain is trivial (0 = 1) if and only if the range of f is the singleton {0}. In particular, if the codomain is trivial, then every image is 0, and conversely, if the image is {0}, then the codomain is constrained to be trivial.
Русский
Для гомоморфизма кольца f: α →+* β кодомонада тривиальна (0 = 1) тогда и только тогда, когда образ f равен единице {0}. Другими словами, если кодомонада тривиальна, то все значения образа равны нулю; и наоборот, если образ равен {0}, кодомонада тривиальна.
LaTeX
$$$\bigl(0_β = 1_β\bigr) \;\Longleftrightarrow\; \operatorname{range}(f) = \{0\}. $$$
Lean4
/-- `f : α →+* β` has a trivial codomain iff its range is `{0}`. -/
@[deprecated "Use range_eq_singleton_iff and codomain_trivial_iff_range_trivial" (since := "2025-06-09")]
theorem codomain_trivial_iff_range_eq_singleton_zero : (0 : β) = 1 ↔ Set.range f = {0} :=
f.codomain_trivial_iff_range_trivial.trans
⟨fun h => Set.ext fun y => ⟨fun ⟨x, hx⟩ => by simp [← hx, h x], fun hy => ⟨0, by simpa using hy.symm⟩⟩, fun h x =>
Set.mem_singleton_iff.mp (h ▸ Set.mem_range_self x)⟩
