mathlib documentation


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 #

Notation #

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

structure has_bracket (L : Type u_1) (M : Type u_2) :
Type (max u_1 u_2)
  • bracket : L → M → M

The has_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 has_scalar in the associative setting).

  3. for binary operations on substructures, like the commutator ⁅H, K⁆ of two subgroups H and K of a group.