Physlib.Units.ISQBridge

Physlib
Units
ISQBridge

Imports

/-
Copyright (c) 2026 Nicolas Rouquette. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Nicolas Rouquette
-/
module

public import Physlib.Units.LTMCTDimensionBase
public import Physlib.Units.ISQDimensionBase

Bridging PhysLib's default basis and the ISQ basis

LTMCTDimensionBase (length, time, mass, charge, temperature) and ISQDimensionBase (the seven ISO/IEC 80000-1 base quantities) make different base/derived choices. This module relates them by the two truth-preserving directions of Dimension.Embedding and Dimension.Projection:

ltmctToISQ : Dimension.Embedding LTMCTDimensionBase ISQDimensionBase — the dimension-preserving inclusion of PhysLib dimensions into ISQ dimensions. It sends the charge generator to the derived ISQ charge I · T (toISQHom_C𝓭), so it is faithful (toISQHom_injective) and physically correct, not a bare relabelling.

isqToLTMCT : Dimension.Projection ISQDimensionBase LTMCTDimensionBase — the truth-preserving reduction of ISQ dimensions onto PhysLib's. It reads electric current as charge/time and forgets amount of substance and luminous intensity (the base quantities PhysLib does not track).

The two fit together as a retraction, isqToLTMCT ∘ ltmctToISQ = id (isqToLTMCT_comp_ltmctToISQ): PhysLib's basis embeds faithfully into ISQ and is recovered exactly by the projection — but the reverse composite is not the identity, because amount of substance and luminous intensity cannot be recovered once dropped. That is the asymmetry: one can reduce ISQ to LTMCT, but not conjure the extra base quantities back without adding them.

@[expose] public section

The function underlying toISQHom: fix length, mass, time and temperature, and send PhysLib's charge generator to the derived ISQ charge I · T (the current exponent is the charge exponent, and the time exponent absorbs it).

def toISQFun (d : Dimension LTMCTDimensionBase) : Dimension ISQDimensionBase :=
  ⟨fun
    | .length => d.exponent .length
    | .mass => d.exponent .mass
    | .time => d.exponent .time + d.exponent .charge
    | .current => d.exponent .charge
    | .temperature => d.exponent .temperature
    | .amount => 0
    | .luminousIntensity => 0⟩

The dimension-preserving embedding of PhysLib dimensions into the ISQ dimensions.

