Concept Classes and Kernel Relations

Abstract

Effective concept classes are dual to source equivalence relations.

Theorem 1.1 (Effective concept classes are order-dual to kernel relations).

$$\begin{array}{c}\forall X:\mathrm{Type},\\ \mathrm{Bijective}(\mathrm{conceptClassKernel}(X))\wedge \\ (\forall C,D\in \mathrm{EffectiveConcept}(X),\mathrm{Refines}(q_C,q_D)⟺\ker (q_D)\subseteq \ker (q_C))\wedge \\ (\forall q_C,q_D,\ker (\mathrm{conceptJoin}(q_C,q_D))=\mathrm{intersection}(\ker (q_C),\ker (q_D)))\wedge \\ (\forall q_C,q_D,\ker (\mathrm{commonCoarsening}(q_C,q_D))=\mathrm{EqvClosure}(\mathrm{union}(\ker (q_C),\ker (q_D)))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Refinement/ConceptKernelOrderDuality.concept_kernel_order_duality (✓ std3). ∎

Source. Repository-derived.

Commentary.

An effective concept presentation consists of a readout together with surjectivity onto its coordinate carrier. Mutual refinement is the antisymmetrization of the canonical factor-map preorder.

The kernel map sends each resulting concept class to the equality relation induced on its source. It is publicly bijective, and a coarse concept refines through a finer one exactly when the finer kernel is contained in the coarse kernel.

The final two public conjuncts use the canonical family join and the quotient projection for common coarsening. Their kernels are, respectively, the relation intersection and the equivalence closure of the relation union.

The proof directly applies the pinned antisymmetrization and setoid lattice constructions. Surjectivity supplies representatives for the reverse kernel-to-factorization implication.

References

• Truth anchor: D5/S3/ConceptDynamics/Refinement/ConceptKernelOrderDuality.concept_kernel_order_duality
• Dependency: D5/S3/ConceptDynamics/ConceptJoinUniversal