counit_def — Mathlib

English

If A is a coalgebra over R, the counit on A^(op) is obtained by composing the original counit with the inverse of the op-linear equivalence; i.e., counit_{A^{op}} = counit ∘ (opLinearEquiv_R)^{-1}.

Русский

Если A — коалгебра над R, counit на A^{op} получается как композиция counit с обратным линейным эквивалентом: counit_{A^{op}} = counit ∘ (opLinearEquiv_R)^{-1}.

LaTeX

$$$\mathrm{counit}_{A^{op}} = \mathrm{counit} \circ (\mathrm{opLinearEquiv}_R)^{-1}.$$$

Lean4

theorem counit_def [CoalgebraStruct R A] : counit (R := R) (A := Aᵐᵒᵖ) = counit ∘ₗ (opLinearEquiv R).symm.toLinearMap :=
  rfl

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