Lean4
/-- The adjunction `Γ ⊣ Spec` from `CommRingᵒᵖ` to `Scheme`. -/
def adjunction : Scheme.Γ.rightOp ⊣ Scheme.Spec.{u}
where
unit :=
{ app := fun X ↦ ⟨locallyRingedSpaceAdjunction.{u}.unit.app X.toLocallyRingedSpace⟩
naturality := fun _ _ f ↦ Scheme.Hom.ext' (locallyRingedSpaceAdjunction.{u}.unit.naturality f.toLRSHom) }
counit := (NatIso.op Scheme.SpecΓIdentity.{u}).inv
left_triangle_components Y := locallyRingedSpaceAdjunction.left_triangle_components Y.toLocallyRingedSpace
right_triangle_components R := Scheme.Hom.ext' <| locallyRingedSpaceAdjunction.right_triangle_components R