cartesianClosedOfReflective — Mathlib

Lean4

/-- If `i` witnesses that `D` is a reflective subcategory and an exponential ideal, then `D` is
itself Cartesian closed.

Unlike `cartesianClosedOfReflective'` this construction lifts exponential objects in `C` to
exponential objects in `D` by applying the reflector to them, even though they already lie in the
essential image of `i`; if you need better control over definitional equality, use
`cartesianClosedOfReflective'` instead. -/
def cartesianClosedOfReflective : CartesianClosed D :=
  cartesianClosedOfReflective' i (i.essImage.ι ⋙ reflector i)
    (NatIso.ofComponents
      (fun X ↦
        have := Functor.essImage.unit_isIso X.2
        (asIso ((reflectorAdjunction i).unit.app X.obj)).symm))

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