counit_antipode — Mathlib

English

For any a ∈ A, counit(antipode(a)) = counit(a).

Русский

Для любого a ∈ A выполняется counit(S(a)) = counit(a).

LaTeX

$$$\varepsilon(\mathrm{antipode}\,R\,a) = \varepsilon(a).$$$

Lean4

@[simp]
theorem counit_antipode (a : A) : counit (R := R) (antipode R a) = counit a := by
  calc
    counit (antipode R a)
    _ = counit (∑ i ∈ (ℛ R a).index, (ℛ R a).left i * antipode R ((ℛ R a).right i)) := by
      simp_rw [map_sum, counit_mul, ← smul_eq_mul, ← map_smul, ← map_sum, sum_counit_smul]
    _ = counit a := by simpa using congr(counit (R := R) $(sum_mul_antipode_eq_smul (ℛ R a)))

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