English
For an injective φ.obj and a Subgroupoid S, a morphism f lies in map φ hφ S iff there exist a,b,g,ha,hb,hg with f equal to the conjugation of φ.map g by ha,hb and hg ∈ S.arrows.
Русский
Пусть φ инъективен по объектам, тогда f ∈ map φ hφ S эквивалентно существованию a,b,g,ha,hb, hg ∈ S.arrows такие, что f = eqToHom ha.symm ≫ φ.map g ≫ eqToHom hb.
LaTeX
$$$f \in (map φ hφ S).arrows\; c\; d \iff \\exists a,b,g,ha,hb,hg:\ g\in S.arrows a b \land f = eqToHom ha.symm \gg (φ.map g) \gg eqToHom hb$$$
Lean4
theorem mem_map_iff (hφ : Function.Injective φ.obj) (S : Subgroupoid C) {c d : D} (f : c ⟶ d) :
f ∈ (map φ hφ S).arrows c d ↔
∃ (a b : C) (g : a ⟶ b) (ha : φ.obj a = c) (hb : φ.obj b = d) (_hg : g ∈ S.arrows a b),
f = eqToHom ha.symm ≫ φ.map g ≫ eqToHom hb :=
Map.arrows_iff φ hφ S f
