English
Auxiliary lemma showing the map F.map f equals F.map (homOfPair b.back f.val) for morphisms f, used in currying construction.
Русский
Вспомогательная лемма, показывающая, что отображение F.map f равно F.map (homOfPair b.back f.val) для морфизмов f, используемая при каррировании.
Lean4
/-- Given `G` acting on `X`, a functor from the corresponding action groupoid to a group `H`
can be curried to a group homomorphism `G →* (X → H) ⋊ G`. -/
@[simps]
def curry (F : ActionCategory G X ⥤ SingleObj H) : G →* (X → H) ⋊[mulAutArrow] G :=
have F_map_eq : ∀ {a b} {f : a ⟶ b}, F.map f = (F.map (homOfPair b.back f.val) : H) :=
by
apply ActionCategory.cases
intros
rfl
{ toFun := fun g => ⟨fun b => F.map (homOfPair b g), g⟩
map_one' := by
dsimp
ext1
· ext b
exact F_map_eq.symm.trans (F.map_id b)
rfl
map_mul' := by
intro g h
ext b
· exact F_map_eq.symm.trans (F.map_comp (homOfPair (g⁻¹ • b) h) (homOfPair b g))
rfl }
