whiskerLeft_map_counit — Mathlib

English

For any morphism f: X1 → Y1, the whiskering identity holds: whiskerLeft _ (F.map f) ≫ (adj2.adj Y1).counit = whiskerRight (G.map f.op) _ ≫ (adj2.adj X1).counit.

Русский

Для любого морфизма f: X1 → Y1 выполняется тождество whiskerLeft ≪...≫ counit.

LaTeX

$$$\operatorname{whiskerLeft} _ (F.map f) \;\gg\; (adj_2.adj Y_1).counit \\ = \\operatorname{whiskerRight} (G.map f.op) _ \\gg \\ (adj_2.adj X_1).counit$$$

Lean4

@[reassoc]
theorem whiskerLeft_map_counit {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁) :
    whiskerLeft _ (F.map f) ≫ (adj₂.adj Y₁).counit = whiskerRight (G.map f.op) _ ≫ (adj₂.adj X₁).counit :=
  by
  ext X₃
  dsimp
  apply adj₂.homEquiv.injective
  rw [homEquiv_naturality_one, homEquiv_naturality_two]
  simp [homEquiv_eq, Adjunction.homEquiv_unit]

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