instIsIsoAppUnitReflectorAdjunctionA

English

Same as 74845: the unit component at X.A is an isomorphism in the reflective setting.

Русский

То же, что и в 74845: компонент единицы в X.A в отражательном контексте является изоморфизмом.

LaTeX

$$$$\\text{IsIso}((\\mathrm{reflectorAdjunction } R).unit.app X.A)$$$$

Lean4

instance [Reflective R] (X : (reflectorAdjunction R).toMonad.Algebra) : IsIso ((reflectorAdjunction R).unit.app X.A) :=
  ⟨⟨X.a,
      ⟨X.unit, by
        dsimp only [Functor.id_obj]
        rw [← (reflectorAdjunction R).unit_naturality]
        dsimp only [Functor.comp_obj, Adjunction.toMonad_coe]
        rw [unit_obj_eq_map_unit, ← Functor.map_comp, ← Functor.map_comp]
        dsimp [X.unit]
        simpa using congrArg (fun t ↦ R.map ((reflector R).map t)) X.unit⟩⟩⟩

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