English
Given a family F of G-sets with actions, the product ∏ F(i) carries a diagonal G-action and forms the limit cone in the category of G-sets; this cone exhibits that the product in G-sets is the categorical product.
Русский
Пусть дана семья множества с действием G, тогда произведение ∏ F(i) несёт диагональное действие G и образует предел в категории G-множест; этот конус реализует произведение в G-множествах как категориальное произведение.
LaTeX
$$$\text{LimitCone}(\mathrm{Discrete}.\mathrm{functor}(i\mapsto \mathrm{Action.ofMulAction}(G,F(i))))$$$
Lean4
/-- Given a family `F` of types with `G`-actions, this is the limit cone demonstrating that the
product of `F` as types is a product in the category of `G`-sets. -/
def ofMulActionLimitCone {ι : Type v} (G : Type max v u) [Monoid G] (F : ι → Type max v u)
[∀ i : ι, MulAction G (F i)] : LimitCone (Discrete.functor fun i : ι => Action.ofMulAction G (F i))
where
cone :=
{ pt := Action.ofMulAction G (∀ i : ι, F i)
π := Discrete.natTrans (fun i => ⟨fun x => x i.as, fun _ => rfl⟩) }
isLimit :=
{ lift := fun s =>
{ hom := fun x i => (s.π.app ⟨i⟩).hom x
comm := fun g => by
ext x
funext j
exact congr_fun ((s.π.app ⟨j⟩).comm g) x }
fac := fun _ _ => rfl
uniq := fun s f h => by
ext x
funext j
dsimp at *
rw [← h ⟨j⟩]
rfl }
