2.1. The tight binding chain🔗

2.1.1. Introduction🔗

The tight binding chain is corresponds to a finite dimensional quantum mechanical system.

It consists of a chain of N sites seperated by a distance a, and a particle, often described as an electron, which can occupy each site. The energy of the electron sitting at a given site is E_0, and a paramter p describes the tunneling of the electron between neighbouring sites.

These parameters are defined within the TightBindingChain structure.

structure

CondensedMatter.TightBindingChain : Type
CondensedMatter.TightBindingChain : Type

The physical parameters making up the tight binding chain.

Constructor

CondensedMatter.TightBindingChain.mk

Fields

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.

The hilbert space is the finite dimensional space of N-dimensional vectors.

def

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

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

The state corresponding to the electron being at site n is defined as

def

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

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

The notation |n⟩ is used to denote this state.

These localized states are orthonormal:

theorem

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

The localized states are normalized.

The linear map |m⟩⟨n| is given by

def

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

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

The hamiltonian is then given by

def

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

The Hamiltonian of the tight binding chain is given by E₀ ∑ n, |n⟩⟨n| - t ∑ n, (|n⟩⟨n + 1| + |n + 1⟩⟨n|), with periodic boundary conditions.

The energy of the localized state |n⟩ is given in the following theorem:

theorem

CondensedMatter.TightBindingChain.energy_localizedState
  (T : TightBindingChain) (n : Fin T.N) (htn : 1 < T.N) :
  inner (TightBindingChain.localizedState n)
      (T.hamiltonian (TightBindingChain.localizedState n)) =
    ↑T.E0
CondensedMatter.TightBindingChain.energy_localizedState
  (T : TightBindingChain) (n : Fin T.N)
  (htn : 1 < T.N) :
  inner
      (TightBindingChain.localizedState n)
      (T.hamiltonian
        (TightBindingChain.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.

The energy eigenfunctions are parameterized by a wavefunction sitting in the following set

def

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

The wavefunctions associated with the energy eigenstates.

The energy eigenfunctions are given by

def

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

The energy eigenstates of the tight binding chain.

The energy eigenvalues are given by

def

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

The energy eigenvalue of the tight binding chain for a k in the BrillouinZone.

They satisfy 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
CondensedMatter.TightBindingChain.hamiltonian_energyEigenstate
  (T : TightBindingChain)
  (k : ↑T.QuantaWaveNumber) :
  T.hamiltonian (T.energyEigenstate k) =
    T.energyEigenvalue k •
      T.energyEigenstate k

The eenergy eigenstates satisfy the time-independent Schrodinger equation.