ImageBound.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TwoWayComplementation.single_edge_cost line 12

Source documentation

Exponential cost of a single edge for every finite source monoid and label type.

theorem single_edge_cost (h : ℕ) :
    ∀ {A : Type u} {H : Type v} [Monoid A] [Finite A] [Finite H] {m : ℕ},
      Nat.card H = h → 2 ≤ h →
      ∀ (ι : A →ₙ* Diagram m) (φ : A →* RelationMonoid H), Function.Surjective φ →
      (∀ a b, (ι a, ι b) ∈ Diagram.inclusion m → (φ b).toRel ⊆ (φ a).toRel) →
      (∀ σ : Equiv.Perm H, ∃ p : Aˣ, φ p = (permutationUnit σ).val) →
      ∀ a, IsIdempotentElem a → ∀ x y : H, x ≠ y →
      (φ a).toRel = SetRel.id ∪ {(x, y)} →
      lossBound h ≤ ((ι 1).missing (ι a)).ncard := by
…

Mentions: OAI.TwoWayComplementation.Diagram, OAI.TwoWayComplementation.RelationMonoid, OAI.TwoWayComplementation.Diagram.inclusion, OAI.TwoWayComplementation.permutationUnit, OAI.TwoWayComplementation.lossBound

theorem OAI.TwoWayComplementation.minimal_unital_corner line 180

Source documentation

A surjection has a unital identity corner with unit lifts for every target unit.

theorem minimal_unital_corner {A M : Type*} [Semigroup A] [Finite A] [Monoid M]
    (θ : A →ₙ* M) (hθ : Function.Surjective θ) :
    ∃ d : A, ∃ hd : IsIdempotentElem d, ∃ ψ : hd.Corner →* M,
      Function.Surjective ψ ∧ (∀ w, ψ w = θ w.val) ∧
      ∀ u : Mˣ, ∃ p : hd.Cornerˣ, ψ p = u.val := by
…

theorem OAI.TwoWayComplementation.identity_pair_idempotent line 209
Source documentation
Identity plus a single pair is always an idempotent relation.
```
theorem identity_pair_idempotent {H : Type*} (x y : H) :
    IsIdempotentElem (RelationMonoid.ofRel (SetRel.id ∪ {(x, y)})) := by
…
```
Mentions: OAI.TwoWayComplementation.RelationMonoid.ofRel

theorem OAI.TwoWayComplementation.order_reversing_image_bound_finite line 219

Source documentation

A surjective order-reversing multiplicative image has exponential cost.

theorem order_reversing_image_bound_finite {H : Type*} [Finite H]
    (m : ℕ) (_hm : 1 ≤ m) (hh : 2 ≤ Nat.card H)
    (S : Set (Diagram m)) (hidentity : Diagram.identity m ∈ S)
    (hclosed : ∀ ⦃a b⦄, a ∈ S → b ∈ S → Diagram.comp a b ∈ S)
    (φ : S → SetRel H H) (hsurj : Function.Surjective φ)
    (hmul : ∀ a b : S,
      φ ⟨Diagram.comp a.val b.val, hclosed a.property b.property⟩ = φ a ○ φ b)
    (hreverse : ∀ a b : S, (a.val, b.val) ∈ Diagram.inclusion m → φ b ⊆ φ a) :
    lossBound (Nat.card H) ≤ 2 * m := by
…

Mentions: OAI.TwoWayComplementation.Diagram, OAI.TwoWayComplementation.Diagram.identity, OAI.TwoWayComplementation.Diagram.comp, OAI.TwoWayComplementation.Diagram.inclusion, OAI.TwoWayComplementation.lossBound

theorem OAI.TwoWayComplementation.order_reversing_image_bound line 268

Source documentation

The order-reversing image bound for a finite label domain.

theorem order_reversing_image_bound
    (m h : ℕ) (_hm : 1 ≤ m) (hh : 2 ≤ h)
    (S : Set (Diagram m)) (hidentity : Diagram.identity m ∈ S)
    (hclosed : ∀ ⦃a b⦄, a ∈ S → b ∈ S → Diagram.comp a b ∈ S)
    (φ : S → SetRel (Fin h) (Fin h)) (hsurj : Function.Surjective φ)
    (hmul : ∀ a b : S,
      φ ⟨Diagram.comp a.val b.val, hclosed a.property b.property⟩ = φ a ○ φ b)
    (hreverse : ∀ a b : S, (a.val, b.val) ∈ Diagram.inclusion m → φ b ⊆ φ a) :
    lossBound h ≤ 2 * m := by
…