Loading...
Searching...
No Matches
involution.cppm File Reference
module dedekind.category
Involution — a direction-reversal that is its own inverse — the atomic shape behind the dagger of a \(\dagger\)-category. More...
#include <algorithm>#include <compare>#include <concepts>#include <cstddef>#include <functional>#include <iterator>#include <ranges>#include <string>#include <type_traits>#include <utility>#include <vector>import dedekind.category:species;
Include dependency graph for involution.cppm:
Classes | |
| struct | dedekind::category::is_involutive< F, T > |
Trait: a callable F is involutive on T iff F(F(x)) = x for all x ∈ T. Primary is std::false_type; opt-in via specialisation or member discovery (mirrors is_reflexive / is_transitive export pattern). It is the CERTIFICATE the shape cannot supply: F² = Id is a claim about F, not a syntactic property of its call. More... | |
| struct | dedekind::category::is_involutive< F, T > |
Discovery: a type may opt in via a nested is_involutive_v template member. More... | |
| struct | dedekind::category::is_involutive< std::logical_not< bool >, bool > |
Canonical: std::logical_not<bool> is the involution on bool. More... | |
| struct | dedekind::category::is_involutive< std::bit_not< T >, T > |
Canonical: std::bit_not<T> is the involution on non-bool integral T (~~x = x). bool is EXCLUDED: ~x promotes to int (−1/−2) then converts back to true, so bit_not is not an involution on bool — its involution is std::logical_not. More... | |
| struct | dedekind::category::is_involutive< std::negate< T >, T > |
Canonical: unary minus is an involution on the unsigned integral carriers, where -x is 2^n - x and -(-x) = x for every x. The signed carriers are EXCLUDED: -INT_MIN is undefined behaviour, so std::negate<int> is an involution on all values but one, and that one makes it not a function. (The Jlt paper's Listing 1 states both.). More... | |
| struct | dedekind::category::Reverse |
An involution on a carrier that is not a number: reversing a word twice is the identity, on any word a value holds, a std::string or a std::vector of letters; not a view, whose copy would alias the caller's letters. A pure function object, value in and value out, so that it is an arrow in the sense of the Jlt paper's Rule 1, and a family of them, one per word type, as std::logical_not is one per truth type; endo<W>(rev) names the domain. More... | |
| struct | dedekind::category::is_involutive< Reverse, W > |
| struct | dedekind::category::is_involutive< Reverse, std::strong_ordering > |
| struct | dedekind::category::is_involutive< Identity< T >, T > |
The identity arrow is (trivially) an involution: id(id(x)) = x, so id⁻¹ = id. Identity is the degenerate case where idempotent (f²=f), involution (f²=id) and isomorphism coincide — the unique arrow with f²=f=id. Witnessed here so the compiler / cata can SEE it: the composition unit law (id∘f=f) subsumes it in practice, but a downstream inverse-cancellation rule (f∘f⁻¹→id, of which neg∘neg→id is the non-trivial case) needs id certified as the trivial member. More... | |
| struct | dedekind::category::is_involutive< Compose< F, G >, T > |
A composite of two commuting involutions is one, certified at the type where both legs are: \((g f)^2 = g g f f = \mathrm{id}\). The same law is_involution reads on a value ( | |
| struct | dedekind::category::is_involutive< Morphism< A, A, Impl >, A > |
The arrow wrapping a callable has the law iff the callable does: endo<A>(f) is an involution when f is. More... | |
| struct | dedekind::category::is_self_inverse< F > |
An involution is its own inverse: \(f \circ f = \mathrm{id}\) makes f an IsIsomorphism, through the f lives), with no inverse of its own. The hooks for a specific arrow (Identity, the negate Morphism) are more specialised and keep precedence. More... | |
| struct | dedekind::category::detail_involution::Reversed< Op > |
Op with its arguments exchanged, \(a \cdot^{op} b = b \cdot
a\). More... | |
| struct | dedekind::category::detail_involution::opposite< Op > |
| struct | dedekind::category::detail_involution::opposite< Reversed< Op > > |
| struct | dedekind::category::is_associative< T, detail_involution::Reversed< Op > > |
| struct | dedekind::category::is_commutative< T, detail_involution::Reversed< Op > > |
| struct | dedekind::category::is_idempotent< T, detail_involution::Reversed< Op > > |
| struct | dedekind::category::unit_trait< T, detail_involution::Reversed< Op > > |
| struct | dedekind::category::is_homomorphism< F, T, Op, detail_involution::Reversed< Op2 > > |
| Over a commutative operation on the codomain, a homomorphism into it is one into its opposite: \(b \cdot a = a \cdot b\) there. More... | |
| struct | dedekind::category::is_homomorphism< Morphism< A, B, Impl >, A, Op, detail_involution::Reversed< Op2 > > |
| The arrow wrapping a callable reverses an operation where the callable does, declared or derived: the meeting of the two rules above, more specialised than either, so that they never both apply. More... | |
Namespaces | |
| namespace | dedekind::category |
| namespace | dedekind::category::detail_involution |
An involution is an endomorphism once read on its object: the implication holds of the lifted arrow, endo<T>(f), and not of a bare callable such as std::logical_not<bool>, which is a family of arrows, one per type, and no IsArrow until endo names its domain. | |
Concepts | |
| concept | dedekind::category::IsInvolution |
Stated in arrow language: F is an endomorphism on the object T (IsEndomorphism, domain and codomain T — applying it twice returns to the domain) carrying the certificate \(f \circ f = \mathrm{id}_T\). T defaults to the arrow's domain; a bare callable names it. The object may be presented by many types (morphism__Objects_And_Their_Presentations), so the complement on \(\mathrm{Sub}(T)\) is an involution here, through this one concept. | |
| concept | dedekind::category::IsAntiHomomorphism |
A map on T that reverses Op, \(f(a \cdot b) = f(b) \cdot
f(a)\): a homomorphism into the opposite, Opposite<Op>, read off the homomorphism certificate rather than declared apart. | |
| concept | dedekind::category::IsDagger |
The \(\dagger\)-category surface built on IsInvolution: IsDagger, the named intermediate IsIsometry, and IsUnitary — where "the converse is the inverse" (bijective relation) and "the
transpose is the inverse" (orthogonal matrix) are one theorem. | |
| concept | dedekind::category::IsIsometry |
A singleton morphism-carrier F (its default value is the arrow) whose dagger is a left inverse: the named non-linear intermediate (Heunen & Vicary). For a value-level carrier, use the is_isometry predicate instead. | |
| concept | dedekind::category::IsUnitary |
A singleton morphism-carrier whose dagger is its inverse (isometry and coisometry) — a dagger-iso, \(f^\dagger = f^{-1}\). Hence an IsIsomorphism once lifted into the arrow surface (follow-up). | |
Typedefs | |
| template<typename F, typename T> | |
| using | dedekind::category::detail_involution::on_t |
F read as an arrow on the object T: itself when it is one; a bare callable (std::logical_not, a logic's RFL) as the endomorphism endo<T>(f) ( | |
| template<std::semiregular Op> | |
| using | dedekind::category::Opposite = typename detail_involution::opposite<Op>::type |
The opposite operation, \(a \cdot^{op} b = b \cdot a\), the product of the opposite monoid \(M^{op}\) (Mac Lane, Categories for the Working Mathematician, II.2), an involution on operations: Opposite<Opposite<Op>> is Op, the same type. A left action of \(M\) is a right action of \(M^{op}\), so a left action folded along a walk acts by the product in \(M^{op}\). The laws read backwards are the laws: associativity, the unit, commutativity and idempotence carry over, declared once here, and totality in | |
Functions | |
| template<typename Dagger, typename Op, typename T> requires std::equality_comparable<T> && requires(const T& g) { Op{}(Dagger{}(g), g); unit<T>(Op{}); } | |
| constexpr bool | dedekind::category::is_isometry (const T &f) |
CRUCIAL (load-bearing across the library): "the converse @b is the
inverse" — unitarity — is a property of an arrow (a value), not of a type. This is why the retired is_unitary certificate was wrong, and why the surface below is two coordinated forms of one computed law. | |
|
template<typename Dagger, typename Op, typename T> requires std::equality_comparable<T> && requires(const T& g) { Op{}(g, Dagger{}(g)); unit<T>(Op{}); } | |
| constexpr bool | dedekind::category::is_coisometry (const T &f) |
| The coisometry law: \(f \circ f^\dagger = \mathrm{id}\) — the dagger is a right inverse. | |
| template<typename Dagger, typename Op, typename T> | |
| constexpr bool | dedekind::category::is_unitary (const T &f) |
The unitary law: isometry and coisometry, hence \(f^\dagger = f^{-1}\) (a dagger-iso). Generalises the permutation's P° ; P = Δ check: the one predicate reads as "the converse is the
inverse" (bijection, Mat(𝔹)), "the transpose is the inverse" (orthogonal, Mat(ℝ)) and "the adjoint is the inverse" (unitary, Mat(ℂ)) — the real / complex face of the same law. | |
Variables | |
| template<typename F, typename T> | |
| constexpr bool | dedekind::category::is_involutive_v = is_involutive<F, T>::value |
| constexpr Reverse | dedekind::category::rev {} |
| The reversal: of a word's positions, \(i \mapsto n - 1 - i\), the symmetry of a palindrome, and of a comparison. | |
| constexpr auto | dedekind::category::detail_involution::neg = endo<std::size_t>(std::negate<std::size_t>{}) |
| constexpr auto | dedekind::category::detail_involution::flip = endo<std::size_t>(std::bit_not<std::size_t>{}) |
| constexpr auto | dedekind::category::detail_involution::not_bool = endo<bool>(std::logical_not<bool>{}) |
| constexpr auto | dedekind::category::detail_involution::not_not = not_bool >> not_bool |
| constexpr auto | dedekind::category::detail_involution::flip_neg |
Detailed Description
Involution — a direction-reversal that is its own inverse — the atomic shape behind the dagger of a \(\dagger\)-category.
@partition :involution
- Copyright
- 2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.
involution__The_Notion
An involution is an endomap \(f : T \to T\) that undoes itself: \(f \circ f = \mathrm{id}_T\). It is the mildest form of "reversibility": weaker than a group inverse (no second operand), and the shape shared by complement (!!x = x), negation (--x = x), transpose ( \((A^{\top})^{\top} = A\)), conjugation, and the converse of a relation ( \(R^{\smile\smile} = R\)).
involution__What_Lives_Here
This partition grew from an atomic seed into the \(\dagger\)-category surface. It is the extraction target flagged by :lattice's Involutive_Endofunctor (an involution at the functor level, \(F^2 \cong \mathrm{Id}\)) and the home for a notion the library keeps re-discovering under different names — in each the dagger \(\dagger\) coincides with the inverse exactly on the "good" arrows:
- Rel: dagger = converse \(R^{\smile}\); \(R^{\smile}=R^{-1}\) iff
Ris a bijection. - real inner-product spaces: dagger = transpose \(Q^{\top}\); \(Q^{\top}=Q^{-1}\) iff
Qis orthogonal. - complex Hilbert spaces: dagger = conjugate-transpose \(Q^{*}\); \(Q^{*}=Q^{-1}\) iff
Qis unitary. - a Boolean subobject lattice: dagger = complement \(\neg\) (self-dual).
Below the dagger, the involution on operations: Opposite<Op>, the product of the opposite monoid, \(a \cdot^{op} b = b \cdot a\). A dagger is an involutive map into it, \((f\,g)^\dagger = g^\dagger f^\dagger\).
The unifying statement — an arrow in a \(\dagger\)-category whose dagger is its inverse (a unitary / dagger-iso) — makes "the converse is the
inverse" (bijective relation) and "the transpose is the inverse" (orthogonal matrix) one theorem. That surface is now built here: IsInvolution (the atom), IsDagger, the computed is_isometry / is_coisometry / is_unitary predicates, and the IsIsometry / IsUnitary concepts — with the linear-algebra consumer (TransposeF over Mat(S)) as the first witness. Still a follow-up (#787): the default inverse from the dagger (so an orthogonal matrix / bijective relation gets inverse for free) and the migration of Involutive_Endofunctor, which need the :morphism arrow surface.
@build_order imports :species (unit_v); upstream of :lattice / :category.
- See also
- #275 nLab algebra/category hierarchy (work in progress): the multi-object dagger.
