An arrow that is both a homomorphism of the signatures and surjective (via category::is_epic_arrow_v). More...

Concept definition

template<typename Arrow, typename S typename detail_universal::default_signatures<Arrow>::source, typename T typename detail_universal::default_signatures<Arrow>::target>
concept dedekind::algebra::IsQuotientMorphism = 
    IsHomomorphism<Arrow, S, T> && dedekind::category::IsSurjective<Arrow>

Detailed Description

An arrow that is both a homomorphism of the signatures and surjective (via category::is_epic_arrow_v).

Mathematically, the canonical quotient morphism π: A → A/~ is a surjective homomorphism: it preserves the operations and hits every element of the quotient algebra. This concept is the structural / syntactic gate for "declared homomorphism + declared surjectivity"; it does not verify that the arrow is the canonical projection of any particular congruence, nor that the quotient algebra has been constructed. It composes IsHomomorphism (above) and category::is_epic_arrow_v (in category:morphism, surfaced via the IsSurjective pedagogical synonym).

See also: Lang §III.1 (kernel-quotient-image factorisation, sometimes called the first isomorphism theorem).