toEven_comp_ofEven — Mathlib

English

The canonical maps between the Clifford algebra and its even subalgebra are inverses: (toEven Q) ∘ (ofEven Q) is the identity on the even subalgebra, and (ofEven Q) ∘ (toEven Q) is the identity on the Clifford algebra. In particular, the even subalgebra is a retract of the full Clifford algebra with respect to these maps.

Русский

Канонические отображения между CliffordAlgebra и его подпалой чётности являются обратными друг другу: (toEven Q) ∘ (ofEven Q) — тождественный отображение на чётной подалге, и (ofEven Q) ∘ (toEven Q) — тождественный на всей CliffordAlgebra. Следовательно, подпольность является retract-ом полной алгебры.

LaTeX

$$$ (\\text{toEven}(Q)) \\circ (\\text{ofEven}(Q)) = \\mathrm{AlgHom.id}_R(\\mathrm{CliffordAlgebra}(Q)) \\quad\\text{and}\\quad (\\text{ofEven}(Q)) \\circ (\\text{toEven}(Q)) = \\mathrm{AlgHom.id}_R(\\mathrm{CliffordAlgebra}(Q)). $$$

Lean4

theorem toEven_comp_ofEven : (toEven Q).comp (ofEven Q) = AlgHom.id R _ :=
  even.algHom_ext (Q' Q) <|
    EvenHom.ext <|
      LinearMap.ext fun m₁ =>
        LinearMap.ext fun m₂ =>
          Subtype.ext <|
            let ⟨m₁, r₁⟩ := m₁
            let ⟨m₂, r₂⟩ := m₂
            calc
              ↑(toEven Q (ofEven Q ((even.ι (Q' Q)).bilin (m₁, r₁) (m₂, r₂)))) =
                  (e0 Q * v Q m₁ + algebraMap R _ r₁) * (e0 Q * v Q m₂ - algebraMap R _ r₂) :=
                by
                rw [ofEven_ι, map_mul, map_add, map_sub, AlgHom.commutes, AlgHom.commutes, Subalgebra.coe_mul,
                  Subalgebra.coe_add, Subalgebra.coe_sub, toEven_ι, toEven_ι, Subalgebra.coe_algebraMap,
                  Subalgebra.coe_algebraMap]
              _ =
                  e0 Q * v Q m₁ * (e0 Q * v Q m₂) + r₁ • e0 Q * v Q m₂ - r₂ • e0 Q * v Q m₁ -
                    algebraMap R _ (r₁ * r₂) :=
                by
                rw [mul_sub, add_mul, add_mul, ← Algebra.commutes, ← Algebra.smul_def, ← map_mul, ← Algebra.smul_def,
                  sub_add_eq_sub_sub, smul_mul_assoc, smul_mul_assoc]
              _ = v Q m₁ * v Q m₂ + r₁ • e0 Q * v Q m₂ + v Q m₁ * r₂ • e0 Q + r₁ • e0 Q * r₂ • e0 Q :=
                by
                have h1 : e0 Q * v Q m₁ * (e0 Q * v Q m₂) = v Q m₁ * v Q m₂ := by rw [← mul_assoc, e0_mul_v_mul_e0]
                have h2 : -(r₂ • e0 Q * v Q m₁) = v Q m₁ * r₂ • e0 Q := by
                  rw [mul_smul_comm, smul_mul_assoc, ← smul_neg, neg_e0_mul_v]
                have h3 : -algebraMap R _ (r₁ * r₂) = r₁ • e0 Q * r₂ • e0 Q := by
                  rw [Algebra.algebraMap_eq_smul_one, smul_mul_smul_comm, e0_mul_e0, smul_neg]
                rw [sub_eq_add_neg, sub_eq_add_neg, h1, h2, h3]
              _ = ι (Q' Q) (m₁, r₁) * ι (Q' Q) (m₂, r₂) := by
                rw [ι_eq_v_add_smul_e0, ι_eq_v_add_smul_e0, mul_add, add_mul, add_mul, add_assoc]

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