instIsIsoInitialComparison — Mathlib

English

If G preserves initial objects, then the canonical comparison morphism initialComparison(G) : ⊥_D → G(⊥_C) is an isomorphism.

Русский

Если G сохраняет начальные объекты, то каноническое отображение initialComparison(G) : ⊥_D → G(⊥_C) является изоморфизмом.

LaTeX

$$$\mathrm{PreservesInitial}(G) \Rightarrow \IsIso(\mathrm{initialComparison}(G))$$$

Lean4

instance : IsIso (initialComparison G) := by
  rw [← PreservesInitial.iso_hom]
  infer_instance

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