antipode_counit — Mathlib

English

The antipode followed by counit vanishes to counit: 𝒮[A] ≫ ε[A] = ε[A].

Русский

Антипод, затем counit, дает counit: 𝒮[A] ≫ ε[A] = ε[A].

LaTeX

$$$ 𝒮[A] \circ ε[A] = ε[A] $$$

Lean4

@[reassoc (attr := simp)]
theorem antipode_counit (A : C) [HopfObj A] : 𝒮[A] ≫ ε[A] = ε[A] :=
  by
  have := (rfl : Δ[A] ≫ (𝒮[A] ▷ A) ≫ μ[A] ≫ ε[A] = _)
  conv at this =>
    rhs
    rw [antipode_left_assoc]
  rw [Bimon.mul_counit, tensorHom_def', Category.assoc, ← whisker_exchange_assoc] at this
  simpa [unitors_equal]

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