homEquiv_apply_eq — Mathlib

English

For any A ∈ C, B ∈ D and f: F(A) → B, g: A → G(B), the hom-equivalence satisfies adj.homEquiv A B f = g if and only if the inverse maps back to f: (adj.homEquiv A B).symm g = f.

Русский

Для любых A ∈ C, B ∈ D и f: F(A) → B, g: A → G(B) биекция гомоморфизмов удовлетворяет: adj.homEquiv A B f = g ⇔ (adj.homEquiv A B).symm g = f.

LaTeX

$$$ adj.homEquiv A B f = g \iff (adj.homEquiv A B)^{-1} g = f $$$

Lean4

theorem homEquiv_apply_eq {A : C} {B : D} (f : F.obj A ⟶ B) (g : A ⟶ G.obj B) :
    adj.homEquiv A B f = g ↔ f = (adj.homEquiv A B).symm g :=
  unit_comp_map_eq_iff adj f g

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