ι_apply — Mathlib

English

The action of the injection ι' on a direct sum element x is the quotient representative of TensorAlgebra.ι R x under the relation rel R A.

Русский

Действие инъекции ι' на элемент x прямой суммы — это репрезентант эквивалентности по отношению rel R A в тензорной алгебре, отображаемый в свободное произведение.

LaTeX

$$$\iota'_R A x = \langle \operatorname{Quot.mk} (\operatorname{RingQuot}.Rel (\mathrm{FreeProduct}.rel\, R\, A)) (\mathrm{TensorAlgebra}.ι\; R\; x) \rangle$$$

Lean4

@[simp]
theorem ι_apply (x : ⨁ i, A i) : ⟨Quot.mk (Rel <| rel R A) (TensorAlgebra.ι R x)⟩ = ι' R A x := by
  aesop (add simp [ι', mkAlgHom, RingQuot.mkAlgHom, mkRingHom])

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