instIsCoreflexivePairMapAppUnitOtherMap

English

If L ⋙ F has a right adjoint, F is comonadic, and C has coreflexive equalizers, then L has a right adjoint.

Русский

Если L ⋙ F имеет правое сопряжение, F комонатический, и C имеет ядра-кофакторизируемые пары, тогда L имеет правое сопряжение.

LaTeX

$$$$(L \\circ F) \\text{ имеет правое сопряжение} \\Rightarrow L \\text{ имеет правое сопряжение},$$ при условии комонодичности F.$$

Lean4

/-- `(U'Fη_X, otherMap X)` is a coreflexive pair: in particular if `C` has coreflexive equalizers
then this pair has an equalizer.
-/
instance (X : B) : IsCoreflexivePair (U'.map (F.map (adj₁.unit.app X))) (otherMap _ _ adj₁ adj₂ X) :=
  IsCoreflexivePair.mk' (U'.map (adj₁.counit.app (F.obj X))) (by simp [← Functor.map_comp])
    (by simp only [otherMap, assoc, ← Functor.map_comp]; simp)

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