lid — Mathlib

English

For any a ∈ P, the symmetric lid maps a to 1 ⊗ a; i.e., (lid_R P).symm a = 1 ⊗ a.

Русский

Для любого a ∈ P симметричное lid отображение даёт 1 ⊗ a; то есть (lid_R P).symm a = 1 ⊗ a.

LaTeX

$$$ (\mathrm{lid}\; R\; P)^{\mathrm{symm}}(a) = 1 \otimes a. $$$

Lean4

/-- The base ring is a left identity for the tensor product of coalgebras, up to
coalgebra equivalence. -/
protected noncomputable def lid : R ⊗[R] P ≃ₗc[R] P :=
  { _root_.TensorProduct.lid R P with
    counit_comp := by ext; simp
    map_comp_comul := by
      ext x
      dsimp
      simp only [one_smul]
      hopf_tensor_induction comul (R := R) x with x₁ x₂
      simp }

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