While this submission is a draft, it cannot be used by other submissions.

Oddomorphisms

Lax461425.Oddomorphisms · concepts/Lax461425/Oddomorphisms.lean · lax-461425

definition

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    Let FF and GG be graphs and φ ⁣:F→G\varphi \colon F \to G a homomorphism. A vertex a∈V(F)a \in V(F) is φ\varphi-even if ∣NF(a)∩φ−1(x)∣|N_F(a) \cap \varphi^{-1}(x)| is even for every x∈NG(φ(a))x \in N_G(\varphi(a)), and φ\varphi-odd if it is odd for every such xx. The homomorphism φ\varphi is an oddomorphism if

    1. every vertex a∈V(F)a \in V(F) is φ\varphi-even or φ\varphi-odd, and
    2. for every x∈V(G)x \in V(G), the fibre φ−1(x)\varphi^{-1}(x) contains an odd number of φ\varphi-odd vertices.

    The homomorphism φ\varphi is a weak oddomorphism if there is a subgraph F′⊆FF' \subseteq F such that the restriction φ∣F′ ⁣:F′→G\varphi|_{F'} \colon F' \to G is an oddomorphism. These notions are due to Roberson.

    A class F\mathcal{F} of finite simple graphs is closed under weak oddomorphisms if G∈FG \in \mathcal{F} whenever F∈FF \in \mathcal{F} and there is a weak oddomorphism F→GF \to G.

    Concept map
    2 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Maps
    2import Mathlib.Combinatorics.SimpleGraph.Subgraph
    3import Mathlib.Data.Set.Card
    4import Lax871432.GraphClasses
    5
    6/-!
    7---
    8title: Oddomorphisms
    9type: definition
    10---
    11Let FF and GG be graphs and φ ⁣:F→G\varphi \colon F \to G a homomorphism. A vertex
    12a∈V(F)a \in V(F) is *φ\varphi-even* if ∣NF(a)∩φ−1(x)∣|N_F(a) \cap \varphi^{-1}(x)| is even for every
    13x∈NG(φ(a))x \in N_G(\varphi(a)), and *φ\varphi-odd* if it is odd for every such xx. The homomorphism
    14φ\varphi is an *oddomorphism* if
    15
    161. every vertex a∈V(F)a \in V(F) is φ\varphi-even or φ\varphi-odd, and
    172. for every x∈V(G)x \in V(G), the fibre φ−1(x)\varphi^{-1}(x) contains an odd number of φ\varphi-odd
    18 vertices.
    19
    20The homomorphism φ\varphi is a *weak oddomorphism* if there is a subgraph F′⊆FF' \subseteq F such
    21that the restriction φ∣F′ ⁣:F′→G\varphi|_{F'} \colon F' \to G is an oddomorphism. These notions are due
    22to Roberson.
    23
    24A class F\mathcal{F} of finite simple graphs is *closed under weak oddomorphisms* if
    25G∈FG \in \mathcal{F} whenever F∈FF \in \mathcal{F} and there is a weak oddomorphism
    26F→GF \to G.
    27-/
    28
    29namespace Lax461425.Oddomorphisms
    30
    31open Lax871432.GraphClasses
    32
    33variable {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)`. -/
    36def 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`. -/
    40def 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`. -/
    44def 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
    48odd number of `φ`-odd vertices. -/
    49structure 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. -/
    54def 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
    58is a member. -/
    59def 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
    63end Lax461425.Oddomorphisms
    64

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…