triangle_assoc_comp_right — Mathlib

English

The triangle axiom on the right expresses that the associator with the right unitor gives a natural isomorphism between f and g, on the right side.

Русский

Треугольная когерентность справа: ассоциатор и правый утор задают естественную изоморфность слева/справа между f и g.

LaTeX

$$$ (\alpha_ f (\mathbb{1} b) g)^{\mathrm{inv}} \; \circ \; (\rho_{f})^{\mathrm{hom}} \; \triangleright g = f \triangleleft (\lambda_{g})^{\mathrm{hom}} $$$

Lean4

@[reassoc (attr := simp)]
theorem triangle_assoc_comp_right (f : a ⟶ b) (g : b ⟶ c) : (α_ f (𝟙 b) g).inv ≫ (ρ_ f).hom ▷ g = f ◁ (λ_ g).hom := by
  rw [← triangle, inv_hom_id_assoc]

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