evenEquivEvenNeg — Mathlib

English

The even subalgebras of Clifford algebras for Q and for −Q are isomorphic via an explicit AlgEquiv, denoted evenEquivEvenNeg.

Русский

Чётные подпери Clifford Algebras для Q и −Q изоморфны через явное алгебро-равенство evenEquivEvenNeg.

LaTeX

$$$ \\mathrm{even}(Q) \\cong_R \\mathrm{even}(-Q) $$$

Lean4

/-- The even subalgebras of the algebras with quadratic form `Q` and `-Q` are isomorphic.

Stated another way, `𝒞ℓ⁺(p,q,r)` and `𝒞ℓ⁺(q,p,r)` are isomorphic. -/
@[simps!]
def evenEquivEvenNeg : CliffordAlgebra.even Q ≃ₐ[R] CliffordAlgebra.even (-Q) :=
  AlgEquiv.ofAlgHom (evenToNeg Q _ rfl) (evenToNeg (-Q) _ (neg_neg _).symm) (evenToNeg_comp_evenToNeg _ _ _ _)
    (evenToNeg_comp_evenToNeg _ _ _ _)

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