doc-next-gen

Mathlib.Data.Bracket

Module docstring

{"# 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. "}

Bracket structure
(L M : Type*)
Full source 
/-- 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. -/
class Bracket (L M : Type*) where
  /-- `⁅x, y⁆` is the result of a bracket operation on elements `x` and `y`.
  It is supported by the `Bracket` typeclass. -/
  bracket : L → M → M
Bracket operation
Informal description
The structure `Bracket L M` represents a binary operation that takes an element from `L$ and an element from `M$ and produces an element in `M$. This operation is denoted by the notation `⁅x, y⁆`. It is used in three main contexts: 1. For binary operations on structures, such as the Lie bracket in a Lie algebra or the commutator in a group. 2. For actions of one structure on another, such as the action of a Lie algebra element on a module element. 3. For binary operations on substructures, such as the commutator of two subgroups in a group.
term⁅_,_⁆ definition
: Lean.ParserDescr✝
Full source 
@[inherit_doc] notation "⁅" x ", " y "⁆" => Bracket.bracket x y
Bracket notation `⁅x, y⁆`
Informal description
The notation `⁅x, y⁆` represents the bracket operation, which is a binary operation taking an element from a type `L` and an element from a type `M` and producing an element in `M`. This notation is commonly used for operations such as the Lie bracket in Lie algebras or the commutator in groups.