proj_reflectsIsomorphisms — Mathlib

English

The projection functor from StructuredArrow reflects isomorphisms: if a morphism in StructuredArrow maps to an isomorphism under the projection, then the morphism is itself an isomorphism.

Русский

Функтор проекции из StructuredArrow отражает изоморфизмы: если морфизм в StructuredArrow отображается как изоморфизм через проекцию, то сам морфизм является изоморфизмом.

LaTeX

$$$ (\\mathrm{proj}\, S T).\\mathrm{map} f \\text{ isIso } \\Rightarrow f \\text{ isIso } $$$

Lean4

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

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