dedekind::category::WitnessesFirstIso Concept Reference

Connector witnesses the First Isomorphism Theorem at homomorphism F. More...

Concept definition

template<typename F, typename Connector>
concept dedekind::category::WitnessesFirstIso = 
    IsArrow<F> && IsIsomorphism<Connector> &&
    requires {
      typename kernel_quotient<F>::Class;
      typename image_carrier<F>::type;
    } &&
    std::same_as<typename Connector::Domain,
                 typename kernel_quotient<F>::Class> &&
    std::same_as<typename Connector::Codomain, typename image_carrier<F>::type>

Detailed Description

Connector witnesses the First Isomorphism Theorem at homomorphism F.

The typed shape of the theorem. A user-supplied Connector is accepted as a First-Iso witness iff

(i) it is an iso (IsIsomorphism<Connector>),

(ii) its Domain is exactly the registered kernel_quotient<F>::Class (the textbook quotient A/ker(F)),

(iii) its Codomain is exactly the registered image_carrier<F>::type (the textbook image im(F)).

A regression in any leg surfaces at compile time. In particular, hand-rolling an iso between unrelated types and claiming it witnesses First-Iso is not enough — the registered quotient and image must match.

Form-chain row 7 (paper-§3 crown) of #718.

Template Parameters

F	The homomorphism F : A → B.
Connector	Candidate iso A/ker(F) → im(F).