naturality_id_inv — Mathlib

English

Expresses the inverse of naturality in StrongTrans as composition of whiskered components.

Русский

Обозначение обратной натуральности в StrongTrans через композицию взвешенных компонентов.

LaTeX

$$$\natu(f g).inv = f ◁ G.map₂ η.inv \; ≫ \; (α.naturality f).inv \; ▷ G.map g \; ≫ \; (α _) .hom \; ◁ \; η.app b$$$

Lean4

@[reassoc, to_app]
theorem naturality_id_inv (α : F ⟶ G) (a : B) :
    (α.naturality (𝟙 a)).inv =
      α.app a ◁ (G.mapId a).hom ≫ (ρ_ (α.app a)).hom ≫ (λ_ (α.app a)).inv ≫ (F.mapId a).inv ▷ α.app a :=
  by simp [naturality_id_iso]

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