def toISQHom : Dimension LTMCTDimensionBase →* Dimension ISQDimensionBase where
  toFun := toISQFun
  map_one' := by⊢ toISQFun 1 = 1 ext bb:ISQDimensionBase⊢ (toISQFun 1).exponent b = exponent 1 b; cases blength⊢ (toISQFun 1).exponent ISQDimensionBase.length = exponent 1 ISQDimensionBase.lengthmass⊢ (toISQFun 1).exponent ISQDimensionBase.mass = exponent 1 ISQDimensionBase.masstime⊢ (toISQFun 1).exponent ISQDimensionBase.time = exponent 1 ISQDimensionBase.timecurrent⊢ (toISQFun 1).exponent ISQDimensionBase.current = exponent 1 ISQDimensionBase.currenttemperature⊢ (toISQFun 1).exponent ISQDimensionBase.temperature = exponent 1 ISQDimensionBase.temperatureamount⊢ (toISQFun 1).exponent ISQDimensionBase.amount = exponent 1 ISQDimensionBase.amountluminousIntensity⊢ (toISQFun 1).exponent ISQDimensionBase.luminousIntensity = exponent 1 ISQDimensionBase.luminousIntensity <;>length⊢ (toISQFun 1).exponent ISQDimensionBase.length = exponent 1 ISQDimensionBase.lengthmass⊢ (toISQFun 1).exponent ISQDimensionBase.mass = exponent 1 ISQDimensionBase.masstime⊢ (toISQFun 1).exponent ISQDimensionBase.time = exponent 1 ISQDimensionBase.timecurrent⊢ (toISQFun 1).exponent ISQDimensionBase.current = exponent 1 ISQDimensionBase.currenttemperature⊢ (toISQFun 1).exponent ISQDimensionBase.temperature = exponent 1 ISQDimensionBase.temperatureamount⊢ (toISQFun 1).exponent ISQDimensionBase.amount = exponent 1 ISQDimensionBase.amountluminousIntensity⊢ (toISQFun 1).exponent ISQDimensionBase.luminousIntensity = exponent 1 ISQDimensionBase.luminousIntensity simp [toISQFun]All goals completed! 🐙
  map_mul' d1 d2 := byd1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBase⊢ (d1 * d2).toISQFun = d1.toISQFun * d2.toISQFun
    ext bd1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBaseb:ISQDimensionBase⊢ (d1 * d2).toISQFun.exponent b = (d1.toISQFun * d2.toISQFun).exponent b
    cases blengthd1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBase⊢ (d1 * d2).toISQFun.exponent ISQDimensionBase.length = (d1.toISQFun * d2.toISQFun).exponent ISQDimensionBase.lengthmassd1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBase⊢ (d1 * d2).toISQFun.exponent ISQDimensionBase.mass = (d1.toISQFun * d2.toISQFun).exponent ISQDimensionBase.masstimed1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBase⊢ (d1 * d2).toISQFun.exponent ISQDimensionBase.time = (d1.toISQFun * d2.toISQFun).exponent ISQDimensionBase.timecurrentd1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBase⊢ (d1 * d2).toISQFun.exponent ISQDimensionBase.current = (d1.toISQFun * d2.toISQFun).exponent ISQDimensionBase.currenttemperatured1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBase⊢ (d1 * d2).toISQFun.exponent ISQDimensionBase.temperature =
  (d1.toISQFun * d2.toISQFun).exponent ISQDimensionBase.temperatureamountd1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBase⊢ (d1 * d2).toISQFun.exponent ISQDimensionBase.amount = (d1.toISQFun * d2.toISQFun).exponent ISQDimensionBase.amountluminousIntensityd1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBase⊢ (d1 * d2).toISQFun.exponent ISQDimensionBase.luminousIntensity =
  (d1.toISQFun * d2.toISQFun).exponent ISQDimensionBase.luminousIntensity <;>lengthd1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBase⊢ (d1 * d2).toISQFun.exponent ISQDimensionBase.length = (d1.toISQFun * d2.toISQFun).exponent ISQDimensionBase.lengthmassd1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBase⊢ (d1 * d2).toISQFun.exponent ISQDimensionBase.mass = (d1.toISQFun * d2.toISQFun).exponent ISQDimensionBase.masstimed1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBase⊢ (d1 * d2).toISQFun.exponent ISQDimensionBase.time = (d1.toISQFun * d2.toISQFun).exponent ISQDimensionBase.timecurrentd1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBase⊢ (d1 * d2).toISQFun.exponent ISQDimensionBase.current = (d1.toISQFun * d2.toISQFun).exponent ISQDimensionBase.currenttemperatured1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBase⊢ (d1 * d2).toISQFun.exponent ISQDimensionBase.temperature =
  (d1.toISQFun * d2.toISQFun).exponent ISQDimensionBase.temperatureamountd1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBase⊢ (d1 * d2).toISQFun.exponent ISQDimensionBase.amount = (d1.toISQFun * d2.toISQFun).exponent ISQDimensionBase.amountluminousIntensityd1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBase⊢ (d1 * d2).toISQFun.exponent ISQDimensionBase.luminousIntensity =
  (d1.toISQFun * d2.toISQFun).exponent ISQDimensionBase.luminousIntensity simp only [toISQFun, mul_exponent]luminousIntensityd1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBase⊢ 0 = 0 + 0
    all_goals ringAll goals completed! 🐙

toISQHom applied to a dimension is toISQFun.

lemma toISQHom_apply (d : Dimension LTMCTDimensionBase) : toISQHom d = toISQFun d := rfl

