Physlib.Units.Dimension

Physlib
Units
Dimension

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Mathlib.Analysis.Normed.Field.Lemmas
public import Mathlib.Tactic.DeriveFintype

Dimension

In this module we define the type Dimension which carries the dimension of a physical quantity.

A Dimension B is parameterised by a basis B of base dimensions: it assigns a rational exponent to each base dimension b : B. The parameterisation is purely in the dimensional algebra: Dimension B is a CommGroup for every B (multiplication adds exponents, inversion negates them), so quantities can be typed by dimensions over any basis. The commutative-group and ℚ-power structure, decidable equality (DecidableEq), the base vectors single b, and the change-of-basis map extend are all generic in B.

PhysLib's default basis is LTMCTDimensionBase — length, time, mass, charge, temperature — whose projections and named generators (L𝓭, T𝓭, …) live in Physlib.Units.LTMCTDimensionBase. It is charge-based with five generators, so it is not the SI/ISQ base-quantity set; the ISQ set is ISQDimensionBase, and other systems (Gaussian–CGS, natural units, …) are equally expressible as Dimension B for a suitable basis B.

@[expose] public section

Defining dimensions

A dimension over a basis B of base dimensions: a rational exponent for each base dimension b : B. PhysLib's default basis is LTMCTDimensionBase.

The exponent of each base dimension.

structure Dimension (B : Type) where exponent : B → ℚ

              @[ext]
lemma ext {d1 d2 : Dimension B} (h : ∀ b, d1.exponent b = d2.exponent b) : d1 = d2 := byB:Typed1:Dimension Bd2:Dimension Bh:∀ (b : B), d1.exponent b = d2.exponent b⊢ d1 = d2
  cases d1mkB:Typed2:Dimension Bexponent✝:B → ℚh:∀ (b : B), { exponent := exponent✝ }.exponent b = d2.exponent b⊢ { exponent := exponent✝ } = d2
  cases d2mk.mkB:Typeexponent✝¹:B → ℚexponent✝:B → ℚh:∀ (b : B), { exponent := exponent✝¹ }.exponent b = { exponent := exponent✝ }.exponent b⊢ { exponent := exponent✝¹ } = { exponent := exponent✝ }
  congrmk.mkB:Typeexponent✝¹:B → ℚexponent✝:B → ℚh:∀ (b : B), { exponent := exponent✝¹ }.exponent b = { exponent := exponent✝ }.exponent b⊢ exponent✝¹ = exponent✝
  funext bmk.mkB:Typeexponent✝¹:B → ℚexponent✝:B → ℚh:∀ (b : B), { exponent := exponent✝¹ }.exponent b = { exponent := exponent✝ }.exponent bb:B⊢ exponent✝¹ b = exponent✝ b
  exact h bAll goals completed! 🐙instance : Mul (Dimension B) where
  mul d1 d2 := ⟨fun b => d1.exponent b + d2.exponent b⟩@[simp]
lemma mul_exponent (d1 d2 : Dimension B) (b : B) :
    (d1 * d2).exponent b = d1.exponent b + d2.exponent b := rflinstance : One (Dimension B) where
  one := ⟨fun _ => 0⟩@[simp]
lemma one_exponent (b : B) : (1 : Dimension B).exponent b = 0 := rflinstance : CommGroup (Dimension B) where
  mul_assoc a b c := byB:Typea:Dimension Bb:Dimension Bc:Dimension B⊢ a * b * c = a * (b * c)
    ext xB:Typea:Dimension Bb:Dimension Bc:Dimension Bx:B⊢ (a * b * c).exponent x = (a * (b * c)).exponent x
    simp [add_assoc]All goals completed! 🐙
  one_mul a := byB:Typea:Dimension B⊢ 1 * a = a
    ext xB:Typea:Dimension Bx:B⊢ (1 * a).exponent x = a.exponent x
    simpAll goals completed! 🐙
  mul_one a := byB:Typea:Dimension B⊢ a * 1 = a
    ext xB:Typea:Dimension Bx:B⊢ (a * 1).exponent x = a.exponent x
    simpAll goals completed! 🐙
  inv d := ⟨fun b => -d.exponent b⟩
  inv_mul_cancel a := byB:Typea:Dimension B⊢ { exponent := fun b => -a.exponent b } * a = 1
    ext xB:Typea:Dimension Bx:B⊢ ({ exponent := fun b => -a.exponent b } * a).exponent x = exponent 1 x
    simpAll goals completed! 🐙
  mul_comm a b := byB:Typea:Dimension Bb:Dimension B⊢ a * b = b * a
    ext xB:Typea:Dimension Bb:Dimension Bx:B⊢ (a * b).exponent x = (b * a).exponent x
    simp [add_comm]All goals completed! 🐙@[simp]
