reverseOp — Mathlib

English

The reverse operation defines an algebra homomorphism from CliffordAlgebra Q to its opposite algebra.

Русский

Операция обратного порядка задаёт алгебраический гомоморфизм от CliffordAlgebra Q в противоположную алгебру.

LaTeX

$$$ \text{reverseOp} : \mathrm{CliffordAlgebra}(Q) \to_{R} (\mathrm{CliffordAlgebra}(Q))^{\mathrm{op}}. $$$

Lean4

/-- `CliffordAlgebra.reverse` as an `AlgHom` to the opposite algebra -/
def reverseOp : CliffordAlgebra Q →ₐ[R] (CliffordAlgebra Q)ᵐᵒᵖ :=
  CliffordAlgebra.lift Q ⟨(MulOpposite.opLinearEquiv R).toLinearMap ∘ₗ ι Q, fun m => unop_injective <| by simp⟩

Похожие утверждения