The function underlying fromISQHom: fix length, mass and temperature, read electric current as charge/time (the charge exponent is the current exponent, and the time exponent subtracts it), and drop amount of substance and luminous intensity.

def fromISQFun (d : Dimension ISQDimensionBase) : Dimension LTMCTDimensionBase :=
  ⟨fun
    | .length => d.exponent .length
    | .time => d.exponent .time - d.exponent .current
    | .mass => d.exponent .mass
    | .charge => d.exponent .current
    | .temperature => d.exponent .temperature⟩

The truth-preserving reduction of ISQ dimensions onto PhysLib's.

def fromISQHom : Dimension ISQDimensionBase →* Dimension LTMCTDimensionBase where
  toFun := fromISQFun
  map_one' := by⊢ fromISQFun 1 = 1 ext bb:LTMCTDimensionBase⊢ (fromISQFun 1).exponent b = exponent 1 b; cases blength⊢ (fromISQFun 1).exponent LTMCTDimensionBase.length = exponent 1 LTMCTDimensionBase.lengthtime⊢ (fromISQFun 1).exponent LTMCTDimensionBase.time = exponent 1 LTMCTDimensionBase.timemass⊢ (fromISQFun 1).exponent LTMCTDimensionBase.mass = exponent 1 LTMCTDimensionBase.masscharge⊢ (fromISQFun 1).exponent LTMCTDimensionBase.charge = exponent 1 LTMCTDimensionBase.chargetemperature⊢ (fromISQFun 1).exponent LTMCTDimensionBase.temperature = exponent 1 LTMCTDimensionBase.temperature <;>length⊢ (fromISQFun 1).exponent LTMCTDimensionBase.length = exponent 1 LTMCTDimensionBase.lengthtime⊢ (fromISQFun 1).exponent LTMCTDimensionBase.time = exponent 1 LTMCTDimensionBase.timemass⊢ (fromISQFun 1).exponent LTMCTDimensionBase.mass = exponent 1 LTMCTDimensionBase.masscharge⊢ (fromISQFun 1).exponent LTMCTDimensionBase.charge = exponent 1 LTMCTDimensionBase.chargetemperature⊢ (fromISQFun 1).exponent LTMCTDimensionBase.temperature = exponent 1 LTMCTDimensionBase.temperature simp [fromISQFun]All goals completed! 🐙
  map_mul' d1 d2 := byd1:Dimension ISQDimensionBased2:Dimension ISQDimensionBase⊢ (d1 * d2).fromISQFun = d1.fromISQFun * d2.fromISQFun
    ext bd1:Dimension ISQDimensionBased2:Dimension ISQDimensionBaseb:LTMCTDimensionBase⊢ (d1 * d2).fromISQFun.exponent b = (d1.fromISQFun * d2.fromISQFun).exponent b
    cases blengthd1:Dimension ISQDimensionBased2:Dimension ISQDimensionBase⊢ (d1 * d2).fromISQFun.exponent LTMCTDimensionBase.length =
  (d1.fromISQFun * d2.fromISQFun).exponent LTMCTDimensionBase.lengthtimed1:Dimension ISQDimensionBased2:Dimension ISQDimensionBase⊢ (d1 * d2).fromISQFun.exponent LTMCTDimensionBase.time = (d1.fromISQFun * d2.fromISQFun).exponent LTMCTDimensionBase.timemassd1:Dimension ISQDimensionBased2:Dimension ISQDimensionBase⊢ (d1 * d2).fromISQFun.exponent LTMCTDimensionBase.mass = (d1.fromISQFun * d2.fromISQFun).exponent LTMCTDimensionBase.masscharged1:Dimension ISQDimensionBased2:Dimension ISQDimensionBase⊢ (d1 * d2).fromISQFun.exponent LTMCTDimensionBase.charge =
  (d1.fromISQFun * d2.fromISQFun).exponent LTMCTDimensionBase.chargetemperatured1:Dimension ISQDimensionBased2:Dimension ISQDimensionBase⊢ (d1 * d2).fromISQFun.exponent LTMCTDimensionBase.temperature =
  (d1.fromISQFun * d2.fromISQFun).exponent LTMCTDimensionBase.temperature <;>lengthd1:Dimension ISQDimensionBased2:Dimension ISQDimensionBase⊢ (d1 * d2).fromISQFun.exponent LTMCTDimensionBase.length =
  (d1.fromISQFun * d2.fromISQFun).exponent LTMCTDimensionBase.lengthtimed1:Dimension ISQDimensionBased2:Dimension ISQDimensionBase⊢ (d1 * d2).fromISQFun.exponent LTMCTDimensionBase.time = (d1.fromISQFun * d2.fromISQFun).exponent LTMCTDimensionBase.timemassd1:Dimension ISQDimensionBased2:Dimension ISQDimensionBase⊢ (d1 * d2).fromISQFun.exponent LTMCTDimensionBase.mass = (d1.fromISQFun * d2.fromISQFun).exponent LTMCTDimensionBase.masscharged1:Dimension ISQDimensionBased2:Dimension ISQDimensionBase⊢ (d1 * d2).fromISQFun.exponent LTMCTDimensionBase.charge =
  (d1.fromISQFun * d2.fromISQFun).exponent LTMCTDimensionBase.chargetemperatured1:Dimension ISQDimensionBased2:Dimension ISQDimensionBase⊢ (d1 * d2).fromISQFun.exponent LTMCTDimensionBase.temperature =
  (d1.fromISQFun * d2.fromISQFun).exponent LTMCTDimensionBase.temperature simp only [fromISQFun, mul_exponent]All goals completed! 🐙
    all_goals ringAll goals completed! 🐙