lemma inv_exponent (d : Dimension B) (b : B) : d⁻¹.exponent b = -d.exponent b := rfl@[simp]
lemma div_exponent (d1 d2 : Dimension B) (b : B) :
    (d1 / d2).exponent b = d1.exponent b - d2.exponent b := byB:Typed1:Dimension Bd2:Dimension Bb:B⊢ (d1 / d2).exponent b = d1.exponent b - d2.exponent b
  simp [div_eq_mul_inv, sub_eq_add_neg]All goals completed! 🐙

@[simp]
lemma npow_exponent (d : Dimension B) (n : ℕ) (b : B) :
    (d ^ n).exponent b = n • d.exponent b := byB:Typed:Dimension Bn:ℕb:B⊢ (d ^ n).exponent b = n • d.exponent b
  induction n with
  | zero =>zeroB:Typed:Dimension Bb:B⊢ (d ^ 0).exponent b = 0 • d.exponent b simpAll goals completed! 🐙
  | succ n ih =>succB:Typed:Dimension Bb:Bn:ℕih:(d ^ n).exponent b = n • d.exponent b⊢ (d ^ (n + 1)).exponent b = (n + 1) • d.exponent b rw [pow_succ,succB:Typed:Dimension Bb:Bn:ℕih:(d ^ n).exponent b = n • d.exponent b⊢ (d ^ n * d).exponent b = (n + 1) • d.exponent bAll goals completed! 🐙 mul_exponent,succB:Typed:Dimension Bb:Bn:ℕih:(d ^ n).exponent b = n • d.exponent b⊢ (d ^ n).exponent b + d.exponent b = (n + 1) • d.exponent bAll goals completed! 🐙 ih,succB:Typed:Dimension Bb:Bn:ℕih:(d ^ n).exponent b = n • d.exponent b⊢ n • d.exponent b + d.exponent b = (n + 1) • d.exponent bAll goals completed! 🐙 succ_nsmulsuccB:Typed:Dimension Bb:Bn:ℕih:(d ^ n).exponent b = n • d.exponent b⊢ n • d.exponent b + d.exponent b = n • d.exponent b + d.exponent bAll goals completed! 🐙]All goals completed! 🐙instance : Pow (Dimension B) ℚ where
  pow d q := ⟨fun b => d.exponent b * q⟩@[simp]
lemma qpow_exponent (d : Dimension B) (q : ℚ) (b : B) :
    (d ^ q).exponent b = d.exponent b * q := rfl

Decidable equality of dimensions over a finite basis B.

instance [Fintype B] : DecidableEq (Dimension B) := fun d1 d2 =>
  decidable_of_iff (∀ b, d1.exponent b = d2.exponent b)
    ⟨fun h => Dimension.ext h, fun h _ => h ▸ rfl⟩

The base-dimension vector for b : B: exponent 1 at b, 0 elsewhere. This is the generic analogue of the named generators L𝓭, T𝓭, …

def single [DecidableEq B] (b : B) : Dimension B := ⟨Pi.single b 1⟩

