11.1. The forgetful map (Dybkær Ch. 19)
The dimension map \dim sends a dimensioned kind — a
kind-of-property paired with a PhysLib Dimension
(ℚ-exponents over length/time/mass/charge/temperature) — to that dimension. It is
deliberately many-to-one: that is what makes
the dimension-1 disambiguation true.
Lean code for Definition11.1.1●1 definition
Associated Lean declarations
-
defdefined in PropertyKindCalculus/Dimension.leancomplete
def PropertyKindCalculus.DimensionedKind.toDimension {B : Type} [DimensionBasis B] (dk : PropertyKindCalculus.DimensionedKind B) : Dimension B
def PropertyKindCalculus.DimensionedKind.toDimension {B : Type} [DimensionBasis B] (dk : PropertyKindCalculus.DimensionedKind B) : Dimension B
The **forgetful functor** on objects: drop the kind identity, keep only the dimension. Naming it as a standalone map is what lets the central fact — that it is *not injective* — be stated and proved. Generic in the basis `B`.
Realized in the Dimension library (dimension/). DimensionedKind is the
structure pairing a kind with its Dimension; toDimension is the forgetful
projection. PhysLib + Mathlib enter only here, as a separate library; the spine
stays Mathlib-free.
The forgetful functor preserves products. The dimension of a product of
dimensioned kinds is the product of their dimensions,
\dim (a \cdot b) = \dim a \cdot \dim b,
the SI exponents adding — ordinary dimensional bookkeeping, proved as a law. This
is the dimension-component of functoriality, stated for the provisional product;
the full interaction-algebra version is the
homomorphism capstone below. Builds on the dimension map.
Lean code for Theorem11.1.2●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Dimension.leancomplete
theorem PropertyKindCalculus.DimensionedKind.toDimension_times {B : Type} [DimensionBasis B] (a b : PropertyKindCalculus.DimensionedKind B) : (a.times b).toDimension = a.toDimension * b.toDimension
theorem PropertyKindCalculus.DimensionedKind.toDimension_times {B : Type} [DimensionBasis B] (a b : PropertyKindCalculus.DimensionedKind B) : (a.times b).toDimension = a.toDimension * b.toDimension
**Coherence (multiplicativity).** `dim` carries products to products — it is a homomorphism into the multiplicative `Dimension` group.
The provisional product multiplies the dimension components (PhysLib's
Dimension.mul, i.e. exponent addition), so the equation holds by rfl. The unit
law \dim 1 = 1 holds likewise.
Dimensional coherence — \dim is a homomorphism over the full interaction
algebra. Whenever the interaction algebra says k_1 and k_2 combine to
k_3, their dimensions combine the same way:
\mathrm{KMul}\ k_1\ k_2\ k_3 \;\Longrightarrow\; \dim k_3 = \dim k_1 \cdot \dim k_2.
This is the theorem that licenses forgetting to the dimension layer without
losing soundness: a kind-level product is always dimensionally consistent. It
upgrades the proved multiplicativity from the
provisional product to Flater's gated kind product.
Lean code for Theorem11.1.3●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Interaction.leancomplete
theorem PropertyKindCalculus.InteractionAlgebra.dim_homomorphism (A : PropertyKindCalculus.InteractionAlgebra) {a b c : PropertyKindCalculus.DimensionedKind LTMCTDimensionBase} (h : A.KMul a b c) : c.toDimension = a.toDimension * b.toDimension
theorem PropertyKindCalculus.InteractionAlgebra.dim_homomorphism (A : PropertyKindCalculus.InteractionAlgebra) {a b c : PropertyKindCalculus.DimensionedKind LTMCTDimensionBase} (h : A.KMul a b c) : c.toDimension = a.toDimension * b.toDimension
**Dimensional coherence — `dim` is a homomorphism over the interaction algebra (R7).** Whenever the algebra sanctions `a × b = c`, forgetting to the dimension layer turns the kind product into PhysLib's `Dimension` product, `dim c = dim a · dim b`. This is the theorem that licenses *forgetting* to the dimension layer without losing soundness — and, read the other way, why matching dimensions are necessary but never sufficient: the kind relation, not `dim`, decides legality.
Realized in the Interaction module as InteractionAlgebra.dim_homomorphism.
Coherence is a well-formedness field of every InteractionAlgebra, so the
homomorphism is its projection: any algebra that can be formed at all already
guarantees \dim k_3 = \dim k_1 \cdot \dim k_2 on every sanctioned edge. The
content sits in the worked algebra, where the obligation is discharged by the
Dimension-group computation, case by case.