reflects_cocone_isomorphism — Mathlib

English

In the left-op construction, the ι-component of the cocone corresponds to the opposite of the original cone’s projection in the opposite category.

Русский

В конструкции leftOp компонент ι кофана соответствует противоположности проекции исходного конуса в противоположной категории.

LaTeX

$$$$ (\mathrm{coconeOfConeLeftOp}\, c).\iota_{j} = (c.\pi_{\mathrm{app}(\mathrm{op}\, j)})^{\mathrm{op}} $$$$

Lean4

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

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