instMulActionCarrierObjTopCatForget₂

English

Let X be an action of a monoid G on an object V. The carrier of X (the underlying topological space) inherits a left G-action defined by g · x = (ρ_g)(x), where ρ is the action morphism of G on X. This action satisfies the unit and associativity laws: 1 · x = x and (gh) · x = g · (h · x) for all g,h ∈ G and x in the carrier.

Русский

Пусть X — действие моноида G на объекты V. Носитель X (указанный сверху топологический носитель) наследует левое действие G, заданное как g · x = (ρ_g)(x). Это действие удовлетворяет единичному и ассоциативному законам: 1·x = x и (gh)·x = g·(h·x) для всех g,h ∈ G и всех x в носителе.

LaTeX

$$$\\forall X\\ (X:\\text{Action } V\\ G)\\;\\text{MulAction } G\\;((\\mathrm{forget}_2\\,TopCat).obj X)\\\\\n\\text{with }g\\cdot x := ((\\mathrm{forget}_2\\,TopCat).map (X.\\rho\\ g))\\,x\\n\\\\\n\\text{and } 1\\cdot x = x,\; (gh)\\cdot x = g\\cdot(h\\cdot x).$$$

Lean4

instance (X : Action V G) : MulAction G ((CategoryTheory.forget₂ _ TopCat).obj X)
    where
  smul g x := ((CategoryTheory.forget₂ _ TopCat).map (X.ρ g)) x
  one_smul
    x := by
    change ((CategoryTheory.forget₂ _ TopCat).map (X.ρ 1)) x = x
    simp
  mul_smul g h
    x :=
    by
    change
      (CategoryTheory.forget₂ _ TopCat).map (X.ρ (g * h)) x =
        ((CategoryTheory.forget₂ _ TopCat).map (X.ρ h) ≫ (CategoryTheory.forget₂ _ TopCat).map (X.ρ g)) x
    rw [← Functor.map_comp, map_mul]
    rfl

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