Skip to content

The contour of a hole-free planar set is a single cycle

5 fully proved

A. The double dual of the square lattice

DefinitionShift by \((-1, -1)\) identifying the double dual with \(\mathbb{Z}^2\)#✓fully proved

The shift x ↦ x - (1, 1) identifying the dual of the dual lattice with ℤ².

def phb_doubleDualShift (x : Site 2) : Site 2 := ![x 0 - 1, x 1 - 1]
Uses 1 · Used by 2
Statement usesSite of the hypercubic lattice
Used byShift by \((-1, -1)\) as an equivalence of \(\mathbb{Z}^2\) · Shift isomorphism: lattice minus barrier edges to face region graph

DefinitionShift by \((-1, -1)\) as an equivalence of \(\mathbb{Z}^2\)#✓fully proved

The shift by (-1, -1) as an equivalence of ℤ².

def phb_doubleDualEquiv : Site 2 ≃ Site 2 where
  toFun := phb_doubleDualShift
  invFun x := ![x 0 + 1, x 1 + 1]
  left_inv x := by
    funext i
    fin_cases i <;> simp [phb_doubleDualShift]
  right_inv x := by
    funext i
    fin_cases i <;> simp [phb_doubleDualShift]
Uses 2 · Used by 1
Statement usesSite of the hypercubic lattice · Shift by \((-1, -1)\) identifying the double dual with \(\mathbb{Z}^2\)
Used byShift isomorphism: lattice minus barrier edges to face region graph

DefinitionShift isomorphism: lattice minus barrier edges to face region graph#✓fully proved

The lattice minus the barrier edges of K is isomorphic, by the shift by (-1, -1), to the face region graph of the face-boundary graph of K.

StatMech.Lattice.phb_doubleDualIso · 22 lines 
noncomputable def phb_doubleDualIso (K : Set (Site 2)) :
    latticeMinusBarrier K ≃g whb_faceRegion (faceBoundaryGraph K) where
  toEquiv := phb_doubleDualEquiv
  map_rel_iff' := by
    intro x y
    change (whb_faceRegion (faceBoundaryGraph K)).Adj
        (phb_doubleDualShift x) (phb_doubleDualShift y) ↔
      (latticeMinusBarrier K).Adj x y
    rw [latticeMinusBarrier_adj, whb_faceRegion_adj]
    have hadj := phb_doubleDualShift_latAdj (x := x) (y := y)
    constructor
    · rintro ⟨hshift, hmem⟩
      have hxy := hadj.mp hshift
      refine ⟨hxy, ?_⟩
      rw [← phb_flankFaces_mem_faceBoundaryGraph_iff hxy,
        ← phb_sharedPrimalEdge_shift_eq_flankFaces hxy]
      exact hmem
    · rintro ⟨hxy, hbd⟩
      refine ⟨hadj.mpr hxy, ?_⟩
      rw [phb_sharedPrimalEdge_shift_eq_flankFaces hxy,
        phb_flankFaces_mem_faceBoundaryGraph_iff hxy]
      exact hbd
Uses 15 · Used by 3
Statement usesSite of the hypercubic lattice · Boundary edge of a set · Edge boundary of a set of sites · Edge with exactly one endpoint in a set · Face-boundary graph of a set · Two faces flanking a primal edge · Two faces flanking an unordered pair of sites · Hypercubic lattice \(\mathbb{Z}^d\) · Square lattice with the boundary edges of a set removed · Shift by \((-1, -1)\) as an equivalence of \(\mathbb{Z}^2\) · Shift by \((-1, -1)\) identifying the double dual with \(\mathbb{Z}^2\) · Primal edge shared by adjacent faces · Primal edge crossed by a dual edge · Primal edge crossed by an unordered pair of faces · Face-region graph of a square-lattice subgraph
Used byPlus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

B. The contour as a planar subgraph

DefinitionSupport of the face-boundary graph of a finite set#✓fully proved

The support of the face-boundary graph of a finite set K, as a finset.

noncomputable def phb_boundarySupport (K : Set (Site 2)) (hK : K.Finite) : Finset (Site 2) :=
  (phb_faceBoundaryGraph_support_finite K hK).toFinset
Uses 16 · Used by 3
Statement usesNearest neighbours in \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Boundary edge of a set · Boundary indicator of an edge · Nearest neighbours of a lattice site · Neighbour of a site in a coordinate direction · Four unit faces at a lattice site · Boundary degree of a unit face · Face-boundary graph of a set · Lower left corner of the unit face at \((a, b)\) · Upper left corner of the unit face at \((a, b)\) · Lower right corner of the unit face at \((a, b)\) · Upper right corner of the unit face at \((a, b)\) · Hypercubic lattice \(\mathbb{Z}^d\) · Primal edge shared by adjacent faces · Shift of a site along a coordinate
Used byPlus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionFace-boundary graph of a finite set as a planar subgraph#✓fully proved

The face-boundary graph of a finite set K, as a finite planar subgraph of ℤ².

noncomputable def phb_planarBoundary (K : Set (Site 2)) (hK : K.Finite) :
    PlanarZ2Subgraph where
  V := (faceBoundaryGraph K).support
  finV := (phb_faceBoundaryGraph_support_finite K hK).to_subtype
  decV := Classical.decEq _
  G := (faceBoundaryGraph K).induce (faceBoundaryGraph K).support
  emb := Function.Embedding.subtype _
  isSub := by
    intro x y hxy
    exact faceBoundaryGraph_le K hxy
Uses 17 · Used by 3
Statement usesNearest neighbours in \(\mathbb{Z}^d\) · Planar lattice subgraph of the square lattice · Site of the hypercubic lattice · Boundary edge of a set · Boundary indicator of an edge · Nearest neighbours of a lattice site · Neighbour of a site in a coordinate direction · Four unit faces at a lattice site · Boundary degree of a unit face · Face-boundary graph of a set · Lower left corner of the unit face at \((a, b)\) · Upper left corner of the unit face at \((a, b)\) · Lower right corner of the unit face at \((a, b)\) · Upper right corner of the unit face at \((a, b)\) · Hypercubic lattice \(\mathbb{Z}^d\) · Primal edge shared by adjacent faces · Shift of a site along a coordinate
Used byPlus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.