fromISQHom applied to a dimension is fromISQFun.

lemma fromISQHom_apply (d : Dimension ISQDimensionBase) : fromISQHom d = fromISQFun d := rfl

The projection recovers PhysLib's basis from its image under the embedding: fromISQHom ∘ toISQHom = id.

lemma fromISQHom_comp_toISQHom :
    fromISQHom.comp toISQHom = MonoidHom.id (Dimension LTMCTDimensionBase) := by⊢ fromISQHom.comp toISQHom = MonoidHom.id (Dimension LTMCTDimensionBase)
  refine MonoidHom.ext fun d => Dimension.ext fun b => ?_d:Dimension LTMCTDimensionBaseb:LTMCTDimensionBase⊢ ((fromISQHom.comp toISQHom) d).exponent b = ((MonoidHom.id (Dimension LTMCTDimensionBase)) d).exponent b
  cases blengthd:Dimension LTMCTDimensionBase⊢ ((fromISQHom.comp toISQHom) d).exponent LTMCTDimensionBase.length =
  ((MonoidHom.id (Dimension LTMCTDimensionBase)) d).exponent LTMCTDimensionBase.lengthtimed:Dimension LTMCTDimensionBase⊢ ((fromISQHom.comp toISQHom) d).exponent LTMCTDimensionBase.time =
  ((MonoidHom.id (Dimension LTMCTDimensionBase)) d).exponent LTMCTDimensionBase.timemassd:Dimension LTMCTDimensionBase⊢ ((fromISQHom.comp toISQHom) d).exponent LTMCTDimensionBase.mass =
  ((MonoidHom.id (Dimension LTMCTDimensionBase)) d).exponent LTMCTDimensionBase.masscharged:Dimension LTMCTDimensionBase⊢ ((fromISQHom.comp toISQHom) d).exponent LTMCTDimensionBase.charge =
  ((MonoidHom.id (Dimension LTMCTDimensionBase)) d).exponent LTMCTDimensionBase.chargetemperatured:Dimension LTMCTDimensionBase⊢ ((fromISQHom.comp toISQHom) d).exponent LTMCTDimensionBase.temperature =
  ((MonoidHom.id (Dimension LTMCTDimensionBase)) d).exponent LTMCTDimensionBase.temperature <;>lengthd:Dimension LTMCTDimensionBase⊢ ((fromISQHom.comp toISQHom) d).exponent LTMCTDimensionBase.length =
  ((MonoidHom.id (Dimension LTMCTDimensionBase)) d).exponent LTMCTDimensionBase.lengthtimed:Dimension LTMCTDimensionBase⊢ ((fromISQHom.comp toISQHom) d).exponent LTMCTDimensionBase.time =
  ((MonoidHom.id (Dimension LTMCTDimensionBase)) d).exponent LTMCTDimensionBase.timemassd:Dimension LTMCTDimensionBase⊢ ((fromISQHom.comp toISQHom) d).exponent LTMCTDimensionBase.mass =
  ((MonoidHom.id (Dimension LTMCTDimensionBase)) d).exponent LTMCTDimensionBase.masscharged:Dimension LTMCTDimensionBase⊢ ((fromISQHom.comp toISQHom) d).exponent LTMCTDimensionBase.charge =
  ((MonoidHom.id (Dimension LTMCTDimensionBase)) d).exponent LTMCTDimensionBase.chargetemperatured:Dimension LTMCTDimensionBase⊢ ((fromISQHom.comp toISQHom) d).exponent LTMCTDimensionBase.temperature =
  ((MonoidHom.id (Dimension LTMCTDimensionBase)) d).exponent LTMCTDimensionBase.temperature simp only [MonoidHom.comp_apply, MonoidHom.id_apply, toISQHom_apply,
    fromISQHom_apply, fromISQFun, toISQFun]All goals completed! 🐙
  all_goals ringAll goals completed! 🐙

