Bracket Notation

This file provides notation which can be used for the Lie bracket, for the commutator of two subgroups, and for other similar operations.

Main Definitions

• Bracket L M for a binary operation that takes something in L and something in M and produces something in M. Defining an instance of this structure gives access to the notation ⁅ ⁆

Notation

We introduce the notation ⁅x, y⁆ for the bracket of any Bracket structure. Note that these are the Unicode "square with quill" brackets rather than the usual square brackets.

class Bracket (L : Type u_1) (M : Type u_2) : Type (max u_1 u_2)

• bracket : L → M → M

  ⁅x, y⁆ is the result of a bracket operation on elements x and y. It is supported by the Bracket typeclass.

The Bracket class has three intended uses:

1. for certain binary operations on structures, like the product ⁅x, y⁆ of two elements x, y in a Lie algebra or the commutator of two elements x and y in a group.
2. for certain actions of one structure on another, like the action ⁅x, m⁆ of an element x of a Lie algebra on an element m in one of its modules (analogous to SMul in the associative setting).
3. for binary operations on substructures, like the commutator ⁅H, K⁆ of two subgroups H and K of a group.

def «term⁅_,_⁆» : Lean.ParserDescr

⁅x, y⁆ is the result of a bracket operation on elements x and y. It is supported by the Bracket typeclass.

Equations

• One or more equations did not get rendered due to their size.