dedekind::category::IsClosureOperator Concept Reference

Structural shape: C is a closure operator on a poset P — an arrow C : P → P that is idempotent (C(C(x)) = C(x)), monotone (x ≤ y ⇒ C(x) ≤ C(y)), and extensive (x ≤ C(x)) for all x. More...

Concept definition

template<typename C>
concept dedekind::category::IsClosureOperator =  IsArrow<C> && std::same_as<Dom<C>, Cod<C>>

Detailed Description

Structural shape: C is a closure operator on a poset P — an arrow C : P → P that is idempotent (C(C(x)) = C(x)), monotone (x ≤ y ⇒ C(x) ≤ C(y)), and extensive (x ≤ C(x)) for all x.

Every Galois connection induces a closure operator via g ∘ f (the round-trip on the source side). Example in arithmetic: for the ceiling/inclusion adjunction ⌈·⌉ ⊣ ι, the source-side round-trip ι ∘ ⌈·⌉ : ℝ → ℝ is the round-up-to-nearest-integer closure (extensive, monotone, and idempotent on (ℝ, ≤)). Dually, for the floor/inclusion adjunction ι ⊣ ⌊·⌋, the source-side round-trip ⌊·⌋ ∘ ι : ℤ → ℤ is a closure operator as well — indeed, the identity on ℤ. Note: embed_uint_sint_ ∘ abs is not a closure operator because it isn't monotone on (ℤ, ≤) (sign-folding inverts order on the negative fragment); the (embed_uint_sint_, abs) pair is a split mono / split epi rather than a Galois connection.

C++ concepts cannot quantify universally over P, so the three properties (idempotent / monotone / extensive) are the engineer's honesty obligation; the structural shape names the signature only (an IsArrow whose Domain equals its Codomain).