English
The uncurried version of curry; given a monoid homomorphism F: G → (X → H) ⋊ G with a coherence condition, one gets a functor from the action category to the one-object category H.
Русский
Развернутая версия каррирования: дано отображение F из G в полупроизведение (X→H) ⋊ G с условием согласованности, и получается функтор из категории действия в категорию с одним объектом H.
LaTeX
$$$\text{uncurry}(F,sane) : \mathsf{ActionCategory}(G,X) \to \mathsf{SingleObj}(H)$$$
Lean4
/-- Given `G` acting on `X`, a group homomorphism `φ : G →* (X → H) ⋊ G` can be uncurried to
a functor from the action groupoid to `H`, provided that `φ g = (_, g)` for all `g`. -/
@[simps]
def uncurry (F : G →* (X → H) ⋊[mulAutArrow] G) (sane : ∀ g, (F g).right = g) : ActionCategory G X ⥤ SingleObj H
where
obj _ := ()
map {_ b} f := (F f.val).left b.back
map_id
x := by
dsimp
rw [F.map_one]
rfl
map_comp f
g := by
cases g using ActionCategory.cases
simp [SingleObj.comp_as_mul, sane]
rfl
