Dimensioned spaces

A space is an index type I together with a unit assignment δ : I → Uom B. A vector over it is a family of quantities indexed by I, the component at i carrying the unit δ i; a linear map is handled in LambdaS.Map.

Spaces are structural

Space B I is a reducible abbreviation for I → Uom B. A space therefore is its unit assignment: two spaces with equal δ are equal, definitionally, with no coercion in between.

This is a decision, not an accident. It is what makes a uniform space equal to triv ⊗ u rather than merely isomorphic to it, and so what lets a signature over uniform spaces reject a non-uniform argument as a type error rather than a failed side condition. Making spaces nominal would break Space.uniform_iff_scale_triv and, with it, the claim that Hart's taxonomy is derived rather than checked.

@[reducible, inline]

abbrev LambdaS.Space (B : Type u_1) (I : Type u_2) : Type (max u_2 u_1)

A space: an index type together with a unit assignment. Structural in δ.

Equations

• LambdaS.Space B I = (I → LambdaS.Uom B)

def LambdaS.Space.triv (B : Type u_4) (I : Type u_5) : Space B I

The dimensionless space on I: every component carries the trivial unit.

Equations

• LambdaS.Space.triv B I x✝ = 1

def LambdaS.Space.dual {B : Type u_1} {I : Type u_2} (V : Space B I) : Space B I

The dual space carries reciprocal units.

This one definition is why ⟨φ|ψ⟩ is dimensionless and why ⟨φ|H|ψ⟩ carries the unit of H: neither needs a rule.

Equations

• V.dual i = (V i)⁻¹

def LambdaS.Space.scale {B : Type u_1} {I : Type u_2} (V : Space B I) (d : Uom B) : Space B I

Scaling a space by a scalar unit, written V ⊗ d.

Equations

• (V ⊗ d) i = V i * d

def LambdaS.Space.«term_⊗_» : Lean.TrailingParserDescr

Scaling a space by a scalar unit, written V ⊗ d.

Equations

• LambdaS.Space.«term_⊗_» = Lean.ParserDescr.trailingNode `LambdaS.Space.«term_⊗_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ ") (Lean.ParserDescr.cat `term 71))

def LambdaS.Space.Uniform {B : Type u_1} {I : Type u_2} (V : Space B I) : Prop

A space is uniform when every component carries the same unit.

Equations

• V.Uniform = ∃ (u : LambdaS.Uom B), ∀ (i : I), V i = u

def LambdaS.Space.tensor {B : Type u_1} {I : Type u_2} {J : Type u_3} (V : Space B I) (W : Space B J) : Space B (I × J)

The tensor product of spaces: index types multiply, units multiply. This is what composite quantum systems need.

Equations

• V.tensor W p = V p.1 * W p.2

def LambdaS.Space.ofUom {B : Type u_1} (d : Uom B) : Space B PUnit.{u_4 + 1}

The one-dimensional space carrying unit d.

Equations

• LambdaS.Space.ofUom d x✝ = d

theorem LambdaS.Space.scale_eq_tensor {B : Type u_1} {I : Type u_2} (V : Space B I) (d : Uom B) (i : I) : (V ⊗ d) i = V.tensor (ofUom d) (i, PUnit.unit)

Scaling is tensoring. V ⊗ d is the tensor product of V with the one-dimensional space carrying d, transported along I × PUnit ≅ I.

So ⊗ is a single operator, not two that happen to share notation: the scalar case is the one-point case. It holds definitionally.

@[simp]

theorem LambdaS.Space.triv_apply {B : Type u_1} {I : Type u_2} (i : I) : triv B I i = 1

@[simp]

theorem LambdaS.Space.dual_apply {B : Type u_1} {I : Type u_2} (V : Space B I) (i : I) : V.dual i = (V i)⁻¹

@[simp]

theorem LambdaS.Space.scale_apply {B : Type u_1} {I : Type u_2} (V : Space B I) (d : Uom B) (i : I) : (V ⊗ d) i = V i * d

@[simp]

theorem LambdaS.Space.dual_dual {B : Type u_1} {I : Type u_2} (V : Space B I) : V.dual.dual = V

@[simp]

theorem LambdaS.Space.scale_one {B : Type u_1} {I : Type u_2} (V : Space B I) : V ⊗ 1 = V

@[simp]

theorem LambdaS.Space.scale_scale {B : Type u_1} {I : Type u_2} (V : Space B I) (d e : Uom B) : V ⊗ d ⊗ e = V ⊗ (d * e)

Scaling composes: (V ⊗ d) ⊗ e = V ⊗ (d * e). Half of the functoriality of ⊗; the other half is entry_scale_scale (in LambdaS.Map).

theorem LambdaS.Space.dual_scale {B : Type u_1} {I : Type u_2} (V : Space B I) (d : Uom B) : (V ⊗ d).dual = V.dual ⊗ d⁻¹

theorem LambdaS.Space.uniform_iff_scale_triv {B : Type u_1} {I : Type u_2} (V : Space B I) : V.Uniform ↔ ∃ (u : Uom B), V = triv B I ⊗ u

A uniform space is equal to a scaled dimensionless space, not merely isomorphic to one. This equality is what structurality buys, and it is what makes svd_entry_const (in LambdaS.Map) a statement about types.

theorem LambdaS.Space.triv_uniform {B : Type u_1} {I : Type u_2} : (triv B I).Uniform