map — Mathlib

English

There is a map on Fix F given by applying wMap to representatives, producing a well-defined map on the quotient (i.e., Fix F is a functor).

Русский

Существуют отображения на Fix F, задаваемые применением wMap к представителям, что обеспечивает структуру функторa.

LaTeX

$$$\mathrm{Fix.map} : \mathrm{Fix} F\;\alpha \to \mathrm{Fix} F\;\beta,\quad \mathrm{map}(g)(\overline{x}) = \overline{\,\mathrm{wMap} \;g\; x\}$$$

Lean4

/-- `Fix F` is a functor -/
def map {α β : TypeVec n} (g : α ⟹ β) : Fix F α → Fix F β :=
  Quotient.lift (fun x : q.P.W α => ⟦q.P.wMap g x⟧) fun _a _b h => Quot.sound (wEquiv_map _ _ _ h)

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