Lean4
/-- If `i` witnesses that `D` is a reflective subcategory and an exponential ideal, then `D` is
itself Cartesian closed.
To allow for better control of definitional equality, this construction
takes in an explicit choice of lift of the essential image of `i` to `D`, in the form of a functor
`l : i.EssImageSubcategory ⥤ D` and natural isomorphism `φ : l ⋙ i ≅ i.essImage.ι`. When
`l ⋙ i` is defeq to `i.essImage.ι`, images of exponential objects in `D` under `i` will be defeq
to the respective exponential objects in `C`. -/
def cartesianClosedOfReflective' (l : i.EssImageSubcategory ⥤ D) (φ : l ⋙ i ≅ i.essImage.ι) : CartesianClosed D where
closed := fun B =>
{ rightAdj := i.essImage.lift (i ⋙ exp (i.obj B)) (fun X ↦ ExponentialIdeal.exp_closed (i.obj_mem_essImage X) _) ⋙ l
adj :=
by
apply (exp.adjunction (i.obj B)).restrictFullyFaithful i.fullyFaithfulOfReflective i.fullyFaithfulOfReflective
· symm
refine NatIso.ofComponents (fun X => ?_) (fun f => ?_)
· haveI := Adjunction.rightAdjoint_preservesLimits.{0, 0} (reflectorAdjunction i)
apply asIso (prodComparison i B X)
· dsimp [asIso]
rw [prodComparison_natural_whiskerLeft]
·
exact
(i.essImage.liftCompιIso _ _).symm.trans <|
(Functor.isoWhiskerLeft _ φ.symm).trans (Functor.associator _ _ _).symm }
