Grace/Cumulus/GraphTheory/Multigraph/Quotient.g17

Open in Workbench Download source

Imports

Connectivity

Declarations

Source

1-- The quotient multigraph of a partition of the vertex set, in which every2-- class is one vertex and an edge keeps its identity: the class of a vertex,3-- refinement of partitions, and the edges crossing a set of classes.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.Quotient10import Connectivity1112-- The class of v: the union of the classes containing v, which under a13-- partition is the one class containing v.14def classesContaining (P v : Set) : Set := { X ∈ P | v ∈ X }15def classOf (P v : Set) : Set := ⋃(classesContaining(P, v))1617theorem classOf.membership (P v z : Set)18  shows z ∈ classOf(P, v) ↔ ∃ X ∈ P, v ∈ X ∧ z ∈ X19proof20  simp [classOf, classesContaining, union.membership]2122theorem classOf.eq_of_member (P v X : Set)23  requires apart : ∀ X ∈ P, ∀ Y ∈ P, X ≠ Y → Disjoint(X, Y)24  requires class : X ∈ P25  requires member : v ∈ X26  shows classOf(P, v) = X27proof28  ext z29  rw classOf.membership30  constructor31  . intro inUnion32    obtain ⟨Y, classY, vInY, inY⟩ := inUnion33    have same : X = Y34      by_contra different35      exact apart with X, class, Y, classY, different, v, member, vInY36    cc37  . intro inX38    exact ⟨X, class, member, inX⟩3940theorem classOf.member (V P v : Set)41  requires partition : Partition(V, P)42  requires vertex : v ∈ V43  shows classOf(P, v) ∈ P ∧ v ∈ classOf(P, v)44proof45  obtain ⟨X, class, member⟩ := partition.right.right with v, vertex46  rw classOf.eq_of_member with partition.right.left, class, member47  exact ⟨class, member⟩4849theorem classOf.eq_iff (V P u v : Set)50  requires partition : Partition(V, P)51  requires first : u ∈ V52  requires second : v ∈ V53  shows classOf(P, u) = classOf(P, v) ↔ (∃ X ∈ P, u ∈ X ∧ v ∈ X)54proof55  have apart := partition.right.left56  constructor57  . intro equal58    obtain ⟨X, classX, uInX⟩ := partition.right.right with u, first59    obtain ⟨Y, classY, vInY⟩ := partition.right.right with v, second60    have classU := classOf.eq_of_member with apart, classX, uInX61    have classV := classOf.eq_of_member with apart, classY, vInY62    witness X63    refine ⟨classX, uInX, _⟩64    cc65  . intro common66    obtain ⟨X, class, uInX, vInX⟩ := common67    have classU := classOf.eq_of_member with apart, class, uInX68    have classV := classOf.eq_of_member with apart, class, vInX69    cc7071-- A vertex lies in a union of classes exactly when its class is one of them.72theorem classOf.mem_union_iff (V P Y v : Set)73  requires partition : Partition(V, P)74  requires subfamily : Y ⊆ P75  requires vertex : v ∈ V76  shows v ∈ ⋃(Y) ↔ classOf(P, v) ∈ Y77proof78  have apart := partition.right.left79  constructor80  . intro inUnion81    obtain ⟨Z, inY, inZ⟩ := union.membership.forward with inUnion82    have classZ := subfamily with Z, inY83    rw classOf.eq_of_member with apart, classZ, inZ84    exact inY85  . intro inY86    obtain ⟨X, class, member⟩ := partition.right.right with v, vertex87    rw classOf.eq_of_member with apart, class, member at inY88    exact union.membership.backward with ⟨X, inY, member⟩8990-- A partition refines another when every class of the first lies in a class91-- of the second.92predicate Refines (P Q : Set) := ∀ X ∈ P, ∃ Y ∈ Q, X ⊆ Y9394-- The quotient multigraph: the vertices are the classes, and an edge joins95-- the classes of its ends. Edges inside a class become loops; the crossing96-- classes of F are its edges joining distinct classes.97def quotientEnd (E P endpoint : Set) : Set :=98  { p ∈ E × P | ∃ e ∈ E, p = (e, classOf(P, endpoint(e))) }99100def crossingClasses (P leftEnd rightEnd F : Set) : Set :=101  { e ∈ F | classOf(P, leftEnd(e)) ≠ classOf(P, rightEnd(e)) }102103theorem quotientEnd.relates (E P endpoint e X : Set)104  requires related : relates(quotientEnd(E, P, endpoint), e, X)105  shows e ∈ E ∧ X = classOf(P, endpoint(e))106proof107  obtain ⟨_, f, inE, equation⟩ := related108  obtain ⟨rfl, value⟩ := orderedPair.injective with equation109  exact ⟨inE, value⟩110111theorem quotientEnd.relates_class (V E P endpoint e : Set)112  requires function : endpoint : E → V113  requires partition : Partition(V, P)114  requires edge : e ∈ E115  shows relates(quotientEnd(E, P, endpoint), e, classOf(P, endpoint(e)))116proof117  have vertex := FunctionBetween.apply_closed with function, edge118  obtain ⟨class, _⟩ := classOf.member with partition, vertex119  exact quotientEnd.membership.backward120    with ⟨(product.pair with edge, class), e, edge, rfl⟩121122theorem quotientEnd.function (V E P endpoint : Set)123  requires function : endpoint : E → V124  requires partition : Partition(V, P)125  shows quotientEnd(E, P, endpoint) : E → P126proof127  constructor128  . intros p member129    exact member.left130  constructor131  . intros x y relatedY z relatedZ132    obtain ⟨_, valueY⟩ := quotientEnd.relates with relatedY133    obtain ⟨_, valueZ⟩ := quotientEnd.relates with relatedZ134    cc135  . intros x edge136    have vertex := FunctionBetween.apply_closed with function, edge137    obtain ⟨class, _⟩ := classOf.member with partition, vertex138    witness classOf(P, endpoint(x))139    exact ⟨class,140      (quotientEnd.relates_class with function, partition, edge)⟩141142theorem quotientEnd.graph (V E P leftEnd rightEnd : Set)143  requires graph : Graph(V, E, leftEnd, rightEnd)144  requires partition : Partition(V, P)145  shows Graph(P, E, quotientEnd(E, P, leftEnd), quotientEnd(E, P, rightEnd))146proof147  constructor148  . exact quotientEnd.function with graph.left, partition149  . exact quotientEnd.function with graph.right, partition150151theorem quotientEnd.value (V E P leftEnd rightEnd e : Set)152  requires graph : Graph(V, E, leftEnd, rightEnd)153  requires partition : Partition(V, P)154  requires edge : e ∈ E155  shows quotientEnd(E, P, leftEnd)(e) = classOf(P, leftEnd(e)) ∧156    quotientEnd(E, P, rightEnd)(e) = classOf(P, rightEnd(e))157proof158  constructor159  . exact FunctionBetween.apply_value with160      (quotientEnd.function with graph.left, partition), edge,161      (quotientEnd.relates_class with graph.left, partition, edge)162  . exact FunctionBetween.apply_value with163      (quotientEnd.function with graph.right, partition), edge,164      (quotientEnd.relates_class with graph.right, partition, edge)165166-- Edges within a class contribute nothing to crossing a union of classes, so167-- crossing in the quotient is crossing in the graph.168theorem crossing.quotient (V E P leftEnd rightEnd F Y : Set)169  requires graph : Graph(V, E, leftEnd, rightEnd)170  requires partition : Partition(V, P)171  requires edges : F ⊆ E172  requires classes : Y ⊆ P173  shows crossing(quotientEnd(E, P, leftEnd), quotientEnd(E, P, rightEnd), F, Y)174    = crossing(leftEnd, rightEnd, F, ⋃(Y))175proof176  ext e177  by_cases inF : e ∈ F178  . have inE := edges with e, inF179    obtain ⟨leftValue, rightValue⟩ :=180      quotientEnd.value with graph, partition, inE181    have leftIn := FunctionBetween.apply_closed with graph.left, inE182    have rightIn := FunctionBetween.apply_closed with graph.right, inE183    have leftIff := classOf.mem_union_iff with partition, classes, leftIn184    have rightIff := classOf.mem_union_iff with partition, classes, rightIn185    simp [crossing, leftValue, rightValue, leftIff, rightIff]186  . simp [crossing, inF]187188-- F connects the classes of P in the quotient when its crossing edges do: an189-- edge inside a class is a loop of the quotient and leaves no vertex set.190theorem Connects.quotient_iff (V E P leftEnd rightEnd F : Set)191  requires graph : Graph(V, E, leftEnd, rightEnd)192  requires partition : Partition(V, P)193  requires edges : F ⊆ E194  shows Connects(P, quotientEnd(E, P, leftEnd), quotientEnd(E, P, rightEnd), F)195    ↔ Connects(P, quotientEnd(E, P, leftEnd), quotientEnd(E, P, rightEnd),196      crossingClasses(P, leftEnd, rightEnd, F))197proof198  have crossingSubset : crossingClasses(P, leftEnd, rightEnd, F) ⊆ F199    intros e member200    exact member.left201  constructor202  . intros connected X classX Y classY A start closed203    have closedF : ClosedUnder(quotientEnd(E, P, leftEnd),204        quotientEnd(E, P, rightEnd), F, A)205      intros e inF206      by_cases same : classOf(P, leftEnd(e)) = classOf(P, rightEnd(e))207      . have inE := edges with e, inF208        obtain ⟨leftValue, rightValue⟩ :=209          quotientEnd.value with graph, partition, inE210        simp [leftValue, rightValue, same]211      . exact closed with e, ⟨inF, same⟩212    exact connected with X, classX, Y, classY, A, start, closedF213  . intros connected X classX Y classY214    have joined := connected with X, classX, Y, classY215    exact Joined.monotone with crossingSubset, joined216