The tight binding chain

i. Overview

The tight binding chain corresponds to an electron in motion in a 1d solid with the assumption the electron can sit only on the atoms of the solid.

The solid is assumed to consist of N sites with a separation of a between them

Mathematically, the tight binding chain corresponds to a QM problem located on a lattice with only self and nearest neighbour interactions, with periodic boundary conditions.

ii. Key results

• TightBindingChain : The physical parameters making up the tight binding chain.
• localizedState : The orthonormal basis of localized states.
• hamiltonian : The Hamiltonian of the tight binding chain.
• BrillouinZone : The Brillouin zone of the tight binding chain.
• QuantaWaveNumber : The quantized wavenumbers of the energy eigenstates.
• energyEigenstate : The energy eigenstates of the tight binding chain.
• energyEigenvalue : The energy eigenvalues of the tight binding chain.
• hamiltonian_energyEigenstate : The Hamiltonian acting on an energy eigenstate gives the corresponding energy eigenvalue times the energy eigenstate.

iii. Table of contents

• A. The setup
  • A.1. The input data for the tight binding chain
  • A.2. The Hilbert space
• B. The localized states
  • B.1. The orthonormal basis of localized states
  • B.2. Notation for localized states
  • B.3. Orthonormality of the localized states
• C. The operator |m⟩⟨n|
  • C.1. Definition of the operator |m⟩⟨n|
  • C.2. Notation for the operator |m⟩⟨n|
  • C.3. The operator |m⟩⟨n| applied to a localized state
• D. The Hamiltonian of the tight binding chain
  • D.1. Hermiticity of the Hamiltonian
  • D.2. Hamiltonian applied to a localized state
  • D.3. Mean energy of a localized state
• E. The Brillouin zone and quantized wavenumbers
  • E.1. The Brillouin zone
  • E.2. The quantized wavenumbers of the energy eigenstates
  • E.3. Wavenumbers lie in the Brillouin zone
  • E.4. Expotentials related to the quantized wavenumbers
• F. The energy eigenstates and eigenvalues
  • F.1. The energy eigenstates
  • F.2. Orthonormality of the energy eigenstates
  • F.3. The energy eigenvalues
  • F.4. The time-independent Schrodinger equation

iv. References

• https://www.damtp.cam.ac.uk/user/tong/aqm/aqmtwo.pdf

A. The setup

A.1. The input data for the tight binding chain

structure CondensedMatter.TightBindingChain : Type

The physical parameters making up the tight binding chain.

• N : ℕ

  The number of sites, or atoms, in the chain

• N_ne_zero : NeZero self.N
• a : ℝ

  The distance between the sites

• a_pos : 0 < self.a
• E0 : ℝ

  The energy associate with a particle sitting at a fixed site.

• t : ℝ

  The hopping parameter.

instance CondensedMatter.TightBindingChain.instNeZeroNatN (T : TightBindingChain) : NeZero T.N

A.2. The Hilbert space

@[reducible, inline]

abbrev CondensedMatter.TightBindingChain.HilbertSpace (T : TightBindingChain) : Type

The Hilbert space of a TightBindingchain is the N-dimensional finite dimensional Hilbert space.

Equations

• T.HilbertSpace = QuantumMechanics.FiniteHilbertSpace T.N

B. The localized states

Localized states correspond to the electron being located on a specific site in the chain.

B.1. The orthonormal basis of localized states

noncomputable def CondensedMatter.TightBindingChain.localizedState {T : TightBindingChain} : OrthonormalBasis (Fin T.N) ℂ T.HilbertSpace

The eigenstate corresponding to the particle been located on the nth site.

Equations

• CondensedMatter.TightBindingChain.localizedState = EuclideanSpace.basisFun (Fin T.N) ℂ

B.2. Notation for localized states

def CondensedMatter.TightBindingChain.«term|_⟩» : Lean.ParserDescr

The eigenstate corresponding to the particle been located on the nth site.

Equations

• One or more equations did not get rendered due to their size.

