dedekind::category::IsLatticeCategory Concept Reference

A posetal category that is both filtered and cofiltered, with joins and meets given by the algebraic lattice operations. More...

Concept definition

template<typename T, typename Rel std::less_equal<T>, typename Join Sup, typename Meet Inf, typename L Boole>
concept dedekind::category::IsLatticeCategory = 
    IsPosetal<T, Rel, L> &&           
    IsFilteredCategory<T, Rel, L> &&  
    requires {
      
      requires is_codirected_v<T, Rel>;
    } &&
    
    IsOrderLatticeOperations<T, Join, Meet>

Detailed Description

A posetal category that is both filtered and cofiltered, with joins and meets given by the algebraic lattice operations.

The Form-witness for row 4 of the lattice Form-chain (#698). Binds:

• the top-down categorical content (thin + antisymmetric + filtered + cofiltered);
• the bottom-up algebraic content (IsOrderLatticeOperations: join / meet operations satisfying commutativity, associativity, idempotence, and absorption).

Both presentations describe the same Form; every carrier satisfying IsLatticeCategory participates in both.

Faithful inclusions encoded definitionally:

IsLatticeCategory ⊊ IsFilteredCategory ⊊ IsThinCategory IsLatticeCategory ⊊ IsPosetal ⊊ IsThinCategory

(Filtered and posetal are parallel branches above thin; lattice conjoins them and adds cofiltered + the algebraic join/meet existence.)

Template Parameters

T	The Domain (Objects).
Rel	The Relation (the unique-morphism witness).
Join	The join operation (default Sup).
Meet	The meet operation (default Inf).
L	The Logic Species (the Subobject Classifier Ω).