Theorems · Definition · ring theory

CliffordAlgebra.map

{R : Type u_1} →
  [inst : CommRing R] →
    {M₁ : Type u_4} →
      {M₂ : Type u_5} →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : AddCommGroup M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] →
                {Q₁ : QuadraticForm R M₁} →
                  {Q₂ : QuadraticForm R M₂} → (Q₁ →qᵢ Q₂) → CliffordAlgebra Q₁ →ₐ[R] CliffordAlgebra Q₂

Any linear map that preserves the quadratic form lifts to an AlgHom between algebras. See CliffordAlgebra.equivOfIsometry for the case when f is a QuadraticForm.IsometryEquiv.

Defined in

Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Cited by

15 results in Mathlib

Foundations

Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupAddCommGroupModuleModule