freeHomEquiv — Mathlib

English

There is a natural bijection between morphisms from the free X to M and functions X → M, i.e., the free-forgetful adjunction is represented by a hom-set bijection.

Русский

Существует естественная биекция между морфизмами free(X) → M и функциями X → M, то есть свободно-забывающая адъюнкция задаётся биекцией множеств.

LaTeX

$$$\mathrm{FreeHomEquiv}: ((\mathrm{Free}(R)\!\cdot X \to M) \cong X \to M$)$$

Lean4

/-- The bijection `((free R).obj X ⟶ M) ≃ (X → M)` when `X` is a type and `M` a module. -/
@[simps]
def freeHomEquiv {X : Type u} {M : ModuleCat.{u} R} : ((free R).obj X ⟶ M) ≃ (X → M)
    where
  toFun φ x := φ (freeMk x)
  invFun ψ := freeDesc ψ
  left_inv _ := by ext; simp
  right_inv _ := by ext; simp

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