closed — Mathlib

Lean4
/-- Auxiliary definition for `monoidalClosed`. -/
noncomputable def closed (c : C) : Closed c
    where
  rightAdj := R ⋙ (ihom (R.obj c)) ⋙ L
  adj :=
    by
    refine
      ((ihom.adjunction (R.obj c)).comp adj).restrictFullyFaithful (FullyFaithful.ofFullyFaithful R)
        (FullyFaithful.id _) ?_ ?_
    · refine
        NatIso.ofComponents (fun _ ↦ (μIso L _ _).symm ≪≫ asIso ((adj.counit.app _) ⊗ₘ (adj.counit.app _))) (fun _ ↦ ?_)
      dsimp
      rw [Category.assoc, ← δ_natural_right_assoc, tensorHom_def', ← MonoidalCategory.whiskerLeft_comp_assoc,
        Adjunction.counit_naturality, whisker_exchange, tensorHom_def_assoc, MonoidalCategory.whiskerLeft_comp]
    · exact NatIso.ofComponents (fun _ ↦ asIso (adj.unit.app ((ihom _).obj _)))
Похожие утверждения