dedekind::category::IsForgetfulFunctor Concept Reference

Directional alias: U is the right adjoint of an adjunction F ⊣ U. Names the forgetful direction — U drops the structure that distinguishes 𝒞 from 𝒟 (e.g., U_Ring→Rig forgets that you can do −). More...

Concept definition

template<typename U, typename F>
concept dedekind::category::IsForgetfulFunctor =  HasAdjunctionShape<F, U>

Detailed Description

Directional alias: U is the right adjoint of an adjunction F ⊣ U. Names the forgetful direction — U drops the structure that distinguishes 𝒞 from 𝒟 (e.g., U_Ring→Rig forgets that you can do −).

Concrete sense: U : Ring → Rig sends a ring to its underlying rig; the adjunction with the Grothendieck-group free functor recovers F(R) as "the smallest ring containing R as a sub-rig".