map_comp_map — Mathlib

English

If f: Q1 →qᵢ Q2 and g: Q2 →qᵢ Q3 are isometries, then the Clifford algebra maps compose: map f followed by map g equals map of f composed with g.

Русский

Если f: Q1 →qᵢ Q2 и g: Q2 →qᵢ Q3 — тождественные изометрии, то отображения CliffordAlgebra соответствуют композиции: map f ∘ map g = map (f ∘ g).

LaTeX

$$$ (\mathrm{CliffordAlgebra.map} f) \circ (\mathrm{CliffordAlgebra.map} g) = \mathrm{CliffordAlgebra.map} (f \circ g). $$$

Lean4

@[simp]
theorem map_comp_map (f : Q₂ →qᵢ Q₃) (g : Q₁ →qᵢ Q₂) : (map f).comp (map g) = map (f.comp g) :=
  by
  ext m
  dsimp only [LinearMap.comp_apply, AlgHom.comp_apply, AlgHom.toLinearMap_apply, AlgHom.id_apply]
  rw [map_apply_ι, map_apply_ι, map_apply_ι, QuadraticMap.Isometry.comp_apply]

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