Corners.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TwoWayComplementation.finite_subsemigroup_idempotent line 10

Source documentation

A finite nonempty subsemigroup contains an idempotent.

theorem finite_subsemigroup_idempotent {A : Type*} [Semigroup A] [Finite A]
    (S : Set A) (hne : S.Nonempty) (hmul : ∀ x ∈ S, ∀ y ∈ S, x * y ∈ S) :
    ∃ e ∈ S, IsIdempotentElem e := by
…

theorem OAI.TwoWayComplementation.finite_idempotent_pow line 19
Source documentation
Every element of a finite monoid has an idempotent positive power.
```
theorem finite_idempotent_pow {A : Type*} [Monoid A] [Finite A] (a : A) :
    ∃ k : ℕ, 0 < k ∧ IsIdempotentElem (a ^ k) := by
…
```
theorem OAI.TwoWayComplementation.map_positive_pow line 28
Source documentation
A multiplicative map preserves positive powers without any unitality assumption.
```
theorem map_positive_pow {A B : Type*} [Monoid A] [Monoid B]
    (f : A →ₙ* B) (a : A) (k : ℕ) : f (a ^ (k + 1)) = f a ^ (k + 1) := by
…
```

theorem OAI.TwoWayComplementation.exists_nested_chain line 35

Source documentation

A nested chain with a common missing-set budget.

theorem exists_nested_chain {A : Type*} [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 := by
…

Mentions: OAI.TwoWayComplementation.Diagram, OAI.TwoWayComplementation.Diagram.nesting

theorem OAI.TwoWayComplementation.minimal_idempotent_lift line 100

Source documentation

An idempotent has a lift minimal in the nesting order.

theorem minimal_idempotent_lift {A M : Type*} [Semigroup A] [Finite A] [Semigroup M]
    (θ : A →ₙ* M) (hθ : Function.Surjective θ) (q : M) (hq : IsIdempotentElem q) :
    ∃ d, IsIdempotentElem d ∧ θ d = q ∧
      ∀ e, IsIdempotentElem e → θ e = q → e * d = e → d * e = e → e = d := by
…

instance OAI.TwoWayComplementation.cornerMonoid line 127
Source documentation
Mathlib's semigroup corner, equipped with its idempotent as identity.
```
instance cornerMonoid {A : Type*} [Semigroup A] {e : A} (he : IsIdempotentElem e) :
    Monoid he.Corner where
…
```
theorem OAI.TwoWayComplementation.finite_corner line 135

def OAI.TwoWayComplementation.cornerMap line 140

Source documentation

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

def cornerMap {A M : Type*} [Semigroup A] [Semigroup M] (θ : A →ₙ* M)
    {d : A} {q : M} (hd : IsIdempotentElem d) (hq : IsIdempotentElem q) (hθd : θ d = q) :
    hd.Corner →* hq.Corner where
…

theorem OAI.TwoWayComplementation.cornerMap_surjective line 149

theorem OAI.TwoWayComplementation.minimal_corner_reflects_units line 162

Source documentation

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

theorem minimal_corner_reflects_units {A M : Type*} [Semigroup A] [Finite A] [Semigroup M]
    (θ : A →ₙ* M) {d : A} {q : M} (hd : IsIdempotentElem d) (hq : IsIdempotentElem q)
    (hθd : θ d = q)
    (hminimal : ∀ e, 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 := by
…

Mentions: OAI.TwoWayComplementation.cornerMap

def OAI.TwoWayComplementation.cornerFlatten line 181

Source documentation

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

def cornerFlatten {M : Type*} [Semigroup M] {p : M} (hp : IsIdempotentElem p)
    (q : hp.Corner) (hq : IsIdempotentElem q) :
    hq.Corner ≃* (show IsIdempotentElem q.val from congrArg Subtype.val hq.eq).Corner := by
…