The infinite digraph space as an R1 instance (directed umbrella #84, D1 / issue #85)

Directed graphs are the one-sort, single binary relation, ordered-arguments, diagonal-permitted case of the generic relational carrier (R1). Rather than re-derive the topology / measurable structure, this file instantiates it: InfiniteDigraph is defined as the relational structure over digraphSig, so it inherits — with no new proofs — the compact / Polish / standard-Borel instances, the measurable finite restrictions, the cylinder π-system, and the finite-restriction measure extensionality of R1b. All topology lives on InfiniteDigraph; the bridge to Mathlib's Digraph is a plain carrier equivalence (Prop ≃ Bool classically), generic over the vertex type, so it yields both the infinite and the finite bridges (the latter for D2).

• digraphSig — the one-sort binary signature (arity 2, NoNullary);
• digraphStructureEquiv V — the carrier equivalence RelStructure digraphSig (fun _ => V) ≃ Digraph V, generic over V;
• InfiniteDigraph / FiniteDigraph n and the derived digraphEquiv / finiteDigraphEquiv;
• InfiniteDigraph.Adj (Prop, matching Mathlib graph APIs) and InfiniteDigraph.adjBit (Bool), reading adjacency off the ordered-pair coordinate;
• InfiniteDigraph.restrictFin and InfiniteDigraph.ext_of_map_restrictFin — the R1b finite restriction and measure extensionality, specialized (public statement over n : ℕ).

The projective extension / exchangeable-law theory is not here — that is D2 (#86) and R2.

@[reducible, inline]

abbrev digraphSig : RelSignature

The one-sort, single binary relation signature: arity 2, ordered arguments, the diagonal permitted (loops allowed).

Equations

• digraphSig = { Srt := Unit, Rel := Unit, arity := fun (x : Unit) => 2, argSort := fun (x : Unit) (x_1 : Fin 2) => () }

theorem digraphSig_noNullary : digraphSig.NoNullary

@[reducible, inline]

abbrev digraphCoord {V : Type u_1} (a b : V) : digraphSig.RelCoord fun (x : digraphSig.Srt) => V

The coordinate at an ordered vertex pair (a, b), over any vertex type.

Equations

• digraphCoord a b = ⟨(), ![a, b]⟩

def digraphCoordEquiv (V : Type u_1) : (digraphSig.RelCoord fun (x : digraphSig.Srt) => V) ≃ V × V

Coordinates are ordered vertex pairs (full square, diagonal included).

Equations

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

noncomputable def digraphStructureEquiv (V : Type u_1) : (digraphSig.RelStructure fun (x : digraphSig.Srt) => V) ≃ Digraph V

The carrier equivalence with Mathlib's Digraph V (Prop ≃ Bool classically), a plain type equivalence — the topology / measurable structure lives on the relational structure, not on Digraph V. A digraph is exactly an arbitrary Bool assignment to ordered vertex pairs.

Equations

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

@[simp]

theorem digraphStructureEquiv_adj {V : Type u_1} (G : digraphSig.RelStructure fun (x : digraphSig.Srt) => V) (a b : V) : ((digraphStructureEquiv V) G).Adj a b ↔ G (digraphCoord a b) = true

The infinite and finite digraph carriers

@[reducible, inline]

abbrev InfiniteDigraph : Type

The infinite digraph space: the relational structure over digraphSig with vertex set ℕ. Inherits the entire R1 topological / measurable structure.

Equations

• InfiniteDigraph = digraphSig.RelStructure digraphSig.Vinfinite

@[reducible, inline]

abbrev FiniteDigraph (n : ℕ) : Type

The finite digraph space on Fin n.

Equations

• FiniteDigraph n = digraphSig.RelStructure (RelSignature.Vfinite fun (x : digraphSig.Srt) => n)

noncomputable def digraphEquiv : InfiniteDigraph ≃ Digraph ℕ

The infinite carrier equivalence with Mathlib's Digraph ℕ.

Equations

• digraphEquiv = digraphStructureEquiv ℕ

noncomputable def finiteDigraphEquiv (n : ℕ) : FiniteDigraph n ≃ Digraph (Fin n)

The finite carrier equivalence with Mathlib's Digraph (Fin n) — the bridge D2 uses.

Equations

• finiteDigraphEquiv n = digraphStructureEquiv (Fin n)

@[simp]

theorem digraphCoord_map {V : Type u_1} {W : Type u_2} (f : V → W) (a b : V) : RelSignature.RelCoord.map (fun (x : digraphSig.Srt) => f) (digraphCoord a b) = digraphCoord (f a) (f b)

Coordinate naturality: the sortwise action of a vertex map sends the coordinate at an ordered pair to the coordinate at the image pair.

theorem digraphStructure_ext_iff {V : Type u_1} {G H : digraphSig.RelStructure fun (x : digraphSig.Srt) => V} : G = H ↔ ∀ (a b : V), G (digraphCoord a b) = H (digraphCoord a b)

Coordinate extensionality: two digraph structures agree once they agree at every ordered vertex pair — every relational coordinate of digraphSig is a digraphCoord.

def InfiniteDigraph.adjBit (G : InfiniteDigraph) (a b : ℕ) : Bool

Boolean adjacency: whether the ordered pair (a, b) stands in the relation.

Equations

• G.adjBit a b = G (digraphCoord a b)

def InfiniteDigraph.Adj (G : InfiniteDigraph) (a b : ℕ) : Prop

Adjacency (Prop-valued, matching Mathlib's graph APIs).

Equations

• G.Adj a b = (G.adjBit a b = true)

@[simp]

theorem InfiniteDigraph.adj_iff_adjBit (G : InfiniteDigraph) (a b : ℕ) : G.Adj a b ↔ G.adjBit a b = true

@[simp]

theorem InfiniteDigraph.digraphEquiv_adj (G : InfiniteDigraph) (a b : ℕ) : (digraphEquiv G).Adj a b ↔ G.Adj a b

Inherited finite restriction and measure extensionality

@[reducible, inline]

abbrev InfiniteDigraph.restrictFin (n : ℕ) : InfiniteDigraph → FiniteDigraph n

Finite restriction of an infinite digraph to the first n vertices (the R1b restrictFin, specialized).

Equations

• InfiniteDigraph.restrictFin n = RelSignature.RelStructure.restrictFin fun (x : digraphSig.Srt) => n

theorem InfiniteDigraph.measurable_restrictFin (n : ℕ) : Measurable (restrictFin n)

theorem InfiniteDigraph.ext_of_map_restrictFin {μ ν : MeasureTheory.Measure InfiniteDigraph} [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (n : ℕ), MeasureTheory.Measure.map (restrictFin n) μ = MeasureTheory.Measure.map (restrictFin n) ν) : μ = ν

Finite-restriction measure extensionality for infinite digraphs (R1b, specialized): two finite measures agree once their finite-restriction pushforwards agree, quantified over n : ℕ (the uniform size vector).