def CondensedMatter.TightBindingChain.«term⟨_|_⟩» : Lean.ParserDescr

The inner product of two localized states.

Equations

• One or more equations did not get rendered due to their size.

B.3. Orthonormality of the localized states

theorem CondensedMatter.TightBindingChain.localizedState_orthonormal (T : TightBindingChain) : Orthonormal ℂ ⇑localizedState

The localized states are normalized.

theorem CondensedMatter.TightBindingChain.localizedState_orthonormal_eq_ite (T : TightBindingChain) (m n : Fin T.N) : inner ℂ (localizedState m) (localizedState n) = if m = n then 1 else 0

C. The operator |m⟩⟨n|

C.1. Definition of the operator |m⟩⟨n|

noncomputable def CondensedMatter.TightBindingChain.localizedComp {T : TightBindingChain} (m n : Fin T.N) : T.HilbertSpace →ₗ[ℂ] T.HilbertSpace

The linear map |m⟩⟨n| for ⟨n| localized states.

Equations

• One or more equations did not get rendered due to their size.

C.2. Notation for the operator |m⟩⟨n|

def CondensedMatter.TightBindingChain.«term|_⟩⟨_|» : Lean.ParserDescr

The linear map |m⟩⟨n| for ⟨n| localized states.

Equations

• One or more equations did not get rendered due to their size.

C.3. The operator |m⟩⟨n| applied to a localized state

theorem CondensedMatter.TightBindingChain.localizedComp_apply_localizedState (T : TightBindingChain) (m n p : Fin T.N) : (localizedComp m n) (localizedState p) = if n = p then localizedState m else 0

D. The Hamiltonian of the tight binding chain

noncomputable def CondensedMatter.TightBindingChain.hamiltonian (T : TightBindingChain) : T.HilbertSpace →ₗ[ℂ] T.HilbertSpace

The Hamiltonian of the tight binding chain with periodic boundary conditions is given by E₀ ∑ n, |n⟩⟨n| - t ∑ n, (|n⟩⟨n + 1| + |n + 1⟩⟨n|). The periodic boundary conditions is manifested by the + in n + 1 being within Fin T.N (that is modulo T.N).

Equations

• One or more equations did not get rendered due to their size.

D.1. Hermiticity of the Hamiltonian

theorem CondensedMatter.TightBindingChain.hamiltonian_hermitian (T : TightBindingChain) (ψ φ : T.HilbertSpace) : inner ℂ (T.hamiltonian ψ) φ = inner ℂ ψ (T.hamiltonian φ)

The hamiltonian of the tight binding chain is hermitian.

D.2. Hamiltonian applied to a localized state

theorem CondensedMatter.TightBindingChain.hamiltonian_apply_localizedState (T : TightBindingChain) (n : Fin T.N) : T.hamiltonian (localizedState n) = ↑T.E0 • localizedState n - ↑T.t • (localizedState (n + 1) + localizedState (n - 1))

The Hamiltonian applied to the localized state |n⟩ gives T.E0 • |n⟩ - T.t • (|n + 1⟩ + |n - 1⟩).

D.3. Mean energy of a localized state

theorem CondensedMatter.TightBindingChain.energy_localizedState (T : TightBindingChain) (n : Fin T.N) (htn : 1 < T.N) : inner ℂ (localizedState n) (T.hamiltonian (localizedState n)) = ↑T.E0

The energy of a localized state in the tight binding chain is E0. This lemma assumes that there is more then one site in the chain otherwise the result is not true.

E. The Brillouin zone and quantized wavenumbers

E.1. The Brillouin zone

def CondensedMatter.TightBindingChain.BrillouinZone (T : TightBindingChain) : Set ℝ

The Brillouin zone of the tight binding model is [-π/a, π/a). This is the set in which wave functions are uniquely defined.

Equations

• T.BrillouinZone = Set.Ico (-Real.pi / T.a) (Real.pi / T.a)

