map₁ — Mathlib

English

The forget X is left adjoint (via costarAdjForget X).

Русский

Forget X — левый сопряжённый.

LaTeX

$$Under.forget X IsLeftAdjoint$$

Lean4

/-- "Functoriality" of `MakesOverArrow η s` in `η`. -/
theorem map₁ {F G : Cᵒᵖ ⥤ Type v} {η : F ⟶ A} {μ : G ⟶ A} {ε : F ⟶ G} (hε : ε ≫ μ = η) {X : C} {s : yoneda.obj X ⟶ A}
    {u : F.obj (op X)} (h : MakesOverArrow η s u) : MakesOverArrow μ s (ε.app _ u) :=
  ⟨by rw [← elementwise_of% NatTrans.comp_app ε μ, hε, h.app]⟩

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