free_hom_ext — Mathlib

English

The hom-equivalence for the free adjunction coincides with the freeHomEquiv bijection.

Русский

Гомэквивалентность свободной адъюнкции совпадает с биекция-freeHomEquiv.

LaTeX

$$$\\mathrm{freeAdjunction\\_homEquiv} = \\mathrm{freeHomEquiv}$$$

Lean4

theorem free_hom_ext {ψ ψ' : freeObj F ⟶ G}
    (h :
      freeAdjunctionUnit R F ≫ Functor.whiskerRight ((toPresheaf _).map ψ) _ =
        freeAdjunctionUnit R F ≫ Functor.whiskerRight ((toPresheaf _).map ψ') _) :
    ψ = ψ' :=
  freeHomEquiv.injective h

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