Self-duality of the square lattice

DefinitionDual square lattice#✓fully proved

The dual square lattice. Its vertices are the face centres of ℤ², relabelled as integer points, so as a graph it is hypercubicLattice 2.

def dualLattice : SimpleGraph (Site 2) := hypercubicLattice 2

Uses 2 · Used by 3

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byBijection between primal and dual edges · Identity self-duality of the square lattice · Rotational self-duality of the square lattice

DefinitionQuarter-turn rotation of the square lattice#✓fully proved

The quarter-turn rotation (a, b) ↦ (-b, a) of ℤ².

def rot90Fun (x : Site 2) : Site 2 := ![- x 1, x 0]

Uses 1 · Used by 29

Statement usesSite of the hypercubic lattice

Used byTotal turning of a boundary orbit is bounded by its length · Successor of a boundary dart · Next boundary dart direction is rotated by the turn · Successor map on boundary darts · Face loop around the domino · Total turning of a closed orbit segment is divisible by four · Inner corner of a boundary dart · Walk along the first iterates of a boundary dart · Rotation of \(\mathbb{Z}^2\) by a number of quarter turns · Quarter-turn rotations form an action of \(\mathbb{Z}/4\) · Nontrivial quarter-turn rotations fix no lattice direction · Four quarter turns of the square lattice are the identity · Quarter turn between consecutive boundary darts modulo 4 · Signed quarter turn between consecutive boundary darts · Face loop around the unit cell · \(p_c(\mathbb{Z}^2) < 1\) under a no-pinch hypothesis · Box exterior embeds in the region graph · Quarter-turn isomorphism onto the region graph · Quarter-turn rotation as a permutation · Quarter-turn rotation as a lattice automorphism · Closed face walk of the canonical contour · Face walk along the first successors of a boundary dart · Unit face to the left of a dart · Face loop of a boundary orbit in the face-boundary graph · Face walk along a boundary orbit · Minimal-period face loop of the exit orbit · Face loop of the exit orbit of a finite cluster · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle

DefinitionInverse quarter-turn rotation#✓fully proved

The inverse quarter-turn rotation (a, b) ↦ (b, -a) of ℤ².

def rot90Inv (x : Site 2) : Site 2 := ![x 1, - x 0]

Uses 1 · Used by 3

Statement usesSite of the hypercubic lattice

Used byBox exterior embeds in the region graph · Quarter-turn isomorphism onto the region graph · Quarter-turn rotation as a permutation

DefinitionQuarter-turn rotation as a permutation#✓fully proved

The quarter-turn rotation as a permutation of ℤ².

def rot90Equiv : Site 2 ≃ Site 2 where
  toFun := rot90Fun
  invFun := rot90Inv
  left_inv := by intro x; funext i; fin_cases i <;> simp [rot90Fun, rot90Inv]
  right_inv := by intro x; funext i; fin_cases i <;> simp [rot90Fun, rot90Inv]

Uses 3 · Used by 8

Statement usesSite of the hypercubic lattice · Quarter-turn rotation of the square lattice · Inverse quarter-turn rotation

Used byWalk along the first iterates of a boundary dart · Box exterior embeds in the region graph · Quarter-turn isomorphism onto the region graph · Quarter-turn rotation of unordered site pairs · Quarter-turn rotation as a lattice automorphism · Face loop of a boundary orbit in the face-boundary graph · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle

DefinitionQuarter-turn rotation as a lattice automorphism#✓fully proved

The quarter-turn rotation as a graph automorphism of the square lattice.

def rot90Iso : hypercubicLattice 2 ≃g hypercubicLattice 2 :=
  ⟨rot90Equiv, fun {x y} => rot90_adj x y⟩

Uses 4 · Used by 2

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Quarter-turn rotation as a permutation · Quarter-turn rotation of the square lattice

Used byBijection between primal and dual edges · Rotational self-duality of the square lattice

DefinitionIdentity self-duality of the square lattice#✓fully proved

The identity isomorphism between the square lattice and its dual.

def selfDual : hypercubicLattice 2 ≃g dualLattice := SimpleGraph.Iso.refl

Uses 3

Statement usesSite of the hypercubic lattice · Dual square lattice · Hypercubic lattice \(\mathbb{Z}^d\)

DefinitionRotational self-duality of the square lattice#✓fully proved

The isomorphism between the square lattice and its dual given by the quarter-turn rotation.

def selfDualCross : hypercubicLattice 2 ≃g dualLattice := rot90Iso

Uses 4

Statement usesSite of the hypercubic lattice · Dual square lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Quarter-turn rotation as a lattice automorphism

DefinitionBijection between primal and dual edges#✓fully proved

The bijection between primal and dual edges induced by rot90Iso.

def crossingEdgeEquiv : (hypercubicLattice 2).edgeSet ≃ dualLattice.edgeSet :=
  rot90Iso.mapEdgeSet

Uses 4

Statement usesSite of the hypercubic lattice · Dual square lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Quarter-turn rotation as a lattice automorphism

DefinitionUnordered pairs under an equivalence#✓fully proved

An equivalence α ≃ β induces an equivalence of unordered pairs Sym2 α ≃ Sym2 β.

def sym2Congr {α β : Type*} (e : α ≃ β) : Sym2 α ≃ Sym2 β where
  toFun := Sym2.map e
  invFun := Sym2.map e.symm
  left_inv := by intro x; rw [Sym2.map_map]; simp
  right_inv := by intro x; rw [Sym2.map_map]; simp

Used by 4

Used byQuarter-turn rotation of unordered site pairs · Induced permutation of ghost-graph edges · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Unordered pairs of the extended set as window edges

DefinitionQuarter-turn rotation of unordered site pairs#✓fully proved

The bijection on unordered pairs of sites induced by the quarter-turn rotation (a, b) ↦ (-b, a). It maps lattice edges to lattice edges, but not to the dual edge crossing them: {(0,0), (1,0)} goes to {(0,0), (0,1)}. For the geometric crossing use sharedPrimalEdge.

def crossEdge : Sym2 (Site 2) ≃ Sym2 (Site 2) := sym2Congr rot90Equiv

Uses 3 · Used by 4

Statement usesSite of the hypercubic lattice · Quarter-turn rotation as a permutation · Unordered pairs under an equivalence

Used byBox exterior embeds in the region graph · Quarter-turn isomorphism onto the region graph · Rotated region graph of a lattice subgraph · Rotated dual configuration

DefinitionRotated dual configuration#✓fully proved

The configuration in which e is open exactly when the inverse quarter turn crossEdge.symm e of e is closed in ω. This is the dual configuration only up to the rotation: applying it twice gives the half-turn of ω (dualConfig_dualConfig), not ω.

def dualConfig (ω : ConfigSpace (Sym2 (Site 2))) : ConfigSpace (Sym2 (Site 2)) :=
  fun e => !(ω (crossEdge.symm e))

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Quarter-turn rotation of unordered site pairs

Used byDual left–right crossing of a rectangle · Dual bottom–top crossing of a rectangle

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.