equiv — Mathlib

English

The Clifford algebra over the zero quadratic form is canonically isomorphic to the ring of dual numbers R[ε].

Русский

Клиффордова алгебра над нулевой квадратичной формой канонически изоморфна кольцу дуальных чисел R[ε].

LaTeX

$$$\mathrm{CliffordAlgebra}(0) \cong_R R[\varepsilon]$$$

Lean4

/-- The clifford algebra over a 1-dimensional vector space with 0 quadratic form is isomorphic to
the dual numbers. -/
protected def equiv : CliffordAlgebra (0 : QuadraticForm R R) ≃ₐ[R] R[ε] :=
  AlgEquiv.ofAlgHom (CliffordAlgebra.lift (0 : QuadraticForm R R) ⟨inrHom R _, fun m => inr_mul_inr _ m m⟩)
    (DualNumber.lift ⟨(Algebra.ofId _ _, ι (R := R) _ 1), ι_mul_ι (1 : R) 1, fun _ => (Algebra.commutes _ _).symm⟩)
    (by
      ext : 1
        -- This used to be a single `simp` before https://github.com/leanprover/lean4/pull/2644

      simp only [QuadraticMap.zero_apply, AlgHom.coe_comp, Function.comp_apply, lift_apply_eps, AlgHom.coe_id, id_eq]
      erw [lift_ι_apply]
      simp)
      -- This used to be a single `simp` before https://github.com/leanprover/lean4/pull/2644

    (by
      ext : 2
      simp only [QuadraticMap.zero_apply, AlgHom.comp_toLinearMap, LinearMap.coe_comp, Function.comp_apply,
        AlgHom.toLinearMap_apply, AlgHom.toLinearMap_id, LinearMap.id_comp]
      erw [lift_ι_apply]
      simp)

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