dedekind::category::IsQuotient Concept Reference

The categorical witness of a regular epimorphism q: A ↠ Q — the dual of IsSubobject. More...

Concept definition

template<typename Q, typename A>
concept dedekind::category::IsQuotient =  requires(Q q) {
  
  { q.q } -> IsArrow;
 
  
  { q.r } -> IsPredicate;
 
  
  typename Q::Domain;
  typename Q::Class;
  requires std::same_as<typename Q::Domain, A>;
 
  
  requires std::same_as<Dom<decltype(q.q)>, A>;
  requires std::same_as<Cod<decltype(q.q)>, typename Q::Class>;
 
  
  requires IsProduct<Dom<decltype(q.r)>, A, A>;
}

Detailed Description

The categorical witness of a regular epimorphism q: A ↠ Q — the dual of IsSubobject.

A quotient Q of A is given by:

• q.q : A ⟶⟶ Q::Class — the regular-epi projection onto equivalence classes (an IsArrow),
• q.r : A × A ⟶ Ω — the kernel relation (the co-classifier, dual to χ for IsSubobject), pinned as an IsPredicate whose domain is a product object IsProduct of A and A: two elements x, y ∈ A are equated by q iff r((x, y)) = True.

In a topos, just as every subobject is uniquely classified by a unary characteristic morphism χ : A → Ω (membership predicate), every regular-epi quotient is uniquely co-classified by its kernel relation r : A × A → Ω (binary equivalence predicate over a product object). This concept names the dual surface so downstream concepts ( IsCoequalizer in :image, future pushouts) can constrain the quotient leg of a colimit at the type level.

Symmetry with IsSubobject: where IsSubobject pins s.χ as an IsPredicate with Dom <χ> = A, IsQuotient pins q.q as an IsArrow with Dom<q> = A and Cod<q> = Q::Class, and q.r as an IsPredicate over a product domain IsProduct<Dom<r>, A, A>. Both members are proper morphisms (carrying Domain / Codomain typedefs) so they compose with the rest of the :category arrow machinery uniformly — raw callables won't satisfy this concept.

The structural shape pinned here is the operational signatures. The equivalence-relation laws on r (reflexivity, symmetry, transitivity) and the regular-epi universality of q (existence and uniqueness of the unique factoring map for any arrow that equates the kernel relation) are the engineer's honesty obligation, as for IsNNO and IsSubobject — C++ concepts can pin shape, not the $\forall$ in the universal property.

Template Parameters

Q	The Quotient Species (The "Quotient Body").
A	The Ambient Species (The "Source Space").