toISQHom is injective: PhysLib dimensions include faithfully into ISQ.


lemma toISQHom_injective : Function.Injective toISQHom := by⊢ Function.Injective ⇑toISQHom
  intro d1 d2 hd1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBaseh:toISQHom d1 = toISQHom d2⊢ d1 = d2
  have key : ∀ b : ISQDimensionBase, (toISQFun d1).exponent b = (toISQFun d2).exponent b := by⊢ Function.Injective ⇑toISQHomd1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBaseh:toISQHom d1 = toISQHom d2key:∀ (b : ISQDimensionBase), d1.toISQFun.exponent b = d2.toISQFun.exponent b⊢ d1 = d2
    intro bd1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBaseh:toISQHom d1 = toISQHom d2b:ISQDimensionBase⊢ d1.toISQFun.exponent b = d2.toISQFun.exponent bd1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBaseh:toISQHom d1 = toISQHom d2key:∀ (b : ISQDimensionBase), d1.toISQFun.exponent b = d2.toISQFun.exponent b⊢ d1 = d2
    have hb := congrArg (fun d => Dimension.exponent d b) hd1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBaseh:toISQHom d1 = toISQHom d2b:ISQDimensionBasehb:(toISQHom d1).exponent b = (toISQHom d2).exponent b⊢ d1.toISQFun.exponent b = d2.toISQFun.exponent bd1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBaseh:toISQHom d1 = toISQHom d2key:∀ (b : ISQDimensionBase), d1.toISQFun.exponent b = d2.toISQFun.exponent b⊢ d1 = d2
    simpa only [toISQHom_apply] using hbd1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBaseh:toISQHom d1 = toISQHom d2key:∀ (b : ISQDimensionBase), d1.toISQFun.exponent b = d2.toISQFun.exponent b⊢ d1 = d2d1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBaseh:toISQHom d1 = toISQHom d2key:∀ (b : ISQDimensionBase), d1.toISQFun.exponent b = d2.toISQFun.exponent b⊢ d1 = d2
  ext bd1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBaseh:toISQHom d1 = toISQHom d2key:∀ (b : ISQDimensionBase), d1.toISQFun.exponent b = d2.toISQFun.exponent bb:LTMCTDimensionBase⊢ d1.exponent b = d2.exponent b
  cases b with
  | length =>lengthd1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBaseh:toISQHom d1 = toISQHom d2key:∀ (b : ISQDimensionBase), d1.toISQFun.exponent b = d2.toISQFun.exponent b⊢ d1.exponent LTMCTDimensionBase.length = d2.exponent LTMCTDimensionBase.length simpa only [toISQFun] using key .lengthAll goals completed! 🐙
  | time =>timed1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBaseh:toISQHom d1 = toISQHom d2key:∀ (b : ISQDimensionBase), d1.toISQFun.exponent b = d2.toISQFun.exponent b⊢ d1.exponent LTMCTDimensionBase.time = d2.exponent LTMCTDimensionBase.time
      have ht := key .timetimed1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBaseh:toISQHom d1 = toISQHom d2key:∀ (b : ISQDimensionBase), d1.toISQFun.exponent b = d2.toISQFun.exponent bht:d1.toISQFun.exponent ISQDimensionBase.time = d2.toISQFun.exponent ISQDimensionBase.time⊢ d1.exponent LTMCTDimensionBase.time = d2.exponent LTMCTDimensionBase.time
      have hc := key .currenttimed1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBaseh:toISQHom d1 = toISQHom d2key:∀ (b : ISQDimensionBase), d1.toISQFun.exponent b = d2.toISQFun.exponent bht:d1.toISQFun.exponent ISQDimensionBase.time = d2.toISQFun.exponent ISQDimensionBase.timehc:d1.toISQFun.exponent ISQDimensionBase.current = d2.toISQFun.exponent ISQDimensionBase.current⊢ d1.exponent LTMCTDimensionBase.time = d2.exponent LTMCTDimensionBase.time
      simp only [toISQFun] at ht hctimed1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBaseh:toISQHom d1 = toISQHom d2key:∀ (b : ISQDimensionBase), d1.toISQFun.exponent b = d2.toISQFun.exponent bht:d1.exponent LTMCTDimensionBase.time + d1.exponent LTMCTDimensionBase.charge =
  d2.exponent LTMCTDimensionBase.time + d2.exponent LTMCTDimensionBase.chargehc:d1.exponent LTMCTDimensionBase.charge = d2.exponent LTMCTDimensionBase.charge⊢ d1.exponent LTMCTDimensionBase.time = d2.exponent LTMCTDimensionBase.time
      linarithAll goals completed! 🐙
  | mass =>massd1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBaseh:toISQHom d1 = toISQHom d2key:∀ (b : ISQDimensionBase), d1.toISQFun.exponent b = d2.toISQFun.exponent b⊢ d1.exponent LTMCTDimensionBase.mass = d2.exponent LTMCTDimensionBase.mass simpa only [toISQFun] using key .massAll goals completed! 🐙
  | charge =>charged1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBaseh:toISQHom d1 = toISQHom d2key:∀ (b : ISQDimensionBase), d1.toISQFun.exponent b = d2.toISQFun.exponent b⊢ d1.exponent LTMCTDimensionBase.charge = d2.exponent LTMCTDimensionBase.charge simpa only [toISQFun] using key .currentAll goals completed! 🐙
  | temperature =>temperatured1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBaseh:toISQHom d1 = toISQHom d2key:∀ (b : ISQDimensionBase), d1.toISQFun.exponent b = d2.toISQFun.exponent b⊢ d1.exponent LTMCTDimensionBase.temperature = d2.exponent LTMCTDimensionBase.temperature simpa only [toISQFun] using key .temperatureAll goals completed! 🐙

