eq_unit_comp_map_iff — Mathlib

English

For A ∈ C, B ∈ D and f: F(A) → B, g: A → G(B), we have g = η_A ≫ G.map f if and only if F.map g ≫ ε_B = f.

Русский

Для A ∈ C, B ∈ D и f: F(A) → B, g: A → G(B) верно: g = η_A ≫ G.map f ⇔ F.map g ≫ ε_B = f.

LaTeX

$$$ g = adj.unit.app A \circ G.map f \iff F.map g \circ adj.counit.app B = f $$$

Lean4

theorem eq_unit_comp_map_iff {A : C} {B : D} (f : F.obj A ⟶ B) (g : A ⟶ G.obj B) :
    g = adj.unit.app A ≫ G.map f ↔ F.map g ≫ adj.counit.app B = f :=
  ⟨fun h => by simp [h], fun h => by simp [← h]⟩

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