English
Let C be a groupoid and S a subgroupoid. Then S carries a natural groupoid structure with objects S.objs and morphisms from a to b given by S.arrows a b, with identities and composition induced from C (and inverses accordingly). In other words, S can be regarded as a groupoid obtained by restriction of the groupoid C to the arrows and objects of S.
Русский
Пусть C — группоида и S — подгруппоида. Тогда S естественным образом образует групподиаду: объектами служат S.objs, морфизмами между a и b являются стрелки S.arrows a b, а тождественные морфизмы, композиция и инверсы наследуются от C.
LaTeX
$$$S$ inherits a groupoid structure on its object set with ${\rm Hom}_S(a,b)=S.{\rm arrows}(a,b)$ for $a,b\in S.{\rm objs}$, with identities $\mathrm{id}_a$ taken from C, composition and inverses induced from C.$$
Lean4
/-- The coercion of a subgroupoid as a groupoid -/
@[simps comp_coe, simps -isSimp inv_coe]
instance coe : Groupoid S.objs where
Hom a b := S.arrows a.val b.val
id a := ⟨𝟙 a.val, id_mem_of_nonempty_isotropy S a.val a.prop⟩
comp p q := ⟨p.val ≫ q.val, S.mul p.prop q.prop⟩
inv p := ⟨Groupoid.inv p.val, S.inv p.prop⟩
