dedekind::category::IsPushout Concept Reference

The categorical dual of IsPullback: the apex of a pushout square over the span f: Z ⟶ X, g: Z ⟶ Y, carrying the two coprojection colegs ι1: X ⟶ P, ι2: Y ⟶ P. More...

Concept definition

template<typename P, typename F, typename G>
concept dedekind::category::IsPushout =  IsArrow<F> && IsArrow<G> && std::same_as<Dom<F>, Dom<G>> &&
                    IsSubobject<P, typename P::Domain> &&
                    requires(const P& p, const Cod<F>& x, const Cod<G>& y) {
                      
                      
                      
                      
                      
                      
                      
                      { p.ι1(x) } -> std::same_as<typename P::Member>;
                      { p.ι2(y) } -> std::same_as<typename P::Member>;
                    }

Detailed Description

The categorical dual of IsPullback: the apex of a pushout square over the span f: Z ⟶ X, g: Z ⟶ Y, carrying the two coprojection colegs ι1: X ⟶ P, ι2: Y ⟶ P.

Every arrow of IsPullback is reversed. The cospan (shared Cod<F> = Cod<G>) becomes a span (shared Dom<F> = Dom<G>); the projection legs P ⟶ X, P ⟶ Y become coprojection colegs X ⟶ P, Y ⟶ P (so the apex exposes p.ι1(x), p.ι2(y) rather than p.π_1(m), p.π_2(m)). In the poset Sub(U) the pushout = coproduct = join (the least upper bound, taken over the initial object ∅), exactly dual to product = pullback = meet (the greatest lower bound, over the terminal U). So A | B is the pushout of the span A ← ∅ → B, with colegs A ↪ A∪B, B ↪ A∪B.

Structural shape only, exactly as IsPullback: commutativity and the ∀-universal property remain the engineer's-honesty obligation (C++ concepts reason about shape, not the ∀ that makes the cocone initial). #881.

Note

Scope: this is the Sub(U)-specific pushout, whose apex is a IsSubobject just as IsPullback's is. In a general category the strict dual of a mono (subobject) apex is an epi (quotient) apex, so a general colimit is not a subobject; category::IsQuotient (topoi.cppm) is the dual representation earmarked for that general pushout / colimit. Here the join A | B genuinely is a subobject of the ambient U (in the thin poset Sub(U) every object is a subobject of U), so the subobject-apex constraint is exact for this setting, not an over-restriction.

Template Parameters

P	The candidate pushout apex (a Sub(U) subobject carrying the colegs; the general colimit apex is a IsQuotient instead).
F	The span arrow f: Z ⟶ X.
G	The span arrow g: Z ⟶ Y.