comparisonRightAdjointHomEquiv — Mathlib

English

Definition of the hom-set bijection between (comparison adj)-morphisms and maps to the right adjoint object, as a canonical equivalence.

Русский

Определение биекции множеств гомоморфизмов между (comparison adj).obj B → A и B → comparisonRightAdjointObj adj A как канонического эквивиентного отображения.

LaTeX

$$$((\mathrm{comparison}\ adj).obj B \to A) \cong (B \to \mathrm{comparisonRightAdjointObj}\ adj A).$$$

Lean4

/-- We have a bijection of homsets which will be used to construct the right adjoint to the comparison
functor.
-/
@[simps!]
def comparisonRightAdjointHomEquiv (A : adj.toComonad.Coalgebra) (B : C)
    [HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] :
    ((comparison adj).obj B ⟶ A) ≃ (B ⟶ comparisonRightAdjointObj adj A)
    where
  toFun
    f := by
    refine equalizer.lift (adj.homEquiv _ _ f.f) ?_
    simp only [Adjunction.toComonad_coe, Functor.comp_obj, Adjunction.homEquiv_unit, Category.assoc, ← G.map_comp,
      ← f.h, comparison_obj_A, comparison_obj_a]
    rw [Functor.comp_map, Functor.map_comp, Adjunction.unit_naturality_assoc, Adjunction.unit_naturality]
  invFun
    f := by
    refine ⟨(adj.homEquiv _ _).symm (f ≫ (equalizer.ι _ _)), (adj.homEquiv _ _).injective ?_⟩
    simp only [Adjunction.toComonad_coe, Functor.comp_obj, comparison_obj_A, comparison_obj_a,
      Adjunction.homEquiv_counit, Functor.map_comp, Category.assoc, Functor.comp_map, Adjunction.homEquiv_unit,
      Adjunction.unit_naturality_assoc, Adjunction.unit_naturality, Adjunction.right_triangle_components_assoc]
    congr 1
    exact (equalizer.condition _ _).symm
  left_inv f := by aesop
  right_inv f := by apply equalizer.hom_ext; simp

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