dedekind::category::IsGaloisConnection Concept Reference

Structural shape: F and G form a Galois connection F ⊣ G in a posetal setting — the simplest adjunction. Both are monotone arrows; F : P → Q and G : Q → P with the source/target carriers crossed (so F's Codomain matches G's Domain and vice versa). The universal-property test, for monotone legs More...

Concept definition

template<typename F, typename G, typename Op std::less_equal<>>
concept dedekind::category::IsGaloisConnection = 
    ((IsCovariantFunctor<F, Op> && IsCovariantFunctor<G, Op>) ||
     (IsContravariantFunctor<F, Op> && IsContravariantFunctor<G, Op>)) &&
    std::same_as<Dom<G>, Cod<F>> && std::same_as<Cod<G>, Dom<F>> &&
    is_adjoint_v<F, G, Op>

Detailed Description

Structural shape: F and G form a Galois connection F ⊣ G in a posetal setting — the simplest adjunction. Both are monotone arrows; F : P → Q and G : Q → P with the source/target carriers crossed (so F's Codomain matches G's Domain and vice versa). The universal-property test, for monotone legs

f(x) ≤ y ⟺ x ≤ g(y)

and for antitone legs, a polarity (the complement on subobjects, \(a \subseteq \neg b \iff b \subseteq \neg a\); \(-x\) on \(\mathbb{Z}\))

y ≤ f(x) ⟺ x ≤ g(y)

holds. These are laws of partial orders; on a finite chain an antitone bijection is the reversal, so its cycle type is known (#1133). C++ concepts cannot quantify universally over x and y, so the equivalence is the law leg is_adjoint_v: derived for a monotone isomorphism and its inverse, registered where its theorem is stated otherwise; the structural shape names the signatures.

Relationship to HasAdjunctionShape: a Galois connection is an adjunction in the simplest possible category-theoretic setting (posets). IsGaloisConnection is the order-theoretic specialisation — it doesn't require the full functor / natural-transformation machinery because in a poset there's at most one arrow between any two objects, so the naturality content trivialises. Useful as a lightweight vocabulary anchor for arithmetic-flavoured adjunctions (floor/ceiling, addition/subtraction, etc.).

P and Q are not free template parameters — they are recovered from F's Domain / Codomain. G's carriers are required to be the cross-pair: G : Q → P.

Note

Matched variance (#946). The legs must share variance: both monotone (the covariant Galois connection) or both antitone (the antitone dual), the defining shape of the adjoints. Mismatched polarity (a monotone F with an antitone G) is not a Galois connection, so a bare IsVariant<F> && IsVariant<G> gate (an earlier #946 review round) was too loose: it admitted the mismatch. IsMonotone / IsAntiMonotone each imply IsArrow, so the matched-variance disjunction below replaces the bare IsArrow gate. Safe to tighten upstream: the only IsGaloisConnection<F,G> instantiation in the tree is IsMeetAsRightAdjoint (:cartesian_bicategory, both legs monotone); the floor / ceil / ±k connections above are documentation-only, so no existing user is constrained. #908 would derive the variance structurally from each leg's injected op.

Threaded order (#950). The variance of both legs is queried against Op rather than a hard-coded std::less_equal<>. A connection in a non-default poset (e.g. the comonoid legs, whose shared P×P object carries the componentwise product order ≤×, not the lexicographic pair order) passes its own relation in; the default keeps the arithmetic examples above unchanged.

Template Parameters

F	the left adjoint.
G	the right adjoint.
Op	the order both legs' variance is tested against; defaults to std::less_equal<>.