The units of charge

A unit of charge corresponding to a choice of translationally-invariant metric on the charge manifold (to be defined diffeomorphic to ℝ). Such a choice is (non-canonically) equivalent to a choice of positive real number. We define the type ChargeUnit to be equivalent to the positive reals.

We assume that the charge manifold is already defined with an orientation, with the electron being in the negative direction.

On ChargeUnit there is an instance of division giving a real number, corresponding to the ratio of the two scales of temperature unit.

To define specific charge units, we first state the existence of a a given charge unit, and then construct all other charge units from it. We choose to state the existence of the charge unit of the coulomb, and construct all other charge units from that.

structure ChargeUnit : Type

The choices of translationally-invariant metrics on the charge-manifold. Such a choice corresponds to a choice of units for charge. This assumes that an orientation has already being picked on the charge manifold.

• val : ℝ

  The underlying scale of the unit.

• property : 0 < self.val

@[simp]

theorem ChargeUnit.val_neq_zero (x : ChargeUnit) : x.val ≠ 0

theorem ChargeUnit.val_pos (x : ChargeUnit) : 0 < x.val

instance ChargeUnit.instInhabited : Inhabited ChargeUnit

Equations

• ChargeUnit.instInhabited = { default := { val := 1, property := ChargeUnit.instInhabited._proof_1 } }

Division of ChargeUnit

noncomputable instance ChargeUnit.instHDivNNReal : HDiv ChargeUnit ChargeUnit NNReal

Equations

• ChargeUnit.instHDivNNReal = { hDiv := fun (x t : ChargeUnit) => ⟨x.val / t.val, ⋯⟩ }

theorem ChargeUnit.div_eq_val (x y : ChargeUnit) : x / y = ⟨x.val / y.val, ⋯⟩

@[simp]

theorem ChargeUnit.div_neq_zero (x y : ChargeUnit) : ¬x / y = 0

@[simp]

theorem ChargeUnit.div_pos (x y : ChargeUnit) : 0 < x / y

@[simp]

theorem ChargeUnit.div_self (x : ChargeUnit) : x / x = 1

theorem ChargeUnit.div_symm (x y : ChargeUnit) : x / y = (y / x)⁻¹

@[simp]

theorem ChargeUnit.div_mul_div_coe (x y z : ChargeUnit) : ↑(x / y) * ↑(y / z) = ↑(x / z)

The scaling of a charge unit

def ChargeUnit.scale (r : ℝ) (x : ChargeUnit) (hr : 0 < r := by norm_num) : ChargeUnit

The scaling of a charge unit by a positive real.

Equations

• ChargeUnit.scale r x hr = { val := r * x.val, property := ⋯ }

@[simp]

theorem ChargeUnit.scale_div_self (x : ChargeUnit) (r : ℝ) (hr : 0 < r) : scale r x hr / x = ⟨r, ⋯⟩

@[simp]

theorem ChargeUnit.self_div_scale (x : ChargeUnit) (r : ℝ) (hr : 0 < r) : x / scale r x hr = ⟨1 / r, ⋯⟩

@[simp]

theorem ChargeUnit.scale_one (x : ChargeUnit) : scale 1 x ⋯ = x

@[simp]

theorem ChargeUnit.scale_div_scale (x1 x2 : ChargeUnit) {r1 r2 : ℝ} (hr1 : 0 < r1) (hr2 : 0 < r2) : scale r1 x1 hr1 / scale r2 x2 hr2 = ⟨r1, ⋯⟩ / ⟨r2, ⋯⟩ * (x1 / x2)

@[simp]

theorem ChargeUnit.scale_scale (x : ChargeUnit) (r1 r2 : ℝ) (hr1 : 0 < r1) (hr2 : 0 < r2) : scale r1 (scale r2 x hr2) hr1 = scale (r1 * r2) x ⋯

Specific choices of charge units

We define specific choices of charge units. We first define the notion of a columb to correspond to the charge unit with underlying value equal to 1. This is really down to a choice in the isomorphism between the set of metrics on the charge manifold and the positive reals.

def ChargeUnit.coulombs : ChargeUnit

The definition of a charge unit of coulomb.

Equations

• ChargeUnit.coulombs = { val := 1, property := ChargeUnit.instInhabited._proof_1 }

noncomputable def ChargeUnit.elementaryCharge : ChargeUnit

The charge unit of a elementryCharge (1.602176634×10−19 coulomb).

Equations

• ChargeUnit.elementaryCharge = ChargeUnit.scale 1602176634e-28 ChargeUnit.coulombs ChargeUnit.elementaryCharge._proof_1