instIsIsoPost_1 — Mathlib

English

There is an isomorphism Colimit.post F G, i.e., the canonical comparison morphism between the colimit of F and the image under G of that colimit is an isomorphism when F has a colimit and G preserves the relevant colimits.

Русский

Существует изоморфизм Colimit.post F G; каноническое отображение между колимитом F и образом этого колимита через G является изоморфизмом, когда у F есть колимит и G сохраняет соответствующие колимиты.

LaTeX

$$$\\operatorname{IsIso}(\\operatorname{colimit.post} F G)$$$

Lean4

instance : IsIso (colimit.post F G) :=
  show IsIso (preservesColimitIso G F).inv from inferInstance

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