of_terminal — Mathlib

English

If a category has both an initial and a terminal object, and the unique arrow from the initial to the terminal is mono, then the category is an InitialMonoClass.

Русский

Если в категории есть как начальный, так и конечный объект, и единственная стрелка из начального в конечный моно, то категория является InitialMonoClass.

LaTeX

$$$$[HasInitial\\ C]\\,[HasTerminal\\ C]\\ (\\mathrm{Mono}(\\mathrm{initial.to}(\\top_C)))\\Rightarrow \\mathrm{InitialMonoClass}\\;C.$$$$

Lean4

/-- To show a category is an `InitialMonoClass` it suffices to show the unique morphism from the
initial object to a terminal object is a monomorphism. -/
theorem of_terminal [HasInitial C] [HasTerminal C] (h : Mono (initial.to (⊤_ C))) : InitialMonoClass C :=
  InitialMonoClass.of_isTerminal initialIsInitial terminalIsTerminal h

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