reflects_cone_isomorphism — Mathlib

English

If F reflects isomorphisms, then the functor Cones.functoriality(K, F) also reflects isomorphisms.

Русский

Если F отражает изоморфизмы, то и конусная функциональность Cones.functoriality(K, F) отражает изоморфизмы.

LaTeX

$$$\mathrm{ReflectsIsomorphisms}(F) \Rightarrow \mathrm{ReflectsIsomorphisms}(\mathrm{Cones.functoriality}(K,F))$$$

Lean4

/-- If `F` reflects isomorphisms, then `Cones.functoriality F` reflects isomorphisms
as well.
-/
instance reflects_cone_isomorphism (F : C ⥤ D) [F.ReflectsIsomorphisms] (K : J ⥤ C) :
    (Cones.functoriality K F).ReflectsIsomorphisms := by
  constructor
  intro A B f _
  haveI : IsIso (F.map f.hom) := (Cones.forget (K ⋙ F)).map_isIso ((Cones.functoriality K F).map f)
  haveI := ReflectsIsomorphisms.reflects F f.hom
  apply cone_iso_of_hom_iso

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