Grace/Cumulus/GraphTheory/Multigraph/Doubling.g17

Open in Workbench Download source

Imports

Multigraph.Trees · Combinatorics.Basics

Declarations

Source

1-- The multigraph with every edge doubled: the edges are the pairs (e, i)2-- with i ∈ 2 and the ends of e, cuts double in size, and an edge set of the3-- doubled graph projects back to the edges with a copy in it.4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.GraphTheory.Multigraph.Doubling10import Multigraph.Trees11import Combinatorics.Basics1213-- Section: The graph with every edge doubled.1415-- Every edge doubled: the edges are the pairs (e, i) with i ∈ 2, with the16-- ends of e.17def doubledEdges (E : Set) : Set := E × 218def doubledEnd (V E endpoint : Set) : Set :=19  { p ∈ (E × 2) × V | ∃ e ∈ E, ∃ i ∈ 2, p = ((e, i), endpoint(e)) }2021-- The doubled end of (e, i) is the end of e.22theorem doubledEnd.function (V E endpoint : Set)23  requires function : endpoint : E → V24  shows doubledEnd(V, E, endpoint) : E × 2 → V25proof26  constructor27  . intros p member28    exact member.left29  constructor30  . intros x y relatedY z relatedZ31    obtain ⟨_, e, _, i, _, shapeY⟩ := relatedY32    obtain ⟨_, f, _, j, _, shapeZ⟩ := relatedZ33    obtain ⟨xY, valueY⟩ := orderedPair.injective with shapeY34    obtain ⟨xZ, valueZ⟩ := orderedPair.injective with shapeZ35    have pairs : (e, i) = (f, j) by cc36    obtain ⟨same, _⟩ := orderedPair.injective with pairs37    cc38  . intros x input39    obtain ⟨_, e, he, i, hi, rfl⟩ := product.membership.forward with input40    have vertex := FunctionBetween.apply_closed with function, he41    witness endpoint(e)42    refine ⟨vertex, _⟩43    exact doubledEnd.membership.backward44      with ⟨(product.pair with input, vertex), e, he, i, hi, rfl⟩4546theorem doubledEnd.value (V E endpoint e i : Set)47  requires function : endpoint : E → V48  requires edge : e ∈ E49  requires side : i ∈ 250  shows doubledEnd(V, E, endpoint)((e, i)) = endpoint(e)51proof52  have input : (e, i) ∈ E × 2 := product.pair with edge, side53  have vertex := FunctionBetween.apply_closed with function, edge54  have related : relates(doubledEnd(V, E, endpoint), (e, i), endpoint(e)) :=55    doubledEnd.membership.backward56      with ⟨(product.pair with input, vertex), e, edge, i, side, rfl⟩57  exact FunctionBetween.apply_value58    with (doubledEnd.function with function), input, related5960theorem doubled.graph (V E leftEnd rightEnd : Set)61  requires graph : Graph(V, E, leftEnd, rightEnd)62  shows Graph(V, doubledEdges(E), doubledEnd(V, E, leftEnd),63    doubledEnd(V, E, rightEnd))64proof65  unfold doubledEdges66  exact ⟨(doubledEnd.function with graph.left),67    (doubledEnd.function with graph.right)⟩6869-- The edges of the doubled graph leaving X are the two copies of each edge70-- of G leaving X.71theorem doubled.crossing (V E leftEnd rightEnd X : Set)72  requires graph : Graph(V, E, leftEnd, rightEnd)73  shows crossing(doubledEnd(V, E, leftEnd), doubledEnd(V, E, rightEnd),74    doubledEdges(E), X) = crossing(leftEnd, rightEnd, E, X) × 275proof76  unfold doubledEdges77  ext p78  constructor79  . intro hp80    obtain ⟨inProduct, sides⟩ := hp81    obtain ⟨_, e, he, i, hi, rfl⟩ :=82      product.membership.forward with inProduct83    rw [(doubledEnd.value with graph.left, he, hi),84      (doubledEnd.value with graph.right, he, hi)] at sides85    exact product.pair with ⟨he, sides⟩, hi86  . intro hp87    obtain ⟨_, e, he, i, hi, rfl⟩ := product.membership.forward with hp88    obtain ⟨inE, sides⟩ := he89    refine ⟨(product.pair with inE, hi), _⟩90    rw [(doubledEnd.value with graph.left, inE, hi),91      (doubledEnd.value with graph.right, inE, hi)]92    exact sides9394theorem doubled.edge_connected (V E leftEnd rightEnd : Set, k : Nat)95  requires graph : Graph(V, E, leftEnd, rightEnd)96  requires finiteEdges : Finite(E)97  requires connected : EdgeConnected(V, E, leftEnd, rightEnd, k)98  shows EdgeConnected(V, doubledEdges(E), doubledEnd(V, E, leftEnd),99    doubledEnd(V, E, rightEnd), 2 * k)100proof101  intros X bound nonempty proper102  have many := connected with X, bound, nonempty, proper103  have finiteCut := crossing.finite at leftEnd, rightEnd, E, X104    with finiteEdges105  rw [(doubled.crossing with graph),106    (cardinality.product_count with finiteCut, (Finite.natural at 2)),107    (cardinality.natural at 2)]108  arith109110-- Section: Projecting doubled edge sets back to G.111112-- The edges of G with a copy in a set S of doubled edges: the image of S113-- under the projection to the edge, so no larger than S.114def projected (E S : Set) : Set := { e ∈ E | ∃ i ∈ 2, (e, i) ∈ S }115116defgraph copyEdge (E : Set) (p ∈ E × 2) : E := fst(p)117proof118  obtain ⟨_, e, he, i, hi, rfl⟩ := product.membership.forward with member119  rw fst.pair120  exact he121122theorem projected.count (E S : Set)123  requires finiteEdges : Finite(E)124  requires subset : S ⊆ E × 2125  shows cardinality(projected(E, S)) ≤ cardinality(S)126proof127  have function := copyEdge.function at E128  have finiteS := Finite.subset129    with (Finite.product with finiteEdges, Finite.natural), subset130  have same : projected(E, S) = functionImage(copyEdge(E), S, E)131    ext e132    constructor133    . intro he134      obtain ⟨inE, i, hi, inS⟩ := he135      refine ⟨inE, (e, i), inS, _⟩136      rw [(copyEdge.value with (subset with (e, i), inS)), fst.pair]137    . intro he138      obtain ⟨inE, p, hp, shape⟩ := he139      obtain ⟨_, f, hf, i, hi, rfl⟩ :=140        product.membership.forward with (subset with p, hp)141      rw [(copyEdge.value with (subset with (f, i), hp)), fst.pair] at shape142      rw shape143      exact ⟨hf, i, hi, hp⟩144  rw same145  exact cardinality.image_le with function, subset, finiteS146147-- The projections of a family of doubled edge sets, as a function on 3.148defgraph projectedTrees (E T : Set) (i ∈ 3) : 𝒫(E) := projected(E, T(i))149proof150  apply powerset.membership_iff.backward151  intros e he152  exact he.left153