one_antipode — Mathlib

English

The unit composed with antipode yields the unit: η[A] ≫ 𝒮[A] = η[A].

Русский

Единица композиции с antipode дает единицу: η[A] ≫ 𝒮[A] = η[A].

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem one_antipode (A : C) [HopfObj A] : η[A] ≫ 𝒮[A] = η[A] :=
  by
  have := (rfl : η[A] ≫ Δ[A] ≫ (𝒮[A] ▷ A) ≫ μ[A] = _)
  conv at this =>
    rhs
    rw [antipode_left]
  rw [Bimon.one_comul_assoc, tensorHom_def_assoc, unitors_inv_equal, ← rightUnitor_inv_naturality_assoc,
    whisker_exchange_assoc, ← rightUnitor_inv_naturality_assoc, rightUnitor_inv_naturality_assoc] at this
  simpa

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