rid — Mathlib

English

The coalgebra rid applied to x coincides with the algebra rid applied to x.

Русский

Применение коалгебр rid к x совпадает с применением алгебр rid к x.

LaTeX

$$$\text{coalgebra_rid}_{{R,S,A}}(x) = \text{algebra_rid}_{R,R,A}(x)$$$

Lean4

/-- The base ring is a right identity for the tensor product of bialgebras, up to
bialgebra equivalence. -/
protected noncomputable def rid : A ⊗[R] R ≃ₐc[S] A
    where
  toCoalgEquiv := Coalgebra.TensorProduct.rid R S A
  map_mul' x
    y := by
    simp only [CoalgEquiv.toCoalgHom_eq_coe, CoalgHom.toLinearMap_eq_coe, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom,
      CoalgHom.coe_toLinearMap, CoalgHom.coe_coe, coalgebra_rid_eq_algebra_rid_apply, map_mul]

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