instIsIsoAppCounitRanAdjunctionOfHasPointwiseRightKanExtension

English

The counit of the ran adjunction is an isomorphism under pointwise right Kan extension assumptions.

Русский

С учетом предположений о правом каноническом расширении правого типа, counit ран-адъюнкции является изоморфизмом.

LaTeX

$$$ \\operatorname{IsIso}((L.ranAdjunction H).counit)$ under the assumptions.$$

Lean4

instance (F : C ⥤ H) [HasPointwiseRightKanExtension L F] [∀ (F : C ⥤ H), HasRightKanExtension L F] :
    IsIso ((L.ranAdjunction H).counit.app F) :=
  by
  rw [ranAdjunction_counit]
  infer_instance

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