coreflective' — Mathlib

English

Under the hypothesis that pointwise left Kan extensions exist for all F, the unit of the LanAdjunction is an isomorphism.

Русский

При условии существования точечных левых канонических расширений для всех F единица LanAdjunction является изоморфизмом.

LaTeX

$$$ \\forall F:\\, C \\to H,\\; \\operatorname{HasPointwiseLeftKanExtension} L F \\Rightarrow \\operatorname{IsIso}((L.\\mathrm{lanAdjunction} H).\\mathrm{unit}).$$$

Lean4

instance coreflective' [∀ (F : C ⥤ H), HasPointwiseLeftKanExtension L F] : IsIso (L.lanAdjunction H).unit := by
  apply NatIso.isIso_of_isIso_app _

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