The adjunction law \(f(x) \le y \iff x \le g(y)\) as an opt-in leaf fact, with the one theorem derived here: a monotone isomorphism is adjoint to its inverse ( \(f(x) \le y \iff x \le f^{-1}(y)\), both legs monotone). Other adjunctions register their fact where their theorem is stated (Δ ⊣ ∧ per glb in :cartesian_bicategory, S ⊣ P on the saturating ℤ in numbers:integer, the antitone involution's self-adjunction in algebra:ordered_algebra).
More...
Detailed Description
struct dedekind::category::is_adjoint< F, G, Op >
The adjunction law \(f(x) \le y \iff x \le g(y)\) as an opt-in leaf fact, with the one theorem derived here: a monotone isomorphism is adjoint to its inverse ( \(f(x) \le y \iff x \le f^{-1}(y)\), both legs monotone). Other adjunctions register their fact where their theorem is stated (Δ ⊣ ∧ per glb in :cartesian_bicategory, S ⊣ P on the saturating ℤ in numbers:integer, the antitone involution's self-adjunction in algebra:ordered_algebra).
- Template Parameters
-
F the left adjoint. G the right adjoint. Op the order.
The trait behind is_adjoint_v, a struct so that a downstream module states an adjunction for a whole arrow family at once — a theorem ( \(\exists_f \dashv f^{-1}\) for every \(f\)) as one partial specialisation on the family's pattern, where a variable-template partial specialisation would not fire across the module boundary.
The documentation for this struct was generated from the following file:
- src/main/modules/dedekind/category/adjunction.cppm
