singletonEquiv — Mathlib

English

There is an explicit equivalence between the family of elements on a singleton f and the value P.op X, given by evaluation at f.

Русский

Существует явное эквивалентное отображение между семейством элементов над синглетоном f и элементами P.op X, задаваемое вычислением на f.

LaTeX

$$$(\\text{singleton } f).\\mathrm{FamilyOfElements} P \\; \\cong\\; P(\\mathrm{op}\,X)$$$

Lean4

/-- A family of elements on `{ f : X ⟶ Y }` is an element of `F(X)`. -/
@[simps apply, simps -isSimp symm_apply]
def singletonEquiv {X Y : C} (f : X ⟶ Y) : (singleton f).FamilyOfElements P ≃ P.obj (op X)
    where
  toFun x := x f (by simp)
  invFun x Z g hg := P.map (eqToHom <| by cases hg; rfl).op x
  left_inv x := by ext _ _ ⟨rfl⟩; simp
  right_inv x := by simp

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