instLawfulFunctor — Mathlib

English

The Witt vector functor is lawful: it preserves identities and composition of maps.

Русский

Функтор Witt‑векторов является законным: сохраняет тождественные отображения и композицию отображений.

LaTeX

$$$\\mathrm{WittVector}_p \\text{ is a LawfulFunctor};\\ map_{p}(\\mathrm{id}) = \\mathrm{id},\\ map_{p}(f \\circ g) = map_{p}(f) \\circ map_{p}(g).$$$

Lean4

instance : LawfulFunctor (WittVector p) where
  map_const := rfl
  id_map _ := rfl
  comp_map _ _ _ := rfl

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