English
Restriction along the identity monoid homomorphism is naturally isomorphic to the identity functor on Action V G.
Русский
Ограничение по единичному гомоморфизму идентичности изоморфно единичному функтору на Action V G.
LaTeX
$$resId {G} : res V (MonoidHom.id G) ≅ 𝟭 (Action V G)$$
Lean4
/-- Actions/representations of the trivial group are just objects in the ambient category. -/
def actionPunitEquivalence : Action V PUnit ≌ V
where
functor := forget V _
inverse :=
{ obj := fun X => ⟨X, 1⟩
map := fun f => ⟨f, fun ⟨⟩ => by simp⟩ }
unitIso :=
NatIso.ofComponents fun X =>
mkIso (Iso.refl _) fun ⟨⟩ =>
by
simp only [Functor.id_obj, MonoidHom.one_apply, End.one_def, Functor.comp_obj, forget_obj, Iso.refl_hom,
Category.comp_id]
exact ρ_one X
counitIso := NatIso.ofComponents fun _ => Iso.refl _
