dedekind::category::IsPullback Concept Reference

The apex of a pullback square over the cospan f: X ⟶ Z, g: Y ⟶ Z: a subobject carrying the two projection legs π₁ ⟶ X, π₂ ⟶ Y. More...

Concept definition

template<typename P, typename F, typename G>
concept dedekind::category::IsPullback =  IsArrow<F> && IsArrow<G> && std::same_as<Cod<F>, Cod<G>> &&
                     IsSubobject<P, typename P::Domain> &&
                     requires(const P& p, typename P::Member m) {
                       
                       
                       
                       
                       
                       { p.π_1(m) } -> std::same_as<Dom<F>>;
                       { p.π_2(m) } -> std::same_as<Dom<G>>;
                     }

Detailed Description

The apex of a pullback square over the cospan f: X ⟶ Z, g: Y ⟶ Z: a subobject carrying the two projection legs π₁ ⟶ X, π₂ ⟶ Y.

A pullback of f: X ⟶ Z and g: Y ⟶ Z is an object P with legs π₁: P ⟶ X and π₂: P ⟶ Y making the square commute (f ∘ π₁ = g ∘ π₂), universal among such cones. This concept pins the structural shape (an apex subobject with the two legs), not the representation of the apex and not the universal property. Both of those are the engineer's-honesty obligation, exactly as for IsEqualizer / IsImageOf / IsNNO (C++ concepts reason about shape, not the ∀ that makes the cone terminal).

Note

Deliberately representation-agnostic (#881). The canonical apex is the fiber product X ×_Z Y, a subobject of the product X × Y with π₁/π₂ the pair projections (this is what the pullback factory below builds). But the same universal object appears in reduced presentations that are not subobjects of the product: the meet A ∩ B in Sub(U) is the pullback of the inclusions A ↪ U ↩ B with apex a subobject of U (legs the co-restrictions A∩B ↪ A, A∩B ↪ B); Codd's natural_join is the fiber product over a shared column. Requiring the apex to be the product (the earlier IsProduct<P::Domain, X, Y> clause) matched only the one canonical realization and rejected these; dropping it lets any apex that carries the two legs qualify, while the fiber-product apex still satisfies it (its π₁/π₂ are the legs).

Template Parameters

P	The candidate pullback apex (a Subobject carrying π₁, π₂).
F	The morphism f: X ⟶ Z.
G	The morphism g: Y ⟶ Z.