solutionSetCondition_of_isRightAdjoint

English

If G is a right adjoint, then G satisfies the solution set condition.

Русский

Если G является правой сопряженной, то она удовлетворяет условию решения множества.

LaTeX

$$$G\text{.IsRightAdjoint} \Rightarrow \text{SolutionSetCondition}(G)$$$

Lean4

/-- If `G : D ⥤ C` is a right adjoint it satisfies the solution set condition. -/
theorem solutionSetCondition_of_isRightAdjoint [G.IsRightAdjoint] : SolutionSetCondition G :=
  by
  intro A
  refine ⟨PUnit, fun _ => G.leftAdjoint.obj A, fun _ => (Adjunction.ofIsRightAdjoint G).unit.app A, ?_⟩
  intro B h
  refine ⟨PUnit.unit, ((Adjunction.ofIsRightAdjoint G).homEquiv _ _).symm h, ?_⟩
  rw [← Adjunction.homEquiv_unit, Equiv.apply_symm_apply]

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