English
Every morphism in the action groupoid is given by some pair (t,g); explicitly, any morphism f: a → b can be written as homOfPair t g for suitable t ∈ X and g ∈ G with a = g⁻¹ · t and b = t.
Русский
Каждый морфизм в группе действия задаётся некоторой парой (t,g); формально любой морфизм f: a → b можно записать как homOfPair t g для подходящих t ∈ X и g ∈ G с a = g⁻¹·t и b = t.
LaTeX
$$$\exists t \in X, \exists g \in G:\ a = g^{-1} \cdot t \land b = t \land f = \mathrm{homOfPair}(t,g)$$$
Lean4
/-- Any morphism in the action groupoid is given by some pair. -/
protected def cases {P : ∀ ⦃a b : ActionCategory G X⦄, (a ⟶ b) → Sort*} (hyp : ∀ t g, P (homOfPair t g)) ⦃a b⦄
(f : a ⟶ b) : P f := by
refine cast ?_ (hyp b.back f.val)
rcases a with ⟨⟨⟩, a : X⟩
rcases b with ⟨⟨⟩, b : X⟩
rcases f with ⟨g : G, h : g • a = b⟩
cases inv_smul_eq_iff.mpr h.symm
rfl
