isSubterminal_of_isIso_diag — Mathlib

English

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

Русский

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

LaTeX

$$HasBinaryProduct(A,A) ∧ IsIso(Δ_A) ⇒ IsSubterminal(A)$$

Lean4

/-- If the diagonal morphism of `A` is an isomorphism, then it is subterminal.
The converse of `isSubterminal.isIso_diag`.
-/
theorem isSubterminal_of_isIso_diag [HasBinaryProduct A A] [IsIso (diag A)] : IsSubterminal A := fun Z f g =>
  by
  have : (Limits.prod.fst : A ⨯ A ⟶ _) = Limits.prod.snd := by simp [← cancel_epi (diag A)]
  rw [← prod.lift_fst f g, this, prod.lift_snd]

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