dedekind::category::IsDagger Concept Reference

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. More...

Concept definition

template<typename Dagger, typename T, typename Op>
concept dedekind::category::IsDagger =  IsInvolution<Dagger, T> && IsAntiHomomorphism<Dagger, T, Op>

Detailed Description

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.

involution__Dagger_Category

A \(\dagger\)-category equips every arrow with a direction-reversal \(f^\dagger\) (a contravariant, identity-on-objects, involutive functor). An arrow is unitary (a dagger-iso) when its dagger is its inverse, \(f^\dagger = f^{-1}\). That one law instantiates as:

• Rel: dagger = converse; unitary ⟺ the relation is a bijection.
• real inner-product spaces: dagger = transpose; unitary ⟺ orthogonal ( \(Q^{\top} = Q^{-1}\)).
• complex Hilbert spaces: dagger = conjugate-transpose; unitary ⟺ the usual unitary matrix. The two CRUCIAL findings the surface encodes — unitarity is a value property (not a type trait), and the dagger is the first bridge to the mono / epi / iso factorisation surface — are documented at the concepts below.

A dagger on the arrows T of one object, composed by Op: an involution, \(f^{\dagger\dagger} = f\), that reverses composition, \((f\,g)^\dagger = g^\dagger f^\dagger\). A refinement of IsInvolution, its certificate inherited, and of IsAntiHomomorphism, a homomorphism into Opposite<Op>: the ring theorist's involution, an involutive anti-automorphism. The unit comes for free, since a bijective anti-homomorphism carries the unit to the unit. The one-object case: in general a dagger's component is an arrow \(\mathrm{Hom}(A, B) \to \mathrm{Hom}(B, A)\), an isomorphism with the component at \((B, A)\) as its inverse, and the involution is its diagonal (#787).

Note

Discussed and postponed (2026-10-30): the multi-object dagger, a refinement of IsIsomorphism with this involution as its diagonal. A matrix transpose is still a matrix, but off the diagonal not of the same type: an \(N \times M\) matrix transposes to an \(M \times N\) one, and a transposed tensor has its dimension order changed. The tree's daggers are all on square carriers, so the one-object case covers them for now.

Contravariance depends on the pair (T, Op): the transpose reverses matrix multiplication only over a commutative scalar ⊗, \((A B)^{\top}_{ij}=\sum_k A_{jk} B_{ki}\) while \((B^{\top}A^{\top})_{ij}=\sum_k B_{ki} A_{jk}\); over a noncommutative semiring it is still an involution but no dagger, which is the conjugate-transpose against the scalar anti-involution.

Template Parameters

Dagger	the dagger.
T	the arrows.
Op	their composition.