The Hasse diagram as a graph

This file defines the Hasse diagram of an order (graph of CovBy, the covering relation) and the path graph on n vertices.

Main declarations

• SimpleGraph.hasse: Hasse diagram of an order.
• SimpleGraph.pathGraph: Path graph on n vertices.

def SimpleGraph.hasse (α : Type u_1) [Preorder α] : SimpleGraph α

The Hasse diagram of an order as a simple graph. The graph of the covering relation.

Equations

• SimpleGraph.hasse α = { Adj := fun (a b : α) => a ⋖ b ∨ b ⋖ a, symm := ⋯, loopless := ⋯ }

@[simp]

theorem SimpleGraph.hasse_adj {α : Type u_1} [Preorder α] {a b : α} : (hasse α).Adj a b ↔ a ⋖ b ∨ b ⋖ a

def SimpleGraph.hasseDualIso {α : Type u_1} [Preorder α] : hasse αᵒᵈ ≃g hasse α

αᵒᵈ and α have the same Hasse diagram.

Equations

• SimpleGraph.hasseDualIso = { toEquiv := OrderDual.ofDual, map_rel_iff' := ⋯ }

@[simp]

theorem SimpleGraph.hasseDualIso_apply {α : Type u_1} [Preorder α] (a : αᵒᵈ) : hasseDualIso a = OrderDual.ofDual a

@[simp]

theorem SimpleGraph.hasseDualIso_symm_apply {α : Type u_1} [Preorder α] (a : α) : hasseDualIso.symm a = OrderDual.toDual a

@[simp]

theorem SimpleGraph.hasse_prod (α : Type u_1) (β : Type u_2) [PartialOrder α] [PartialOrder β] : hasse (α × β) = hasse α □ hasse β

theorem SimpleGraph.hasse_preconnected_of_succ (α : Type u_1) [LinearOrder α] [SuccOrder α] [IsSuccArchimedean α] : (hasse α).Preconnected

theorem SimpleGraph.hasse_preconnected_of_pred (α : Type u_1) [LinearOrder α] [PredOrder α] [IsPredArchimedean α] : (hasse α).Preconnected

def SimpleGraph.pathGraph (n : ℕ) : SimpleGraph (Fin n)

The path graph on n vertices.

Equations

• SimpleGraph.pathGraph n = SimpleGraph.hasse (Fin n)

theorem SimpleGraph.pathGraph_adj {n : ℕ} {u v : Fin n} : (pathGraph n).Adj u v ↔ ↑u + 1 = ↑v ∨ ↑v + 1 = ↑u

theorem SimpleGraph.pathGraph_preconnected (n : ℕ) : (pathGraph n).Preconnected

theorem SimpleGraph.pathGraph_connected (n : ℕ) : (pathGraph (n + 1)).Connected

theorem SimpleGraph.pathGraph_two_eq_top : pathGraph 2 = ⊤