resId — Mathlib

English

Restriction along a monoid equivalence f: G ≃* H yields an equivalence of action categories.

Русский

Ограничение по эквивалентности моноидов $G \simeq H$ порождает эквивалентность категорий действий.

LaTeX

$$def resEquiv {G H} [Monoid G] [Monoid H] (f : G ≃* H) : Action V H ⇌ Action V G$$

Lean4

/-- The natural isomorphism from restriction along the identity homomorphism to
the identity functor on `Action V G`.
-/
@[simps!]
def resId {G : Type*} [Monoid G] : res V (MonoidHom.id G) ≅ 𝟭 (Action V G) :=
  NatIso.ofComponents fun M => mkIso (Iso.refl _)

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