mateEquiv_leftUnitor_hom_rightUnitor_inv

English

The mateEquiv with left/right unital structures satisfies a simplification: mateEquiv adj adj ((λ_ _).hom ≫ (ρ_ _).inv) equals (ρ_ _).hom ≫ (λ_ _).inv.

Русский

Упрощение через левый/правый юнит: mateEquiv adj adj ((λ_ _).hom ≫ (ρ_ _).inv) = (ρ_ _).hom ≫ (λ_ _).inv.

LaTeX

$$$$ \\text{mateEquiv } adj\\ adj\\ ((\\lambda_\\_).hom \\gg (\\rho_\\_).inv) = (\\rho_\\_).hom \\gg (\\lambda_\\_).inv. $$$$

Lean4

@[simp]
theorem mateEquiv_leftUnitor_hom_rightUnitor_inv {a b : B} {l : a ⟶ b} {r : b ⟶ a} (adj : l ⊣ r) :
    mateEquiv adj adj ((λ_ _).hom ≫ (ρ_ _).inv) = (ρ_ _).hom ≫ (λ_ _).inv := by
  simp [← cancel_mono (λ_ r).hom, ← conjugateEquiv_id adj, conjugateEquiv_apply]

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