fromISQHom is surjective: every PhysLib dimension is the reduction of some ISQ dimension (namely its own embedding).


lemma fromISQHom_surjective : Function.Surjective fromISQHom := fun y =>
  ⟨toISQHom y, byy:Dimension LTMCTDimensionBase⊢ fromISQHom (toISQHom y) = y rw [← MonoidHom.comp_apply,y:Dimension LTMCTDimensionBase⊢ (fromISQHom.comp toISQHom) y = yAll goals completed! 🐙 fromISQHom_comp_toISQHom,y:Dimension LTMCTDimensionBase⊢ (MonoidHom.id (Dimension LTMCTDimensionBase)) y = yAll goals completed! 🐙 MonoidHom.id_applyy:Dimension LTMCTDimensionBase⊢ y = yAll goals completed! 🐙]All goals completed! 🐙⟩

PhysLib's dimensions embed into the ISQ dimensions (charge ↦ I · T).

def ltmctToISQ : Embedding LTMCTDimensionBase ISQDimensionBase where
  toHom := toISQHom
  inj := toISQHom_injective

The ISQ dimensions project onto PhysLib's, reading current as charge/time and forgetting amount of substance and luminous intensity.

def isqToLTMCT : Projection ISQDimensionBase LTMCTDimensionBase where
  toHom := fromISQHom
  surj := fromISQHom_surjective

