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 = ⊤

def SimpleGraph.Walk.pathGraphHomToSubgraph {V : Type u_3} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) : pathGraph (w.length + 1) →g w.toSubgraph.coe

The subgraph of a walk contains the path graph with the same number of vertices

Equations

• w.pathGraphHomToSubgraph = { toFun := fun (n : Fin (w.length + 1)) => ⟨w.support[n], ⋯⟩, map_rel' := ⋯ }

def SimpleGraph.Walk.pathGraphHom {V : Type u_3} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) : pathGraph (w.length + 1) →g G

A walk induces a homomorphism from a path graph to the graph

Equations

• w.pathGraphHom = w.toSubgraph.hom.comp w.pathGraphHomToSubgraph

def SimpleGraph.Walk.IsPath.pathGraphIsoToSubgraph {V : Type u_3} [DecidableEq V] {G : SimpleGraph V} {u v : V} {w : G.Walk u v} (hw : w.IsPath) : pathGraph (w.length + 1) ≃g w.toSubgraph.coe

The subgraph of a path is isomorphic to the path graph with the same number of vertices

Equations

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

def SimpleGraph.Walk.IsPath.pathGraphCopy {V : Type u_3} [DecidableEq V] {G : SimpleGraph V} {u v : V} {w : G.Walk u v} (hw : w.IsPath) : (pathGraph (w.length + 1)).Copy G

A path induces an injective homomorphism from a path graph to the graph

Equations

• hw.pathGraphCopy = w.toSubgraph.coeCopy.comp hw.pathGraphIsoToSubgraph.toCopy

theorem SimpleGraph.Walk.IsPath.isContained_pathGraph {V : Type u_3} {G : SimpleGraph V} {u v : V} {w : G.Walk u v} (hw : w.IsPath) : (pathGraph (w.length + 1)).IsContained G