RelationMonoid.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TwoWayComplementation.restrictedIdentity line 10
Source documentation
Identity restricted to the retained points.
```
def restrictedIdentity {α : Type*} (F : Set α) : SetRel α α :=
…
```
theorem OAI.TwoWayComplementation.restrictedIdentity_comp_self line 14

theorem OAI.TwoWayComplementation.singleton_context line 20

Source documentation

Singleton contexts test an individual relation edge.

theorem singleton_context {α : Type*} (R : SetRel α α) (p q : α) :
    restrictedIdentity {p} ○ R ○ restrictedIdentity {q} =
      {(x, y) | x = p ∧ y = q ∧ (p, q) ∈ R} := by
…

Mentions: OAI.TwoWayComplementation.restrictedIdentity

theorem OAI.TwoWayComplementation.relation_corner_identities line 29
Source documentation
Restriction-corner identities. The supporting relation i can be any idempotent with iPi = i.
```
theorem relation_corner_identities {α : Type*} (P i : SetRel α α)
    (hP : P ○ P = P) (hiPi : i ○ P ○ i = i) :
    let Q := P ○ i ○ P
…
```

theorem OAI.TwoWayComplementation.relation_corner_inverse line 42

Source documentation

Restriction and extension are inverse on the two supported corners.

theorem relation_corner_inverse {α : Type*} (P i : SetRel α α)
    (hP : P ○ P = P) (hiPi : i ○ P ○ i = i) :
    (∀ Z, (P ○ i ○ P) ○ Z ○ (P ○ i ○ P) = Z → P ○ (i ○ Z ○ i) ○ P = Z) ∧
    (∀ A, i ○ A ○ i = A →
      (P ○ i ○ P) ○ (P ○ A ○ P) ○ (P ○ i ○ P) = P ○ A ○ P ∧
      i ○ (P ○ A ○ P) ○ i = A) := by
…

theorem OAI.TwoWayComplementation.relation_corner_comp line 72

Source documentation

Extension preserves products on the supported relation corner.

theorem relation_corner_comp {α : Type*} (P i A B : SetRel α α)
    (hP : P ○ P = P) (hi : i ○ i = i) (hiPi : i ○ P ○ i = i)
    (hA : i ○ A ○ i = A) (hB : i ○ B ○ i = B) :
    (P ○ A ○ P) ○ (P ○ B ○ P) = P ○ (A ○ B) ○ P := by
…

abbrev OAI.TwoWayComplementation.RelationMonoid line 87
Source documentation
Relations in path order, using the opposite of Mathlib's endomorphism monoid.
```
abbrev RelationMonoid (H : Type*) :=
…
```
def OAI.TwoWayComplementation.RelationMonoid.ofRel line 93
Source documentation
Regard a binary relation as a path-ordered endomorphism.
```
def ofRel {H : Type*} (R : SetRel H H) : RelationMonoid H :=
…
```
Mentions: OAI.TwoWayComplementation.RelationMonoid
def OAI.TwoWayComplementation.RelationMonoid.toRel line 97
Source documentation
The underlying binary relation.
```
def toRel {H : Type*} (R : RelationMonoid H) : SetRel H H := R.unop.rel
…
```
Mentions: OAI.TwoWayComplementation.RelationMonoid
theorem OAI.TwoWayComplementation.RelationMonoid.ext line 100
theorem OAI.TwoWayComplementation.RelationMonoid.toRel_ofRel line 104
theorem OAI.TwoWayComplementation.RelationMonoid.toRel_mul line 107
theorem OAI.TwoWayComplementation.RelationMonoid.toRel_one line 111

theorem OAI.TwoWayComplementation.relation_extend_restrict line 116

Source documentation

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

theorem relation_extend_restrict {H : Type*} (F : Set H) (R : SetRel F F) :
    {xy : F × F | (xy.1.val, xy.2.val) ∈ (Prod.map Subtype.val Subtype.val) '' R} = R := by
…

theorem OAI.TwoWayComplementation.relation_restrict_extend line 127

Source documentation

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

theorem relation_restrict_extend {H : Type*} (F : Set H) (R : SetRel H H) :
    (Prod.map Subtype.val Subtype.val) '' {xy : F × F | (xy.1.val, xy.2.val) ∈ R} =
      restrictedIdentity F ○ R ○ restrictedIdentity F := by
…

Mentions: OAI.TwoWayComplementation.restrictedIdentity

theorem OAI.TwoWayComplementation.relation_extend_comp line 140

Source documentation

Extension of relations on a subset preserves path composition.

theorem relation_extend_comp {H : Type*} (F : Set H) (A B : SetRel F F) :
    (Prod.map Subtype.val Subtype.val) '' (A ○ B) =
      ((Prod.map Subtype.val Subtype.val) '' A) ○
        ((Prod.map Subtype.val Subtype.val) '' B) := by
…

theorem OAI.TwoWayComplementation.relation_corner_equiv line 158

Source documentation

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

theorem relation_corner_equiv {H : Type*} (P : SetRel H H) (F : Set H)
    (hP : P ○ P = P) (hiPi : restrictedIdentity F ○ P ○ restrictedIdentity F =
      restrictedIdentity F) :
    ∃ hQ : IsIdempotentElem (RelationMonoid.ofRel (P ○ restrictedIdentity F ○ P)),
      ∃ ρ : hQ.Corner ≃* RelationMonoid F,
        ∀ Z, (ρ Z).toRel = {xy : F × F | (xy.1.val, xy.2.val) ∈ Z.val.toRel} := by
…

Mentions: OAI.TwoWayComplementation.restrictedIdentity, OAI.TwoWayComplementation.RelationMonoid.ofRel, OAI.TwoWayComplementation.RelationMonoid