constructRightAdjoint — Mathlib

Lean4
/-- Construct the right adjoint to `L`, with object map `constructRightAdjointObj`. -/
noncomputable def constructRightAdjoint [∀ X : B, RegularMono (adj₁.unit.app X)] : B ⥤ C :=
  by
  refine Adjunction.rightAdjointOfEquiv (fun X Y => (constructRightAdjointEquiv L _ adj₁ adj₂ X Y).symm) ?_
  intro X Y Y' g h
  rw [constructRightAdjointEquiv_symm_apply, constructRightAdjointEquiv_symm_apply, Equiv.symm_apply_eq,
    Subtype.ext_iff]
  dsimp
  simp only [Adjunction.homEquiv_counit]
  erw [Fork.IsLimit.homIso_natural, Fork.IsLimit.homIso_natural]
  simp only [Fork.ofι_pt, Functor.map_comp, assoc, limit.cone_x]
  erw [adj₂.homEquiv_naturality_left, Equiv.rightInverse_symm]
  simp
Похожие утверждения