Two-way complementation: relation monoid

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/TwoWayAutomata/RelationMonoid.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

def Complexity.FiniteAutomaton.Complementation.Internal.restrictedIdentity {α : Type u_1} (F : Set α) : SetRel α α

Identity restricted to the retained points.

Equations

• Complexity.FiniteAutomaton.Complementation.Internal.restrictedIdentity F = {(x, y) : α × α | x = y ∧ x ∈ F}

@[simp]

theorem Complexity.FiniteAutomaton.Complementation.Internal.restrictedIdentity_comp_self {α : Type u_1} (F : Set α) : (restrictedIdentity F).comp (restrictedIdentity F) = restrictedIdentity F

theorem Complexity.FiniteAutomaton.Complementation.Internal.singleton_context {α : Type u_1} (R : SetRel α α) (p q : α) : ((restrictedIdentity {p}).comp R).comp (restrictedIdentity {q}) = {(x, y) : α × α | x = p ∧ y = q ∧ (p, q) ∈ R}

Singleton contexts test an individual relation edge.

theorem Complexity.FiniteAutomaton.Complementation.Internal.relation_corner_identities {α : Type u_1} (P i : SetRel α α) (hP : P.comp P = P) (hiPi : (i.comp P).comp i = i) : have Q := (P.comp i).comp P; Q.comp Q = Q ∧ P.comp Q = Q ∧ Q.comp P = Q ∧ Q.comp i = P.comp i ∧ i.comp Q = i.comp P ∧ (i.comp Q).comp i = i

Restriction-corner identities. The supporting relation i can be any idempotent with iPi = i.

theorem Complexity.FiniteAutomaton.Complementation.Internal.relation_corner_inverse {α : Type u_1} (P i : SetRel α α) (hP : P.comp P = P) (hiPi : (i.comp P).comp i = i) : (∀ (Z : SetRel α α), (((P.comp i).comp P).comp Z).comp ((P.comp i).comp P) = Z → (P.comp ((i.comp Z).comp i)).comp P = Z) ∧ ∀ (A : SetRel α α), (i.comp A).comp i = A → (((P.comp i).comp P).comp ((P.comp A).comp P)).comp ((P.comp i).comp P) = (P.comp A).comp P ∧ (i.comp ((P.comp A).comp P)).comp i = A

Restriction and extension are inverse on the two supported corners.

theorem Complexity.FiniteAutomaton.Complementation.Internal.relation_corner_comp {α : Type u_1} (P i A B : SetRel α α) (hP : P.comp P = P) (hi : i.comp i = i) (hiPi : (i.comp P).comp i = i) (hA : (i.comp A).comp i = A) (hB : (i.comp B).comp i = B) : ((P.comp A).comp P).comp ((P.comp B).comp P) = (P.comp (A.comp B)).comp P

Extension preserves products on the supported relation corner.

@[reducible, inline]

abbrev Complexity.FiniteAutomaton.Complementation.Internal.RelationMonoid (H : Type u_1) : Type u_1

Relations in path order, using the opposite of Mathlib's endomorphism monoid.

Equations

• Complexity.FiniteAutomaton.Complementation.Internal.RelationMonoid H = (CategoryTheory.End (have this := H; this))ᵐᵒᵖ

def Complexity.FiniteAutomaton.Complementation.Internal.RelationMonoid.ofRel {H : Type u_1} (R : SetRel H H) : RelationMonoid H

Regard a binary relation as a path-ordered endomorphism.

Equations

• Complexity.FiniteAutomaton.Complementation.Internal.RelationMonoid.ofRel R = MulOpposite.op { rel := R }

def Complexity.FiniteAutomaton.Complementation.Internal.RelationMonoid.toRel {H : Type u_1} (R : RelationMonoid H) : SetRel H H

The underlying binary relation.

Equations

• R.toRel = (MulOpposite.unop R).rel

theorem Complexity.FiniteAutomaton.Complementation.Internal.RelationMonoid.ext {H : Type u_1} {R S : RelationMonoid H} (h : R.toRel = S.toRel) : R = S

theorem Complexity.FiniteAutomaton.Complementation.Internal.RelationMonoid.ext_iff {H : Type u_1} {R S : RelationMonoid H} : R = S ↔ R.toRel = S.toRel

@[simp]

theorem Complexity.FiniteAutomaton.Complementation.Internal.RelationMonoid.toRel_ofRel {H : Type u_1} (R : SetRel H H) : (ofRel R).toRel = R

@[simp]

theorem Complexity.FiniteAutomaton.Complementation.Internal.RelationMonoid.toRel_mul {H : Type u_1} (R S : RelationMonoid H) : (R * S).toRel = R.toRel.comp S.toRel

@[simp]

theorem Complexity.FiniteAutomaton.Complementation.Internal.RelationMonoid.toRel_one {H : Type u_1} : toRel 1 = SetRel.id

theorem Complexity.FiniteAutomaton.Complementation.Internal.relation_extend_restrict {H : Type u_1} (F : Set H) (R : SetRel ↑F ↑F) : {xy : ↑F × ↑F | (↑xy.1, ↑xy.2) ∈ Prod.map Subtype.val Subtype.val '' R} = R

Extending a relation on a subset and restricting it again loses no pairs.

theorem Complexity.FiniteAutomaton.Complementation.Internal.relation_restrict_extend {H : Type u_1} (F : Set H) (R : SetRel H H) : Prod.map Subtype.val Subtype.val '' {xy : ↑F × ↑F | (↑xy.1, ↑xy.2) ∈ R} = ((restrictedIdentity F).comp R).comp (restrictedIdentity F)

Extension of restriction is precisely the identity sandwich on the subset.

theorem Complexity.FiniteAutomaton.Complementation.Internal.relation_extend_comp {H : Type u_1} (F : Set H) (A B : SetRel ↑F ↑F) : Prod.map Subtype.val Subtype.val '' A.comp B = SetRel.comp (Prod.map Subtype.val Subtype.val '' A) (Prod.map Subtype.val Subtype.val '' B)

Extension of relations on a subset preserves path composition.

theorem Complexity.FiniteAutomaton.Complementation.Internal.relation_corner_equiv {H : Type u_1} (P : SetRel H H) (F : Set H) (hP : P.comp P = P) (hiPi : ((restrictedIdentity F).comp P).comp (restrictedIdentity F) = restrictedIdentity F) : ∃ (hQ : IsIdempotentElem (RelationMonoid.ofRel ((P.comp (restrictedIdentity F)).comp P))) (ρ : hQ.Corner ≃* RelationMonoid ↑F), ∀ (Z : hQ.Corner), (ρ Z).toRel = {xy : ↑F × ↑F | (↑xy.1, ↑xy.2) ∈ (↑Z).toRel}

The full relation monoid on a subset is the compressed relation corner.