unit_comp_map_eq_iff — Mathlib

English

In an adjunction F ⊣ G with unit η and counit ε, for any A ∈ C, B ∈ D, f: F(A) → B and g: A → G(B), the equation η_A ≫ G.map f = g holds if and only if f = F.map g ≫ ε_B.

Русский

Пусть F ⊣ G с единицей η и сопряжённой частью ε. Для любых A ∈ C, B ∈ D и морфизмов f: F(A) → B, g: A → G(B) верно: η_A ≫ G.map f = g тогда и только если f = F.map g ≫ ε_B.

LaTeX

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

Lean4

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

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