proj_reflectsIsomorphisms — Mathlib

English

The projection functor from CostructuredArrow to C reflects isomorphisms: if its map is an isomorphism, then the original morphism is an isomorphism.

Русский

Проекция-функтор из CostructuredArrow в C отражает изоморфизмы: если образ под ним является изоморфизмом, то исходный морфизм тоже изоморфизм.

LaTeX

$$$ \forall A,B : \mathrm{CostructuredArrow}(S,T),\; \forall f: A \to B,\; IsIso((\mathrm{proj}(S,T)).map(f)) \Rightarrow IsIso(f). $$$

Lean4

instance proj_reflectsIsomorphisms : (proj S T).ReflectsIsomorphisms where
  reflects {Y Z} f
    t :=
    ⟨⟨CostructuredArrow.homMk (inv ((proj S T).map f)) (by rw [Functor.map_inv, IsIso.inv_comp_eq]; simp), by
        constructor <;> ext <;> dsimp at t ⊢ <;> simp⟩⟩

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