counit_naturality — Mathlib

English

The counit of an adjunction is natural in the codomain: F maps G f then comp with counit equals counit then f.

Русский

Натуральность counit сопряжённости по коду: F maps G f затем композиция с counit равна counit затем f.

LaTeX

$$$\forall f: X \to Y,\; F.map (G.map f) ≫ adj.counit.app Y = adj.counit.app X ≫ f$$$

Lean4

@[reassoc (attr := simp)]
theorem counit_naturality {X Y : D} (f : X ⟶ Y) : F.map (G.map f) ≫ adj.counit.app Y = adj.counit.app X ≫ f :=
  adj.counit.naturality f

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