Corners.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.OneWayLiveness.exists_idempotent_power line 8

Source documentation

Positive powers in any finite monoid contain an idempotent.

lemma exists_idempotent_power {M : Type*} [Monoid M] [Finite M] (a : M) :
    ∃ n : ℕ, 0 < n ∧ a ^ n * a ^ n = a ^ n := by
…

structure OAI.OneWayLiveness.Corner line 22
Source documentation
The local monoid at an idempotent, with its genuine local identity.
```
@[ext] structure Corner {M : Type*} [Monoid M] (e : M) (he : e * e = e) where
…
```
instance OAI.OneWayLiveness.Corner.(instance at line 29) line 29
instance OAI.OneWayLiveness.Corner.(instance at line 30) line 30
lemma OAI.OneWayLiveness.Corner.val_one line 36
lemma OAI.OneWayLiveness.Corner.val_mul line 37
instance OAI.OneWayLiveness.Corner.(instance at line 38) line 38
def OAI.OneWayLiveness.Corner.sandwich line 40
lemma OAI.OneWayLiveness.Corner.val_pow_pos line 43
lemma OAI.OneWayLiveness.isUnit_of_injective_map_finite line 51
def OAI.OneWayLiveness.Corner.mapTo line 68
lemma OAI.OneWayLiveness.Corner.mapTo_val line 73
lemma OAI.OneWayLiveness.Corner.mapTo_surjective line 76
lemma OAI.OneWayLiveness.Corner.val_idempotent line 84
lemma OAI.OneWayLiveness.Pairing.image_idempotent line 95
def OAI.OneWayLiveness.Pairing.reduceHom line 97
lemma OAI.OneWayLiveness.Pairing.reduceHom_injective line 106
lemma OAI.OneWayLiveness.Pairing.reduceHom_rank line 113
lemma OAI.OneWayLiveness.Pairing.reduceHom_common_support line 116
lemma OAI.OneWayLiveness.Pairing.rank_pow_le line 125

lemma OAI.OneWayLiveness.exists_idempotent_lift line 133

Source documentation

A lift of an idempotent can always be made idempotent without changing its image.

lemma exists_idempotent_lift {M N : Type*} [Monoid M] [Monoid N] [Finite M]
    (f : M →* N) (hf : Function.Surjective f) (q : N) (hq : q * q = q) :
    ∃ e : M, e * e = e ∧ f e = q := by
…

lemma OAI.OneWayLiveness.exists_min_rank_lift line 142

lemma OAI.OneWayLiveness.min_rank_corner_isUnit line 153

Source documentation

Minimum rank over the local identity forces all local unit lifts to be units.

lemma min_rank_corner_isUnit {M N A : Type*} [Monoid M] [Monoid N] [Finite M] [Fintype A]
    (ρ : M →* Pairing (A ⊕ A)) (hρ : Function.Injective ρ)
    (f : M →* N) (e : M) (he : e * e = e) (q : N) (hq : q * q = q) (hf : f e = q)
    (hmin : ∀ z : M, z * z = z → f z = q → Pairing.rank (ρ e) ≤ Pairing.rank (ρ z))
    (y : Corner e he) (hy : IsUnit (Corner.mapTo (he := he) (hq := hq) f hf y)) : IsUnit y := by
…

Mentions: OAI.OneWayLiveness.Pairing, OAI.OneWayLiveness.Pairing.rank, OAI.OneWayLiveness.Corner, OAI.OneWayLiveness.Corner.mapTo

def OAI.OneWayLiveness.Corner.transfer line 182
Source documentation
Transport a local monoid across a split pair.
```
def transfer (u v : M) (huv : u * v = e) (hvu : v * u = f)
    (hu : u * f = u) (hv : f * v = v) : Corner e he →* Corner f hf where
…
```
Mentions: OAI.OneWayLiveness.Corner
def OAI.OneWayLiveness.Corner.equivOfSplit line 197