rid — Mathlib

English

For any a in P, the inverse of the lid map sends a to 1 ⊗ a; i.e., (lid R P).symm a = 1 ⊗ a.

Русский

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

LaTeX

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

Lean4

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

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