isIso_diag — Mathlib

English

If A is subterminal and has a binary product A × A, then the diagonal Δ_A: A → A × A is an isomorphism.

Русский

Если A подтерминален и существует бинарное произведение A × A, диагональный морфизм Δ_A: A → A × A является изоморфизмом.

LaTeX

$$\operatorname{IsSubterminal}(A) \land \operatorname{HasBinaryProduct}(A,A) \rightarrow \operatorname{IsIso}(\Delta_A)$$

Lean4

/-- If `A` is subterminal, its diagonal morphism is an isomorphism.
The converse of `isSubterminal_of_isIso_diag`.
-/
theorem isIso_diag (hA : IsSubterminal A) [HasBinaryProduct A A] : IsIso (diag A) :=
  ⟨⟨Limits.prod.fst,
      ⟨by simp, by
        rw [IsSubterminal.def] at hA
        cat_disch⟩⟩⟩

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