unit_mateEquiv_symm — Mathlib

English

The mate equivalence for symmetrically inverted adjunctions is inverse to itself.

Русский

Единичная мейт-эквивалентность симметрично обращённых сопряжений является своей собственной обратной.

LaTeX

$$$$(\\text{mateEquiv adj1 adj2}).symm$$$$

Lean4

/-- A component of a transposed version of the inverse mates correspondence. -/
theorem unit_mateEquiv_symm (α : TwoSquare R₁ H G R₂) (c : C) :
    G.map (adj₁.unit.app c) ≫ α.app _ = adj₂.unit.app _ ≫ R₂.map (((mateEquiv adj₁ adj₂).symm α).app _) :=
  by
  conv_lhs => rw [← (mateEquiv adj₁ adj₂).right_inv α]
  exact (unit_mateEquiv adj₁ adj₂ ((mateEquiv adj₁ adj₂).symm α) c)

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