instHasForget₂Action — Mathlib

English

There is a forgetful 2-step functor from ContAction V G to Action V G, reflecting the underlying action structure by forgetting the continuous topology.

Русский

Существует забывающий двухшаговый функтор из ContAction V G в Action V G, который забывает непрерывную топологическую структуру, оставляя только действие.

LaTeX

$$$\\text{HasForget₂} (\\mathrm{ContAction} V G)\\;\\rightarrow\\; (\\mathrm{Action} V G)$ expresses the forgetful relation.$$

Lean4

instance : HasForget₂ (ContAction V G) (Action V G) :=
  FullSubcategory.hasForget₂ (IsContinuous (V := V) (G := G))

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