The projection is a retraction of the embedding: isqToLTMCT ∘ ltmctToISQ = id. So PhysLib's basis embeds faithfully into ISQ and is recovered by the projection, but not conversely — amount of substance and luminous intensity cannot be recovered.

lemma isqToLTMCT_comp_ltmctToISQ :
    isqToLTMCT.toHom.comp ltmctToISQ.toHom = MonoidHom.id (Dimension LTMCTDimensionBase) :=
  fromISQHom_comp_toISQHom

The embedding is physically faithful on charge: PhysLib's charge generator C𝓭 maps to the derived ISQ charge I · T.

lemma toISQHom_C𝓭 : toISQHom C𝓭 = ISQDimensionBase.charge := by⊢ toISQHom C𝓭 = ISQDimensionBase.charge
  ext bb:ISQDimensionBase⊢ (toISQHom C𝓭).exponent b = ISQDimensionBase.charge.exponent b
  cases blength⊢ (toISQHom C𝓭).exponent ISQDimensionBase.length = ISQDimensionBase.charge.exponent ISQDimensionBase.lengthmass⊢ (toISQHom C𝓭).exponent ISQDimensionBase.mass = ISQDimensionBase.charge.exponent ISQDimensionBase.masstime⊢ (toISQHom C𝓭).exponent ISQDimensionBase.time = ISQDimensionBase.charge.exponent ISQDimensionBase.timecurrent⊢ (toISQHom C𝓭).exponent ISQDimensionBase.current = ISQDimensionBase.charge.exponent ISQDimensionBase.currenttemperature⊢ (toISQHom C𝓭).exponent ISQDimensionBase.temperature = ISQDimensionBase.charge.exponent ISQDimensionBase.temperatureamount⊢ (toISQHom C𝓭).exponent ISQDimensionBase.amount = ISQDimensionBase.charge.exponent ISQDimensionBase.amountluminousIntensity⊢ (toISQHom C𝓭).exponent ISQDimensionBase.luminousIntensity =
  ISQDimensionBase.charge.exponent ISQDimensionBase.luminousIntensity <;>length⊢ (toISQHom C𝓭).exponent ISQDimensionBase.length = ISQDimensionBase.charge.exponent ISQDimensionBase.lengthmass⊢ (toISQHom C𝓭).exponent ISQDimensionBase.mass = ISQDimensionBase.charge.exponent ISQDimensionBase.masstime⊢ (toISQHom C𝓭).exponent ISQDimensionBase.time = ISQDimensionBase.charge.exponent ISQDimensionBase.timecurrent⊢ (toISQHom C𝓭).exponent ISQDimensionBase.current = ISQDimensionBase.charge.exponent ISQDimensionBase.currenttemperature⊢ (toISQHom C𝓭).exponent ISQDimensionBase.temperature = ISQDimensionBase.charge.exponent ISQDimensionBase.temperatureamount⊢ (toISQHom C𝓭).exponent ISQDimensionBase.amount = ISQDimensionBase.charge.exponent ISQDimensionBase.amountluminousIntensity⊢ (toISQHom C𝓭).exponent ISQDimensionBase.luminousIntensity =
  ISQDimensionBase.charge.exponent ISQDimensionBase.luminousIntensity simp [toISQHom_apply, toISQFun, C𝓭, ofLTMCTDimensionBase,
    ISQDimensionBase.charge, single_exponent]All goals completed! 🐙