dedekind::category::IsSubobjectLattice Concept Reference

A type S is the carrier of a subobject lattice over S::Domain, with lattice structure induced pointwise from the classifier S::logic_species::Ω. More...

Concept definition

template<typename S, typename Meet std::bit_and<>, typename Join std::bit_or<>>
concept dedekind::category::IsSubobjectLattice =  requires(const S& a, const S& b) {
  
  typename S::Domain;
  typename S::logic_species;
  
  requires IsOckhamAlgebra<typename S::logic_species>;
  
  Meet{}(a, b);
  Join{}(a, b);
}

Detailed Description

A type S is the carrier of a subobject lattice over S::Domain, with lattice structure induced pointwise from the classifier S::logic_species::Ω.

The textbook content (#698 Slice 8): in a topos with subobject classifier Ω, the bijection

Sub(A) ≅ Hom(A, Ω) ≅ Ω^A

gives Sub(A) an automatic lattice structure for every A, inherited pointwise from the lattice structure on Ω. Direction is Ω → Sub(A); not the reverse without representability.

lattice__IsSubobjectLattice_Structural_Shape

IsSubobjectLattice checks the carrier's CT-vocabulary metadata plus the family-typed shape of meet / join / complement. The Form-chain row 1 (thin) ≤ relation is derivable from meet (see the derivability section below); the concept therefore doesn't need a separate subset_eq / operator<= clause or a carrier-side SubsetEqRel typedef.

The strength S inherits at higher rows is determined by L = S::logic_species:

• L = Boole → S participates in IsBooleanSubobjectLattice (below) — the Boolean refinement mirroring Diaconescu's classical-Ω direction.
• L = Kleene → S stays Heyting-only (the "tricky to decide" escape door, Slice 8 constructive collapse).

Complement is required unconditionally; its semantic strength (Boolean vs Kleene-involution-only) is established at the L-witness level via the parallel IsBooleanSubobjectLattice concept, not gated inside this concept's body.

lattice__IsSubobjectLattice_CT_Vocabulary

The concept body uses CT-vocabulary primitives: the carrier exposes Domain and logic_species typedefs, and free functions meet, join, complement exist with the right shape. Operator sugar (<=, &, |, !) lives in :sets as forwarders. Pierce-style stratification: abstract content in the body, set-theoretic hints in the defaults.

Template Parameters

S	The subobject carrier. Must expose Domain and logic_species typedefs (the latter satisfying IsOckhamAlgebra).