dedekind::category::IsSubobject Concept Reference

The categorical witness of a monomorphism ι: S ↣ A — a characteristic morphism χ: A → Ω together with its inclusion. More...

Concept definition

template<typename S, typename A>
concept dedekind::category::IsSubobject =  IsCharacteristic<S> && std::same_as<Dom<S>, A> &&
                      requires(S s, typename S::Member m) {
                        
                        { s.ι(m) } -> std::same_as<A>;
                      }

Detailed Description

The categorical witness of a monomorphism ι: S ↣ A — a characteristic morphism χ: A → Ω together with its inclusion.

Categorically a subobject is the characteristic morphism plus the inclusion, so IsSubobject refines IsCharacteristic definitionally (#850): IsCharacteristic (S is the χ arrow A → Ω), same_as<Dom, A> (the domain tie), and the inclusion { s.ι(m) } -> A.

topoi__IsSubobject_Codomain_Tagging

Every inhabitant declares ::Codomain: the Subobject wrapper re-exports its stored rule's codomain (logic_species::Ω), and the #607 std-range lifts (ambient_set) and image results all go through it. The #681 lesson still holds — no materialised χ value member: IsCharacteristic recognises χ by call shape (via LogicalMap), not a s.χ member — so requiring the ::Codomain typedef (not a value member) is compatible with it, and subsumes the earlier structural { s(a) } -> IsΩ check.

Template Parameters

S	The Subobject Species (The "Body").
A	The Ambient Species (The "Space").