Mathlib.Logic.OpClass

Module docstring

{"# Typeclasses for commuting heterogeneous operations

The three classes in this file are for two-argument functions where one input is of type α, the output is of type β and the other input is of type α or β. They express the property that permuting arguments of type α does not change the result.

Main definitions

IsSymmOp: for op : α → α → β, op a b = op b a.
LeftCommutative: for op : α → β → β, op a₁ (op a₂ b) = op a₂ (op a₁ b).
RightCommutative: for op : β → α → β, op (op b a₁) a₂ = op (op b a₂) a₁. "}

IsSymmOp structure

(op : α → α → β)

Full source

/-- `IsSymmOp op` where `op : α → α → β` says that `op` is a symmetric operation,
i.e. `op a b = op b a`.
It is the natural generalisation of `Std.Commutative` (`β = α`) and `IsSymm` (`β = Prop`). -/
class IsSymmOp (op : α → α → β) : Prop where
  /-- A symmetric operation satisfies `op a b = op b a`. -/
  symm_op : ∀ a b, op a b = op b a

Symmetric Binary Operation

Informal description

The structure `IsSymmOp` asserts that a binary operation `op : α → α → β` is symmetric, meaning that for any two elements `a` and `b` of type `α`, the result of `op a b` is equal to `op b a`. This generalizes the notion of commutativity (when `β = α`) and symmetry (when `β = Prop`).

LeftCommutative structure

(op : α → β → β)

Full source

/-- `LeftCommutative op` where `op : α → β → β` says that `op` is a left-commutative operation,
i.e. `op a₁ (op a₂ b) = op a₂ (op a₁ b)`. -/
class LeftCommutative (op : α → β → β) : Prop where
  /-- A left-commutative operation satisfies `op a₁ (op a₂ b) = op a₂ (op a₁ b)`. -/
  left_comm : (a₁ a₂ : α) → (b : β) → op a₁ (op a₂ b) = op a₂ (op a₁ b)

Left-commutative operation

Informal description

A binary operation `op : α → β → β` is called left-commutative if for any elements `a₁, a₂ : α` and `b : β`, the equality `op a₁ (op a₂ b) = op a₂ (op a₁ b)` holds. This means that the order of operations with respect to the first argument can be swapped without changing the result.

RightCommutative structure

(op : β → α → β)

Full source

/-- `RightCommutative op` where `op : β → α → β` says that `op` is a right-commutative operation,
i.e. `op (op b a₁) a₂ = op (op b a₂) a₁`. -/
class RightCommutative (op : β → α → β) : Prop where
  /-- A right-commutative operation satisfies `op (op b a₁) a₂ = op (op b a₂) a₁`. -/
  right_comm : (b : β) → (a₁ a₂ : α) → op (op b a₁) a₂ = op (op b a₂) a₁

Right-commutative operation

Informal description

A binary operation $\mathrm{op} : \beta \to \alpha \to \beta$ is called *right-commutative* if for all $b \in \beta$ and $a_1, a_2 \in \alpha$, we have $\mathrm{op} (\mathrm{op} b a_1) a_2 = \mathrm{op} (\mathrm{op} b a_2) a_1$.

isSymmOp_of_isCommutative instance

(α : Sort u) (op : α → α → α) [Std.Commutative op] : IsSymmOp op

Full source

instance (priority := 100) isSymmOp_of_isCommutative (α : Sort u) (op : α → α → α)
    [Std.Commutative op] : IsSymmOp op where symm_op := Std.Commutative.comm

Commutative Operations are Symmetric

Informal description

For any type $\alpha$ and binary operation $\mathrm{op} : \alpha \to \alpha \to \alpha$ that is commutative (i.e., $\mathrm{op} a b = \mathrm{op} b a$ for all $a, b \in \alpha$), the operation $\mathrm{op}$ is symmetric.

IsSymmOp.flip_eq theorem

(op : α → α → β) [IsSymmOp op] : flip op = op

Full source

theorem IsSymmOp.flip_eq (op : α → α → β) [IsSymmOp op] : flip op = op :=
  funext fun a ↦ funext fun b ↦ (IsSymmOp.symm_op a b).symm

Flipped Symmetric Operation Equals Original

Informal description

For any symmetric binary operation $\mathrm{op} : \alpha \to \alpha \to \beta$, the flipped operation $\mathrm{flip}\ \mathrm{op}$ is equal to $\mathrm{op}$ itself.

instRightCommutativeOfLeftCommutative instance

{f : α → β → β} [h : LeftCommutative f] : RightCommutative (fun x y ↦ f y x)

Full source

instance {f : α → β → β} [h : LeftCommutative f] : RightCommutative (fun x y ↦ f y x) :=
  ⟨fun _ _ _ ↦ (h.left_comm _ _ _).symm⟩

Right-commutativity of the flipped left-commutative operation

Informal description

For any left-commutative operation $f : \alpha \to \beta \to \beta$, the operation $(x, y) \mapsto f y x$ is right-commutative.

instLeftCommutativeOfRightCommutative instance

{f : β → α → β} [h : RightCommutative f] : LeftCommutative (fun x y ↦ f y x)

Full source

instance {f : β → α → β} [h : RightCommutative f] : LeftCommutative (fun x y ↦ f y x) :=
  ⟨fun _ _ _ ↦ (h.right_comm _ _ _).symm⟩

Left-commutativity of the flipped right-commutative operation

Informal description

For any right-commutative operation $f : \beta \to \alpha \to \beta$, the operation $(x, y) \mapsto f y x$ is left-commutative.

instLeftCommutativeOfCommutativeOfAssociative instance

{f : α → α → α} [hc : Std.Commutative f] [ha : Std.Associative f] : LeftCommutative f

Full source

instance {f : α → α → α} [hc : Std.Commutative f] [ha : Std.Associative f] : LeftCommutative f :=
  ⟨fun a b c ↦ by rw [← ha.assoc, hc.comm a, ha.assoc]⟩

Commutative and Associative Operations are Left-Commutative

Informal description

For any binary operation $f : \alpha \to \alpha \to \alpha$ that is commutative and associative, $f$ is left-commutative. That is, for any $a_1, a_2, b \in \alpha$, we have $f(a_1, f(a_2, b)) = f(a_2, f(a_1, b))$.

instRightCommutativeOfCommutativeOfAssociative instance

{f : α → α → α} [hc : Std.Commutative f] [ha : Std.Associative f] : RightCommutative f

Full source

instance {f : α → α → α} [hc : Std.Commutative f] [ha : Std.Associative f] : RightCommutative f :=
  ⟨fun a b c ↦ by rw [ha.assoc, hc.comm b, ha.assoc]⟩

Commutative and Associative Operations are Right-Commutative

Informal description

For any binary operation $f : \alpha \to \alpha \to \alpha$ that is commutative and associative, $f$ is right-commutative. That is, for any $b, a_1, a_2 \in \alpha$, we have $f(f(b, a_1), a_2) = f(f(b, a_2), a_1)$.