unit_conjugateEquiv — Mathlib

English

The mates equivalence commutes with horizontal composition of squares of adjunctions.

Русский

Эквивалентность мат‑мейт сохраняет горизонтальную композицию квадратов сопряжений.

LaTeX

$$$$ (\\text{mateEquiv} (adj1.comp adj3) (adj2.comp adj4)) (\\alpha \\; \\hcomp \\; \\beta) = (\\text{mateEquiv adj3 adj4 } \\beta) \\; \\hcomp \\; (\\text{mateEquiv adj1 adj2 } \\alpha). $$$$

Lean4

/-- A component of a transposed form of the conjugation definition. -/
theorem unit_conjugateEquiv (α : L₂ ⟶ L₁) (c : C) :
    adj₁.unit.app _ ≫ (conjugateEquiv adj₁ adj₂ α).app _ = adj₂.unit.app c ≫ R₂.map (α.app _) :=
  by
  dsimp [conjugateEquiv]
  rw [id_comp, comp_id]
  have := unit_mateEquiv adj₁ adj₂ (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) c
  dsimp at this
  rw [this]
  simp

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