E.2. The quantized wavenumbers of the energy eigenstates

def CondensedMatter.TightBindingChain.QuantaWaveNumber (T : TightBindingChain) : Set ℝ

The wavenumbers associated with the energy eigenstates. This corresponds to the set 2 π / (a N) * (n - ⌊N/2⌋) for n : Fin T.N. It is defined as such so it sits in the Brillouin zone.

Equations

• T.QuantaWaveNumber = {x : ℝ | ∃ (n : Fin T.N), 2 * Real.pi / (T.a * ↑T.N) * (↑↑n - ↑(T.N / 2)) = x}

E.3. Wavenumbers lie in the Brillouin zone

theorem CondensedMatter.TightBindingChain.quantaWaveNumber_subset_brillouinZone (T : TightBindingChain) : T.QuantaWaveNumber ⊆ T.BrillouinZone

The quantized wavenumbers form a subset of the BrillouinZone.

E.4. Expotentials related to the quantized wavenumbers

theorem CondensedMatter.TightBindingChain.quantaWaveNumber_exp_N (T : TightBindingChain) (n : ℕ) (k : ↑T.QuantaWaveNumber) : Complex.exp (Complex.I * ↑↑k * ↑n * ↑T.N * ↑T.a) = 1

theorem CondensedMatter.TightBindingChain.quantaWaveNumber_exp_sub_one (T : TightBindingChain) (n : Fin T.N) (k : ↑T.QuantaWaveNumber) : Complex.exp (Complex.I * ↑↑k * ↑↑(n - 1) * ↑T.a) = Complex.exp (Complex.I * ↑↑k * ↑↑n * ↑T.a) * Complex.exp (-Complex.I * ↑↑k * ↑T.a)

theorem CondensedMatter.TightBindingChain.quantaWaveNumber_exp_add_one (T : TightBindingChain) (n : Fin T.N) (k : ↑T.QuantaWaveNumber) : Complex.exp (Complex.I * ↑↑k * ↑↑(n + 1) * ↑T.a) = Complex.exp (Complex.I * ↑↑k * ↑↑n * ↑T.a) * Complex.exp (Complex.I * ↑↑k * ↑T.a)

F. The energy eigenstates and eigenvalues

F.1. The energy eigenstates

noncomputable def CondensedMatter.TightBindingChain.energyEigenstate (T : TightBindingChain) (k : ↑T.QuantaWaveNumber) : T.HilbertSpace

The energy eigenstates of the tight binding chain They are given by ∑ n, exp (I * k * n * T.a) • |n⟩.

Equations

• T.energyEigenstate k = ∑ n : Fin T.N, Complex.exp (Complex.I * ↑↑k * ↑↑n * ↑T.a) • CondensedMatter.TightBindingChain.localizedState n

F.2. Orthonormality of the energy eigenstates

theorem CondensedMatter.TightBindingChain.energyEigenstate_orthogonal (T : TightBindingChain) : Pairwise fun (k1 k2 : ↑T.QuantaWaveNumber) => inner ℂ (T.energyEigenstate k1) (T.energyEigenstate k2) = 0

The energy eigenstates of the tight binding chain are orthogonal.

F.3. The energy eigenvalues

noncomputable def CondensedMatter.TightBindingChain.energyEigenvalue (T : TightBindingChain) (k : ↑T.QuantaWaveNumber) : ℝ

The energy eigenvalue of the tight binding chain for a k in QuantaWaveNumber is E0 - 2 * t * Real.cos (k * T.a).

Equations

• T.energyEigenvalue k = T.E0 - 2 * T.t * Real.cos (↑k * T.a)

F.4. The time-independent Schrodinger equation

theorem CondensedMatter.TightBindingChain.hamiltonian_energyEigenstate (T : TightBindingChain) (k : ↑T.QuantaWaveNumber) : T.hamiltonian (T.energyEigenstate k) = T.energyEigenvalue k • T.energyEigenstate k

The energy eigenstates satisfy the time-independent Schrodinger equation.