Two-way complementation: corners

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

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

theorem Complexity.FiniteAutomaton.Complementation.Internal.finite_subsemigroup_idempotent {A : Type u_1} [Semigroup A] [Finite A] (S : Set A) (hne : S.Nonempty) (hmul : ∀ x ∈ S, ∀ y ∈ S, x * y ∈ S) : ∃ e ∈ S, IsIdempotentElem e

A finite nonempty subsemigroup contains an idempotent.

theorem Complexity.FiniteAutomaton.Complementation.Internal.finite_idempotent_pow {A : Type u_1} [Monoid A] [Finite A] (a : A) : ∃ (k : ℕ), 0 < k ∧ IsIdempotentElem (a ^ k)

Every element of a finite monoid has an idempotent positive power.

theorem Complexity.FiniteAutomaton.Complementation.Internal.map_positive_pow {A : Type u_1} {B : Type u_2} [Monoid A] [Monoid B] (f : A →ₙ* B) (a : A) (k : ℕ) : f (a ^ (k + 1)) = f a ^ (k + 1)

A multiplicative map preserves positive powers without any unitality assumption.

theorem Complexity.FiniteAutomaton.Complementation.Internal.exists_nested_chain {A : Type u_1} [Monoid A] [Finite A] {m k : ℕ} (ι : A →ₙ* Diagram m) (b0 : A) (hb0 : IsIdempotentElem b0) (g : ℕ → A) (J : Set (Bool × Set (Fin m))) (hg : ∀ j < k, ι (g j) ∈ (ι b0).corner ∧ (ι b0).missing (ι (g j)) ⊆ J) : ∃ (b : ℕ → A), b 0 = b0 ∧ (∀ (j : ℕ), IsIdempotentElem (b j)) ∧ (∀ (j : ℕ), ∃ (n : ℕ), b (j + 1) = (b j * g j * b j) ^ (n + 1)) ∧ (∀ (j : ℕ), (ι (b (j + 1)), ι (b j)) ∈ Diagram.nesting m) ∧ (∀ j ≤ k, (ι b0).missing (ι (b j)) ⊆ J) ∧ ∑ j ∈ Finset.range k, ((ι (b j)).missing (ι (b (j + 1)))).ncard ≤ 2 * J.ncard

A nested chain with a common missing-set budget.

theorem Complexity.FiniteAutomaton.Complementation.Internal.minimal_idempotent_lift {A : Type u_1} {M : Type u_2} [Semigroup A] [Finite A] [Semigroup M] (θ : A →ₙ* M) (hθ : Function.Surjective ⇑θ) (q : M) (hq : IsIdempotentElem q) : ∃ (d : A), IsIdempotentElem d ∧ θ d = q ∧ ∀ (e : A), IsIdempotentElem e → θ e = q → e * d = e → d * e = e → e = d

An idempotent has a lift minimal in the nesting order.

@[instance_reducible]

instance Complexity.FiniteAutomaton.Complementation.Internal.cornerMonoid {A : Type u_1} [Semigroup A] {e : A} (he : IsIdempotentElem e) : Monoid he.Corner

Mathlib's semigroup corner, equipped with its idempotent as identity.

Equations

• One or more equations did not get rendered due to their size.

instance Complexity.FiniteAutomaton.Complementation.Internal.finite_corner {A : Type u_1} [Semigroup A] [Finite A] {e : A} (he : IsIdempotentElem e) : Finite he.Corner

def Complexity.FiniteAutomaton.Complementation.Internal.cornerMap {A : Type u_1} {M : Type u_2} [Semigroup A] [Semigroup M] (θ : A →ₙ* M) {d : A} {q : M} (hd : IsIdempotentElem d) (hq : IsIdempotentElem q) (hθd : θ d = q) : hd.Corner →* hq.Corner

A multiplicative map restricts to a unital map between matching idempotent corners.

Equations

• Complexity.FiniteAutomaton.Complementation.Internal.cornerMap θ hd hq hθd = { toFun := fun (x : hd.Corner) => ⟨θ ↑x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

theorem Complexity.FiniteAutomaton.Complementation.Internal.cornerMap_surjective {A : Type u_1} {M : Type u_2} [Semigroup A] [Semigroup M] (θ : A →ₙ* M) (hθ : Function.Surjective ⇑θ) {d : A} {q : M} (hd : IsIdempotentElem d) (hq : IsIdempotentElem q) (hθd : θ d = q) : Function.Surjective ⇑(cornerMap θ hd hq hθd)

theorem Complexity.FiniteAutomaton.Complementation.Internal.minimal_corner_reflects_units {A : Type u_1} {M : Type u_2} [Semigroup A] [Finite A] [Semigroup M] (θ : A →ₙ* M) {d : A} {q : M} (hd : IsIdempotentElem d) (hq : IsIdempotentElem q) (hθd : θ d = q) (hminimal : ∀ (e : A), IsIdempotentElem e → θ e = q → e * d = e → d * e = e → e = d) (w : hd.Corner) (hw : IsUnit ((cornerMap θ hd hq hθd) w)) : IsUnit w

At a minimal idempotent lift, every element with unit image is a unit.

def Complexity.FiniteAutomaton.Complementation.Internal.cornerFlatten {M : Type u_1} [Semigroup M] {p : M} (hp : IsIdempotentElem p) (q : hp.Corner) (hq : IsIdempotentElem q) : hq.Corner ≃* ⋯.Corner

Taking a corner inside an absorbing corner gives the same smaller corner.

Equations

• One or more equations did not get rendered due to their size.