Catalog/Sparsity/ShallowMinorComposition/Contract.lean
| 1 | import Catalog.Sparsity.Preliminaries.Contract |
| 2 | import Catalog.Sparsity.ShallowMinor.Contract |
| 3 | import Catalog.Sparsity.NowhereDense.Contract |
| 4 | |
| 5 | open Catalog.Sparsity.ShallowMinor |
| 6 | open Catalog.Sparsity.NowhereDense |
| 7 | open Catalog.Sparsity.Preliminaries |
| 8 | |
| 9 | namespace Catalog.Sparsity.ShallowMinorComposition |
| 10 | |
| 11 | /-- The depth-`d` reduct of a graph class `C`: the class of all graphs |
| 12 | that are depth-`d` shallow minors of some graph in `C`. (Def 2.13) -/ |
| 13 | def ShallowReduct (C : GraphClass) (d : ℕ) : GraphClass := |
| 14 | fun {V : Type} [DecidableEq V] [Fintype V] (H : SimpleGraph V) => |
| 15 | ∃ (W : Type) (_ : DecidableEq W) (_ : Fintype W) (G : SimpleGraph W), |
| 16 | C G ∧ IsShallowMinor H G d |
| 17 | |
| 18 | /-- Lemma 2.12: Composition of shallow minors. |
| 19 | If J ≼_b H and H ≼_a G, then J ≼_{2ab+a+b} G. -/ |
| 20 | axiom shallowMinor_trans |
| 21 | {V W U : Type} {J : SimpleGraph U} {H : SimpleGraph W} {G : SimpleGraph V} |
| 22 | {a b : ℕ} : |
| 23 | IsShallowMinor J H b → IsShallowMinor H G a → |
| 24 | IsShallowMinor J G (2 * a * b + a + b) |
| 25 | |
| 26 | /-- Corollary 2.14: If C is nowhere dense, then C ∇ d is nowhere dense. -/ |
| 27 | axiom nowhereDense_shallowReduct (C : GraphClass) (d : ℕ) : |
| 28 | IsNowhereDense C → IsNowhereDense (ShallowReduct C d) |
| 29 | |
| 30 | end Catalog.Sparsity.ShallowMinorComposition |
| 31 |