@[simp]
lemma single_exponent [DecidableEq B] (b b' : B) :
    (single b).exponent b' = if b' = b then 1 else 0 := byB:Typeinst✝:DecidableEq Bb:Bb':B⊢ (single b).exponent b' = if b' = b then 1 else 0
  simp only [single, Pi.single_apply]All goals completed! 🐙

Change of basis along a map f : B → B' of base dimensions: reindex a dimension over B into one over B' by placing each exponent at its image. For an embedding f (injective) this preserves every exponent (extend_exponent_apply), so a dimension in one system re-expresses faithfully in an extending one.

def extend {B' : Type} [Fintype B] [DecidableEq B'] (f : B → B') (d : Dimension B) :
    Dimension B' :=
  ⟨fun b' => ∑ b, if f b = b' then d.exponent b else 0⟩



@[simp]
lemma extend_exponent_apply {B' : Type} [Fintype B] [DecidableEq B'] {f : B → B'}
    (hf : Function.Injective f) (d : Dimension B) (b : B) :
    (extend f d).exponent (f b) = d.exponent b := byB:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'hf:Function.Injective fd:Dimension Bb:B⊢ (extend f d).exponent (f b) = d.exponent b
  simp only [extend]B:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'hf:Function.Injective fd:Dimension Bb:B⊢ (∑ b_1, if f b_1 = f b then d.exponent b_1 else 0) = d.exponent b
  rw [Finset.sum_eq_single b (fun b'' _ hne => byB:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'hf:Function.Injective fd:Dimension Bb:Bb'':Bx✝:b'' ∈ Finset.univhne:b'' ≠ b⊢ (if f b'' = f b then d.exponent b'' else 0) = 0B:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'hf:Function.Injective fd:Dimension Bb:B⊢ (if f b = f b then d.exponent b else 0) = d.exponent b simp [hf.ne hne]All goals completed! 🐙B:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'hf:Function.Injective fd:Dimension Bb:B⊢ (if f b = f b then d.exponent b else 0) = d.exponent b) (byB:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'hf:Function.Injective fd:Dimension Bb:B⊢ b ∉ Finset.univ → (if f b = f b then d.exponent b else 0) = 0B:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'hf:Function.Injective fd:Dimension Bb:B⊢ (if f b = f b then d.exponent b else 0) = d.exponent b simpAll goals completed! 🐙B:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'hf:Function.Injective fd:Dimension Bb:B⊢ (if f b = f b then d.exponent b else 0) = d.exponent b)]B:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'hf:Function.Injective fd:Dimension Bb:B⊢ (if f b = f b then d.exponent b else 0) = d.exponent b
  simpAll goals completed! 🐙

Dimension-preserving maps between bases

A cross-basis map of dimensions is only admissible if it preserves the dimensional algebra. We record the two truth-preserving directions as bundled data:

an Embedding B B' is an injective MonoidHom (Dimension B) (Dimension B') — a faithful, dimension-preserving inclusion of one basis into another; and

a Projection B' B is a surjective MonoidHom (Dimension B') (Dimension B) — a truth-preserving reduction of a richer basis onto a coarser one.

Being a MonoidHom is what makes either map dimension-preserving (it respects products, inverses and rational powers); the injectivity / surjectivity side condition distinguishes the two directions. Cross-basis dimension maps should be produced as one of these, so that dimension-preservation holds by construction — a bare relabelling that sends a base dimension to an inequivalent one is not expressible as either.

extend f packaged as a monoid homomorphism of dimensions.


def extendHom {B' : Type} [Fintype B] [DecidableEq B'] (f : B → B') :
    Dimension B →* Dimension B' where
  toFun := extend f
  map_one' := byB:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'⊢ extend f 1 = 1 ext b'B:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'b':B'⊢ (extend f 1).exponent b' = exponent 1 b'; simp [extend]All goals completed! 🐙
  map_mul' d1 d2 := byB:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'd1:Dimension Bd2:Dimension B⊢ extend f (d1 * d2) = extend f d1 * extend f d2
    ext b'B:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'd1:Dimension Bd2:Dimension Bb':B'⊢ (extend f (d1 * d2)).exponent b' = (extend f d1 * extend f d2).exponent b'
    simp only [extend, mul_exponent]B:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'd1:Dimension Bd2:Dimension Bb':B'⊢ (∑ x, if f x = b' then d1.exponent x + d2.exponent x else 0) =
  (∑ b, if f b = b' then d1.exponent b else 0) + ∑ b, if f b = b' then d2.exponent b else 0
    rw [← Finset.sum_add_distribB:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'd1:Dimension Bd2:Dimension Bb':B'⊢ (∑ x, if f x = b' then d1.exponent x + d2.exponent x else 0) =
  ∑ x, ((if f x = b' then d1.exponent x else 0) + if f x = b' then d2.exponent x else 0)B:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'd1:Dimension Bd2:Dimension Bb':B'⊢ (∑ x, if f x = b' then d1.exponent x + d2.exponent x else 0) =
  ∑ x, ((if f x = b' then d1.exponent x else 0) + if f x = b' then d2.exponent x else 0)]B:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'd1:Dimension Bd2:Dimension Bb':B'⊢ (∑ x, if f x = b' then d1.exponent x + d2.exponent x else 0) =
  ∑ x, ((if f x = b' then d1.exponent x else 0) + if f x = b' then d2.exponent x else 0)
    refine Finset.sum_congr rfl fun b _ => ?_B:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'd1:Dimension Bd2:Dimension Bb':B'b:Bx✝:b ∈ Finset.univ⊢ (if f b = b' then d1.exponent b + d2.exponent b else 0) =
  (if f b = b' then d1.exponent b else 0) + if f b = b' then d2.exponent b else 0
    split_ifsposB:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'd1:Dimension Bd2:Dimension Bb':B'b:Bx✝:b ∈ Finset.univh✝:f b = b'⊢ d1.exponent b + d2.exponent b = d1.exponent b + d2.exponent bnegB:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'd1:Dimension Bd2:Dimension Bb':B'b:Bx✝:b ∈ Finset.univh✝:¬f b = b'⊢ 0 = 0 + 0 <;>posB:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'd1:Dimension Bd2:Dimension Bb':B'b:Bx✝:b ∈ Finset.univh✝:f b = b'⊢ d1.exponent b + d2.exponent b = d1.exponent b + d2.exponent bnegB:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'd1:Dimension Bd2:Dimension Bb':B'b:Bx✝:b ∈ Finset.univh✝:¬f b = b'⊢ 0 = 0 + 0 simpAll goals completed! 🐙

A dimension embedding B ↪ B': an injective monoid homomorphism of dimensions. As a MonoidHom it is dimension-preserving (it respects products, inverses and rational powers); injectivity makes it a faithful inclusion of the basis B into B'. Cross-basis dimension injections are produced as Embeddings so that dimension-preservation holds by construction.

The underlying dimension-preserving homomorphism.

The homomorphism is injective (a faithful embedding).

              structure Embedding (B B' : Type) where  toHom : Dimension B →* Dimension B'  inj : Function.Injective toHom

A dimension projection B' ↠ B: a surjective monoid homomorphism of dimensions. As a MonoidHom it is truth-preserving, but it is lossy — it reduces a richer basis B' onto a coarser basis B, collapsing the base dimensions that B does not track.

The underlying dimension-preserving homomorphism.

The homomorphism is surjective (the reduction hits every dimension of B).

              structure Projection (B' B : Type) where  toHom : Dimension B' →* Dimension B  surj : Function.Surjective toHom

An injective basis map f : B → B' induces a dimension embedding, via extend. This is the label-level case: it sends each base dimension of B to a base dimension of B', so it is automatically dimension-preserving and faithful.


def Embedding.ofBasis {B B' : Type} [Fintype B] [DecidableEq B']
    (f : B → B') (hf : Function.Injective f) : Embedding B B' where
  toHom := extendHom f
  inj := byB✝:TypeB:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'hf:Function.Injective f⊢ Function.Injective ⇑(extendHom f)
    intro d1 d2 hB✝:TypeB:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'hf:Function.Injective fd1:Dimension Bd2:Dimension Bh:(extendHom f) d1 = (extendHom f) d2⊢ d1 = d2
    ext bB✝:TypeB:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'hf:Function.Injective fd1:Dimension Bd2:Dimension Bh:(extendHom f) d1 = (extendHom f) d2b:B⊢ d1.exponent b = d2.exponent b
    have h2 : (extendHom f d1).exponent (f b) = (extendHom f d2).exponent (f b) := byB✝:TypeB:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'hf:Function.Injective f⊢ Function.Injective ⇑(extendHom f)B✝:TypeB:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'hf:Function.Injective fd1:Dimension Bd2:Dimension Bh:(extendHom f) d1 = (extendHom f) d2b:Bh2:((extendHom f) d1).exponent (f b) = ((extendHom f) d2).exponent (f b)⊢ d1.exponent b = d2.exponent b
      rw [hB✝:TypeB:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'hf:Function.Injective fd1:Dimension Bd2:Dimension Bh:(extendHom f) d1 = (extendHom f) d2b:B⊢ ((extendHom f) d2).exponent (f b) = ((extendHom f) d2).exponent (f b)B✝:TypeB:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'hf:Function.Injective fd1:Dimension Bd2:Dimension Bh:(extendHom f) d1 = (extendHom f) d2b:Bh2:((extendHom f) d1).exponent (f b) = ((extendHom f) d2).exponent (f b)⊢ d1.exponent b = d2.exponent b]B✝:TypeB:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'hf:Function.Injective fd1:Dimension Bd2:Dimension Bh:(extendHom f) d1 = (extendHom f) d2b:Bh2:((extendHom f) d1).exponent (f b) = ((extendHom f) d2).exponent (f b)⊢ d1.exponent b = d2.exponent bB✝:TypeB:TypeB':Typeinst✝¹:Fintype Binst✝:DecidableEq B'f:B → B'hf:Function.Injective fd1:Dimension Bd2:Dimension Bh:(extendHom f) d1 = (extendHom f) d2b:Bh2:((extendHom f) d1).exponent (f b) = ((extendHom f) d2).exponent (f b)⊢ d1.exponent b = d2.exponent b
    simpa only [extendHom, MonoidHom.coe_mk, OneHom.coe_mk, extend_exponent_apply hf]
      using h2All goals completed! 🐙