Oddomorphisms
Lax461425.Oddomorphisms · concepts/Lax461425/Oddomorphisms.lean · lax-461425
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
Let and be graphs and a homomorphism. A vertex is -even if is even for every , and -odd if it is odd for every such . The homomorphism is an oddomorphism if
- every vertex is -even or -odd, and
- for every , the fibre contains an odd number of -odd vertices.
The homomorphism is a weak oddomorphism if there is a subgraph such that the restriction is an oddomorphism. These notions are due to Roberson.
A class of finite simple graphs is closed under weak oddomorphisms if whenever and there is a weak oddomorphism .
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Combinatorics.SimpleGraph.Maps |
| 2 | import Mathlib.Combinatorics.SimpleGraph.Subgraph |
| 3 | import Mathlib.Data.Set.Card |
| 4 | import Lax871432.GraphClasses |
| 5 | |
| 6 | /-! |
| 7 | --- |
| 8 | title: Oddomorphisms |
| 9 | type: definition |
| 10 | --- |
| 11 | Let and be graphs and a homomorphism. A vertex |
| 12 | is *-even* if is even for every |
| 13 | , and *-odd* if it is odd for every such . The homomorphism |
| 14 | is an *oddomorphism* if |
| 15 | |
| 16 | 1. every vertex is -even or -odd, and |
| 17 | 2. for every , the fibre contains an odd number of -odd |
| 18 | vertices. |
| 19 | |
| 20 | The homomorphism is a *weak oddomorphism* if there is a subgraph such |
| 21 | that the restriction is an oddomorphism. These notions are due |
| 22 | to Roberson. |
| 23 | |
| 24 | A class of finite simple graphs is *closed under weak oddomorphisms* if |
| 25 | whenever and there is a weak oddomorphism |
| 26 | . |
| 27 | -/ |
| 28 | |
| 29 | namespace Lax461425.Oddomorphisms |
| 30 | |
| 31 | open Lax871432.GraphClasses |
| 32 | |
| 33 | variable {V W : Type*} {F : SimpleGraph V} {G : SimpleGraph W} |
| 34 | |
| 35 | /-- The neighbours of `a` in `F` that `φ` maps to `x`, i.e. `N_F(a) ∩ φ⁻¹(x)`. -/ |
| 36 | def neighborsOver (φ : F →g G) (a : V) (x : W) : Set V := |
| 37 | {b | F.Adj a b ∧ φ b = x} |
| 38 | |
| 39 | /-- `a` is `φ`-even: it has an even number of neighbours over every neighbour of `φ a`. -/ |
| 40 | def IsEven (φ : F →g G) (a : V) : Prop := |
| 41 | ∀ x, G.Adj (φ a) x → Even (neighborsOver φ a x).ncard |
| 42 | |
| 43 | /-- `a` is `φ`-odd: it has an odd number of neighbours over every neighbour of `φ a`. -/ |
| 44 | def IsOdd (φ : F →g G) (a : V) : Prop := |
| 45 | ∀ x, G.Adj (φ a) x → Odd (neighborsOver φ a x).ncard |
| 46 | |
| 47 | /-- `φ` is an oddomorphism: every vertex is `φ`-even or `φ`-odd, and every fibre contains an |
| 48 | odd number of `φ`-odd vertices. -/ |
| 49 | structure IsOddomorphism (φ : F →g G) : Prop where |
| 50 | even_or_odd : ∀ a, IsEven φ a ∨ IsOdd φ a |
| 51 | odd_card_fibre : ∀ x, Odd {a | φ a = x ∧ IsOdd φ a}.ncard |
| 52 | |
| 53 | /-- `φ` is a weak oddomorphism: its restriction to some subgraph of `F` is an oddomorphism. -/ |
| 54 | def IsWeakOddomorphism (φ : F →g G) : Prop := |
| 55 | ∃ F' : F.Subgraph, IsOddomorphism (φ.comp F'.hom) |
| 56 | |
| 57 | /-- `𝓕` is closed under weak oddomorphisms: the target of a weak oddomorphism from a member |
| 58 | is a member. -/ |
| 59 | def IsWeakOddomorphismClosed (𝓕 : GraphClass) : Prop := |
| 60 | ∀ {V W : Type} [Finite V] [Finite W] {F : SimpleGraph V} {G : SimpleGraph W} (φ : F →g G), |
| 61 | IsWeakOddomorphism φ → 𝓕.Mem F → 𝓕.Mem G |
| 62 | |
| 63 | end Lax461425.Oddomorphisms |
| 64 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments