Elaboration of tensor expressions

• Syntax in Lean allows us to represent tensor expressions in a way close to what we expect to see on pen-and-paper.
• The elaborator turns this syntax into a tensor tree.

Examples

• Suppose T and T' are tensors S.F (OverColor.mk ![c1, c2]).
• {T | μ ν}ᵀ is tensorNode T.
• We can also write e.g. {T | μ ν}ᵀ.tensor to get the tensor itself.
• {- T | μ ν}ᵀ is neg (tensorNode T).
• {T | 0 ν}ᵀ is eval 0 0 (tensorNode T).
• {T | [μ] ν}ᵀ is eval 0 μ (tensorNode T).
• {T | μ ν + T' | μ ν}ᵀ is addNode (tensorNode T) (perm _ (tensorNode T')), where here _ will be the identity permutation so does nothing.
• {T | μ ν = T' | μ ν}ᵀ is (tensorNode T).tensor = (perm _ (tensorNode T')).tensor.
• If a ∈ k then {a •ₜ T | μ ν}ᵀ is smulNode a (tensorNode T).
• If g ∈ S.G then {g •ₐ T | μ ν}ᵀ is actionNode g (tensorNode T).
• Suppose T2 is a tensor S.F (OverColor.mk ![c3]). Then {T | μ ν ⊗ T2 | σ}ᵀ is prodNode (tensorNode T1) (tensorNode T2).
• If T3 is a tensor S.F (OverColor.mk ![S.τ c1, S.τ c2]), then {T | μ ν ⊗ T3 | μ σ}ᵀ is contr 0 1 _ (prodNode (tensorNode T1) (tensorNode T3)). {T | μ ν ⊗ T3 | μ ν }ᵀ is contr 0 0 _ (contr 0 1 _ (prodNode (tensorNode T1) (tensorNode T3))).
• If T4 is a tensor S.F (OverColor.mk ![c2, c1]) then {T | μ ν + T4 | ν μ }ᵀis addNode (tensorNode T) (perm _ (tensorNode T4)) where _ is the permutation of the two indices of T4. {T | μ ν = T4 | ν μ }ᵀ is (tensorNode T).tensor = (perm _ (tensorNode T4)).tensor is the permutation of the two indices of T4.

Comments

• In all of these expressions μ, ν etc are free. It does not matter what they are called, Lean will elaborate them in the same way. In other words, {T | μ ν ⊗ T3 | μ ν }ᵀ is exactly the same to Lean as {T | α β ⊗ T3 | α β }ᵀ.
• Note that compared to ordinary index notation, we do not rise or lower the indices. This is for two reasons: 1) It is difficult to make this general for all tensor species, 2) It is a redundancy in ordinary index notation, since the tensor T itself already tells you this information.

Indices

def TensorSpecies.Tensor.indexExpr.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.indexExpr : Category

A syntax category for indices of tensor expressions.

Equations

• Lean.Parser.Category.indexExpr = { }

def TensorSpecies.Tensor.indexExpr_ : Lean.ParserDescr

A basic index is a ident.

Equations

• TensorSpecies.Tensor.indexExpr_ = Lean.ParserDescr.node `TensorSpecies.Tensor.indexExpr_ 1022 (Lean.ParserDescr.const `ident)

def TensorSpecies.Tensor.indexExpr__1 : Lean.ParserDescr

An index can be a num, which will be used to evaluate the tensor.

Equations

• TensorSpecies.Tensor.indexExpr__1 = Lean.ParserDescr.node `TensorSpecies.Tensor.indexExpr__1 1022 (Lean.ParserDescr.const `num)

def TensorSpecies.Tensor.«indexExprτ(_)» : Lean.ParserDescr

Notation to describe the jiggle of a tensor index.

Equations

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

def TensorSpecies.Tensor.«indexExpr[_]» : Lean.ParserDescr

Notation to describe the evaluation of a tensor index.

Equations

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

def TensorSpecies.Tensor.indexExprIsNum (stx : Lean.Syntax) : Bool

Bool which is true if an index is a num.

Equations

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

def TensorSpecies.Tensor.indexExprIsBracketEval (stx : Lean.Syntax) : Bool

Bool which is true if an index is evaluated bracket [μ].

Equations

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

def TensorSpecies.Tensor.indexToNum (stx : Lean.Syntax) : Lean.Elab.TermElabM ℕ

If an index is a num - the underlying natural number.

Equations

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

def TensorSpecies.Tensor.indexToIdent (stx : Lean.Syntax) : Lean.Elab.TermElabM Lean.Ident

When an index is not a num, the corresponding ident.

Equations

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

def TensorSpecies.Tensor.indexPosEq (a b : Lean.TSyntax `indexExpr × ℕ) : Lean.Elab.TermElabM (Option (ℕ × ℕ))

Takes a pair a b : ℕ × TSyntax `indexExpr. If a.1 < b.1 and a.2 = b.2 then outputs some (a.1, b.1), otherwise none.

Equations

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

def TensorSpecies.Tensor.indexToDual (stx : Lean.Syntax) : Bool

Bool which is true if an index is of the form τ(i) that is, to be dualed.

Equations

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

Manipulation of lists of indexExpr

def TensorSpecies.Tensor.evalAdjustPos (l : List ℕ) : List ℕ

Adjusts a list List ℕ by subtracting from each natural number the number of elements before it in the list which are less than itself. This is used to form a list of pairs which can be used for evaluating indices.

Equations

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

def TensorSpecies.Tensor.getEvalPos (ind : List (Lean.TSyntax `indexExpr)) : Lean.Elab.TermElabM (List (ℕ × ℕ))

For list of indexExpr e.g. [α, 3, β, 2, γ], getEvalPos returns a list of pairs ℕ × ℕ related to indices which are numbers. The second element of each pair is the number corresponding to that index. The first element is the position of that number in the list of indices when all other numbered indices before it are removed. Thus for the example given getEvalPos outputs [(1, 3), (2, 2)].

Equations

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

def TensorSpecies.Tensor.getEvalBracketPos (ind : List (Lean.TSyntax `indexExpr)) : Lean.Elab.TermElabM (List (ℕ × Lean.Term))

For list of indexExpr e.g. [α, 3, β, 2, [γ]], getEvalPos returns a list of pairs ℕ × Term related to indices which are evaluated e.g. [μ]. The second element of each pair is the value corresponding to that index. The first element is the position of that number in the list of indices when all other numbered indices before it are removed. Thus for the example given getEvalBracketPos outputs [(4, γ)].

Equations

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

def TensorSpecies.Tensor.getContrPos (ind : List (Lean.TSyntax `indexExpr)) : Lean.Elab.TermElabM (List (ℕ × ℕ))

For list of indexExpr e.g. [α, 3, β, α, 2, γ], getContrPos first removes all indices which are numbers (e.g. [α, β, α, γ]). It then outputs pairs (a, b) in ℕ × ℕ of positions of this list with a < b such that the index at a is equal to the index at b. It checks whether or not an element is contracted more then once.

Equations

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

def TensorSpecies.Tensor.withoutContrEval (ind : List (Lean.TSyntax `indexExpr)) : Lean.Elab.TermElabM (List (Lean.TSyntax `indexExpr))

The list of indices after contraction or evaluation.

Equations

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

def TensorSpecies.Tensor.toPairs (l : List ℕ) : List (ℕ × ℕ)

Takes a list and puts consecutive elements into pairs. e.g. [0, 1, 2, 3] becomes [(0, 1), (2, 3)].

Equations

• TensorSpecies.Tensor.toPairs (x1 :: x2 :: xs) = (x1, x2) :: TensorSpecies.Tensor.toPairs xs
• TensorSpecies.Tensor.toPairs [] = []
• TensorSpecies.Tensor.toPairs [x] = [(x, 0)]

def TensorSpecies.Tensor.contrListAdjust (l : List (ℕ × ℕ)) : List (ℕ × ℕ)

Adjusts a list List (ℕ × ℕ) by subtracting from each natural number the number of elements before it in the list which are less than itself. This is used to form a list of pairs which can be used for contracting indices.

Equations

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

Permutations of indices

def TensorSpecies.Tensor.getPermutation (l1 l2 : List (Lean.TSyntax `indexExpr)) : Lean.Elab.TermElabM (List ℕ)

Given two lists of indices, all of which are indent, returns the List (ℕ) representing the how one list permutes into the other.

Equations

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

def TensorSpecies.Tensor.stringToTerm (str : String) : Lean.Elab.TermElabM Lean.Term

The construction of an expression corresponding to the type of a given string once parsed.

Equations

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

def TensorSpecies.Tensor.getPermutationTerm (l1 l2 : List (Lean.TSyntax `indexExpr)) : Lean.Elab.TermElabM Lean.Term

Given two lists of indices returns the permutation between them based on finMapToEquiv.

Equations

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

Syntax for tensor expressions.

def TensorSpecies.Tensor.tensorExpr.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.tensorExpr : Category

A syntax category for tensor expressions.

Equations

• Lean.Parser.Category.tensorExpr = { }

def TensorSpecies.Tensor.«tensorExpr_|__» : Lean.ParserDescr

The syntax for a tensor node.

Equations

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

def TensorSpecies.Tensor.«tensorExpr_=_» : Lean.TrailingParserDescr

Equality.

Equations

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

def TensorSpecies.Tensor.«tensorExpr_⊗_» : Lean.TrailingParserDescr

The syntax for tensor prod two tensor nodes.

Equations

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

def TensorSpecies.Tensor.«tensorExpr_+_» : Lean.TrailingParserDescr

The syntax for tensor addition.

Equations

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

def TensorSpecies.Tensor.«tensorExpr(_)» : Lean.ParserDescr

Allowing brackets to be used in a tensor expression.

Equations

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

def TensorSpecies.Tensor.«tensorExpr_•ₜ_» : Lean.ParserDescr

Scalar multiplication for tensors.

Equations

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

def TensorSpecies.Tensor.«tensorExpr_•ₐ_» : Lean.ParserDescr

group action for tensors.

Equations

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

def TensorSpecies.Tensor.«tensorExpr-_» : Lean.ParserDescr

Negation of a tensor tree.

Equations

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

Syntax of tensor expressions to indices.

def TensorSpecies.Tensor.getNumIndicesExact (stx : Lean.Syntax) : Lean.Elab.TermElabM ℕ

For syntax of the form T where T is S.F.obj (OverColor.mk c) this returns the value of TensorSpecies.numIndices T. That is, the exact number of indices associated with that tensor.

Equations

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

def TensorSpecies.Tensor.getAllIndices (stx : Lean.Syntax) : Lean.Elab.TermElabM (List (Lean.TSyntax `indexExpr))

For syntax of the form T | α β 2 β, getAllIndices returns a list [α, β, 2, β] of all indexExpr.

Equations

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

partial def TensorSpecies.Tensor.getProdIndices (stx : Lean.Syntax) : Lean.Elab.TermElabM (List (Lean.TSyntax `indexExpr))

The function getProdIndices is defined for the following syntax:

1. For e.g. T | α β 2 β, it returns all uncontracted and unevaluated indices e.g.[α]
2. For e.g. T1 | α β 2 β ⊗ T2 | α γ δ δ it returns all unevaluated indices which are not contracted in either tensor e.g. [α, α, γ].
3. For e.g. (T1 | α β 2 β ⊗ T2 | α γ δ δ) ⊗ T3 | γ it does 2 recursively e.g. [γ, γ]

partial def TensorSpecies.Tensor.getIndicesFull (stx : Lean.Syntax) : Lean.Elab.TermElabM (List (Lean.TSyntax `indexExpr))

Returns the remaining indices of a tensor expression after contraction and evaluation. Thus every index in the output of getIndicesFull is ident and there are no duplicates. Examples are:

1. T | α β 2 β gives [α]
2. T1 | α β 2 β ⊗ T2 | α γ δ δ gives [γ]
3. (T1 | α β 2 β ⊗ T2 | α γ δ δ) ⊗ T3 | γ gives []
4. T1 | α β 2 β + T2 | α 4 δ δ gives [α]

def TensorSpecies.Tensor.getIndicesLeft (stx : Lean.Syntax) : Lean.Elab.TermElabM (List (Lean.TSyntax `indexExpr))

Gets the indices associated with the LHS of an addition.

Equations

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

def TensorSpecies.Tensor.getIndicesRight (stx : Lean.Syntax) : Lean.Elab.TermElabM (List (Lean.TSyntax `indexExpr))

Gets the indices associated with the RHS of an addition.

Equations

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

def TensorSpecies.Tensor.getIndicesLeftEq (stx : Lean.Syntax) : Lean.Elab.TermElabM (List (Lean.TSyntax `indexExpr))

Gets the indices associated with the LHS of an equality.

Equations

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

def TensorSpecies.Tensor.getIndicesRightEq (stx : Lean.Syntax) : Lean.Elab.TermElabM (List (Lean.TSyntax `indexExpr))

Gets the indices associated with the RHS of an equality.

Equations

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

Modifying terms to tensor trees

def TensorSpecies.Tensor.nodeTermMap (T : Lean.Term) : Lean.Term

For a term of the form T where T is S.F.obj (OverColor.mk c), tensorTermToTensorTree returns the term corresponding to the tensorNode T

Equations

• TensorSpecies.Tensor.nodeTermMap T = Lean.Syntax.mkApp { raw := (Lean.mkIdent `TensorSpecies.Tensorial.toTensor).raw } #[T]

def TensorSpecies.Tensor.evalTermMap (l : List (ℕ × ℕ)) (T : Lean.Term) : Lean.Term

Given a list l of pairs ℕ × ℕ and a term T corresponding to a tensor tree, for each (a, b) in l, evalSyntax applies TensorTree.eval a b to T recursively. Here a is the position of the index to be evaluated and b is the value it is evaluated to.

For example, if l is [(1, 2), (1, 4)] and T is a tensor tree then evalSyntax l T is TensorTree.eval 1 4 (TensorTree.eval 1 2 T).

The list l is expected to be the output of getEvalPos.

Equations

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

def TensorSpecies.Tensor.evalTermBracketMap (l : List (ℕ × Lean.Term)) (T : Lean.Term) : Lean.Term

Given a list l of pairs ℕ × Term and a term T corresponding to a tensor tree, for each (a, b) in l, evalSyntax applies TensorTree.eval a b to T recursively. Here a is the position of the index to be evaluated and b is the value it is evaluated to from the [μ] syntax.

For example, if l is [(1, μ), (1, ν)] and T is a tensor tree then evalSyntax l T is TensorTree.eval 1 ν (TensorTree.eval 1 μ T).

The list l is expected to be the output of getEvalBracketPos.

Equations

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

def TensorSpecies.Tensor.contrTermMap (n : ℕ) (l : List (ℕ × ℕ)) (T : Lean.Term) : Lean.Term

For each element of l : List (ℕ × ℕ) applies TensorTree.contr to the given term.

Equations

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

def TensorSpecies.Tensor.prodTermMap (T1 T2 : Lean.Term) : Lean.Term

The syntax associated with a product of tensors.

Equations

• TensorSpecies.Tensor.prodTermMap T1 T2 = Lean.Syntax.mkApp { raw := (Lean.mkIdent `TensorSpecies.Tensor.prodT).raw } #[T1, T2]

def TensorSpecies.Tensor.negTermMap (T1 : Lean.Term) : Lean.Term

The syntax associated with negation of tensors.

Equations

• TensorSpecies.Tensor.negTermMap T1 = Lean.Syntax.mkApp { raw := (Lean.mkIdent `Neg.neg).raw } #[T1]

def TensorSpecies.Tensor.smulTermMap (c T : Lean.Term) : Lean.Term

The syntax associated with the scalar multiplication of tensors.

Equations

• TensorSpecies.Tensor.smulTermMap c T = Lean.Syntax.mkApp { raw := (Lean.mkIdent `HSMul.hSMul).raw } #[c, T]

def TensorSpecies.Tensor.actionTermMap (c T : Lean.Term) : Lean.Term

The syntax associated with the group action of tensors.

Equations

• TensorSpecies.Tensor.actionTermMap c T = Lean.Syntax.mkApp { raw := (Lean.mkIdent `HSMul.hSMul).raw } #[c, T]

def TensorSpecies.Tensor.addTermMap (P T1 T2 : Lean.Term) : Lean.Elab.TermElabM Lean.Term

The syntax for a equality of tensor trees.

Equations

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

def TensorSpecies.Tensor.equalTermMap (P T1 T2 : Lean.Term) : Lean.Elab.TermElabM Lean.Term

The syntax for a equality of tensor trees.

Equations

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

Syntax to tensor tree

partial def TensorSpecies.Tensor.syntaxFull (stx : Lean.Syntax) : Lean.Elab.TermElabM Lean.Term

Takes a syntax corresponding to a tensor expression and turns it into a term corresponding to a tensor tree.

Elaboration

def TensorSpecies.Tensor.elaborateTensorNode (stx : Lean.Syntax) : Lean.Elab.TermElabM Lean.Expr

Takes a syntax corresponding to a tensor expression and turns it into an expression corresponding to a tensor tree.

Equations

• TensorSpecies.Tensor.elaborateTensorNode stx = do let __do_lift ← TensorSpecies.Tensor.syntaxFull stx let tensorExpr ← Lean.Elab.Term.elabTerm __do_lift.raw none pure tensorExpr

def TensorSpecies.Tensor.tensorExprSyntax : Lean.ParserDescr

The tensor tree corresponding to a tensor expression.

Equations

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

Test cases