Theorems · Theorem · ring theory

CliffordAlgebra.map_surjective

∀ {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₂} (f : Q₁ →qᵢ Q₂), Function.Surjective ⇑f → Function.Surjective ⇑(CliffordAlgebra.map f)

If a linear map preserves the quadratic forms and is surjective, then the algebra maps it induces between Clifford algebras is also surjective.

Defined in

Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupAddCommGroupModuleModule