comp_tensorLId_eq — Mathlib

English

For a quadratic form Q2, composing with TensorProduct.lid R M2 yields Q2 ⊗ sq: Q2 ∘ lid = Q2 ⊗ sq.

Русский

Для Q2 композиция с TensorProduct.lid R M2 даёт Q2 ⊗ sq.

LaTeX

$$$Q_2 \circ (\mathrm{TensorProduct}.lid\, R\, M_2) = Q_2 \otimes \mathrm{sq}(Q_2)$$$

Lean4

theorem comp_tensorLId_eq (Q₂ : QuadraticForm R M₂) :
    Q₂.comp (TensorProduct.lid R M₂) = QuadraticForm.tmul (sq (R := R)) Q₂ :=
  by
  refine (QuadraticMap.associated_rightInverse R).injective ?_
  ext m₂ m₂'
  dsimp [-associated_apply]
  simp only [associated_tmul, QuadraticMap.associated_comp]
  simp [-associated_apply, mul_one]

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