isQuotientMap_of_isColimit_cofork

English

If c is a colimit cofork, then the canonical projection c.π is a quotient map. In particular, the quotient topology on c.pt coincides with the final topology induced by π.

Русский

Если c является кофорком-колимитом, то каноническое отображение c.π является факторным (квотиентным) отображением. В частности, топология на c.pt совпадает с финальной топологией, индуцированной π.

LaTeX

$$IsQuotientMap c.π$$

Lean4

theorem isQuotientMap_of_isColimit_cofork (c : Cofork f g) (hc : IsColimit c) : IsQuotientMap c.π :=
  by
  rw [isQuotientMap_iff]
  constructor
  · simpa only [← epi_iff_surjective] using epi_of_isColimit_cofork hc
  · exact isOpen_iff_of_isColimit_cofork c hc

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