Injective Interface Target Factorization

Abstract

An injective interface uniquely factors every target on its realized image.

Theorem 1.1 (An injective interface factors every target).

$$\begin{array}{c}\forall X,B,Y:\mathrm{Type},\\ q:X\to B,T:X\to Y,\\ \mathrm{Injective}(q)\Rightarrow \\ \exists !h:\mathrm{range}(q)\to \mathrm{range}(T),\\ \mathrm{rangeFactorization}(T)=h\circ \mathrm{rangeFactorization}(q).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/RefinementFactorization/InjectiveInterfaceTargetFactorization.injective_interface_factors_every_target (✓ std3). ∎

Source. Repository-derived.

Commentary.

Both the interface and target are restricted canonically to their realized images. Thus the factor is total without choosing arbitrary values outside the interface image, and the statement remains valid for an empty state type.

Injectivity makes equality of interface values imply equality of states and hence equality of every target value. The imported realized-image kernel criterion turns this kernel inclusion directly into the displayed unique commuting factor.

References

• Truth anchor: D5/S3/ConceptDynamics/RefinementFactorization/InjectiveInterfaceTargetFactorization.injective_interface_factors_every_target
• Dependency: D5/S3/ConceptDynamics/RefinementFactorization/RealizedImageKernelFactorization