Directional alias: F is the left adjoint of an adjunction F ⊣ U. Names the free direction — F sends an object d : 𝒟 to its free construction F(d) : 𝒞 (the universal recipient under U). More...

Concept definition

template<typename F, typename U>

concept dedekind::category::IsFreeFunctor = HasAdjunctionShape<F, U>

dedekind::category::HasAdjunctionShape

Structural shape: F and U have the categorical signature of an adjoint pair F ⊣ U — F : 𝒟 → 𝒞 (left,...

Definition adjunction.cppm:122

dedekind::category::IsFreeFunctor

Directional alias: F is the left adjoint of an adjunction F ⊣ U. Names the free direction — F sends a...

Definition adjunction.cppm:143

Detailed Description

Directional alias: F is the left adjoint of an adjunction F ⊣ U. Names the free direction — F sends an object d : 𝒟 to its free construction F(d) : 𝒞 (the universal recipient under U).

Mathematical instances: free monoid (Set → Mon), Grothendieck group (CommMon → Ab), tensor algebra (Vect → Ring), free module / vector space, group ring, etc. In this codebase: the carrier-lattice steps ℕ → ℤ → ℚ → ℝ → ℂ are each a free construction in their respective category.