Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax132576.HomomorphismComplement

The complement of a homomorphism is rational

concepts/Lax132576/HomomorphismComplement.lean · lax-132576

proven

Loading review…

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.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    Theorem

    If h:A∗→B∗h : A^* \to B^* is a string homomorphism, then its complement

    {(w,v)∈A∗×B∗∣v≠h(w)}\{(w, v) \in A^* \times B^* \mid v \neq h(w)\}

    is a rational relation (Claim B.1.7 of Transducers). The automaton guesses a prefix of the input on which the homomorphism is applied correctly, then insists on an error at the next letter: it outputs a proper prefix of the image of that letter and nothing more, or a string incomparable with it and then anything. This is the observation behind the undecidability of equivalence (Theorem B.1.6).

    Lean source view on GitHub

    1import Lax132576.RationalRelations
    2import Lax132576.StringHomomorphisms
    3
    4/-!
    5---
    6title: The complement of a homomorphism is rational
    7type: theorem
    8---
    9If h:A∗→B∗h : A^* \to B^* is a string homomorphism, then its complement
    10{(w,v)∈A∗×B∗∣v≠h(w)}\{(w, v) \in A^* \times B^* \mid v \neq h(w)\}
    11is a rational relation (Claim B.1.7 of *Transducers*). The automaton guesses a
    12prefix of the input on which the homomorphism is applied correctly, then
    13insists on an error at the next letter: it outputs a proper prefix of the image
    14of that letter and nothing more, or a string incomparable with it and then
    15anything. This is the observation behind the undecidability of equivalence
    16(Theorem B.1.6).
    17
    18# Formalization notes
    19
    20Both alphabets are assumed finite, as in the book; the automaton has one
    21transition per letter and per prefix of its image.
    22-/
    23
    24namespace Lax132576.HomomorphismComplement
    25
    26open Lax132576.RationalRelations Lax132576.StringHomomorphisms
    27
    28/-- The complement of the graph of a string homomorphism is a rational relation. -/
    29axiom isRationalRel_ne_homOf {A B : Type} [Finite A] [Finite B] (φ : A → List B) :
    30 IsRationalRel (fun (w : List A) (v : List B) => v ≠ homOf φ w)
    31
    32end Lax132576.HomomorphismComplement
    33
    Show Proof

    Formalization notes

    Both alphabets are assumed finite, as in the book; the automaton has one transition per letter and per prefix of its image.

    Builds on

    Used by

    none

    From Mathlib

    none

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…