English
If φ is a functor between groupoids that is object-injective and essentially surjective on objects, and S is a normal subgroupoid of the source, then the image of S under φ is a normal subgroupoid of the target.
Русский
Если φ — функционор между группоидами, сохраняющий инъективность на объектах и сюръективность объектов, и S — нормальная подгруппоида в источнике, то образ S под действием φ является нормальной подгруппоида в целевом.
LaTeX
$$$\\forall C,D [Groupoid\\ C] [Groupoid\\ D] (\\varphi : C \\to D) (h_\\varphi : Function.Injective (\\varphi.obj)) (h_\\varphi' : im \\varphi \\ h_\\varphi = \\top) (S : Subgroupoid\\ C) (Sn : S.IsNormal),\quad (map\\ \\varphi\\ h_\\varphi\\ S).IsNormal$$$
Lean4
theorem isNormal_map (hφ : Function.Injective φ.obj) (hφ' : im φ hφ = ⊤) (Sn : S.IsNormal) : (map φ hφ S).IsNormal :=
{ wide := fun d => by
obtain ⟨c, rfl⟩ := obj_surjective_of_im_eq_top φ hφ hφ' d
change Map.Arrows φ hφ S _ _ (𝟙 _); rw [← Functor.map_id]
constructor; exact Sn.wide c
conj := fun {d d'} g δ hδ => by
rw [mem_map_iff] at hδ
obtain ⟨c, c', γ, cd, cd', γS, hγ⟩ := hδ; subst_vars; cases hφ cd'
have : d' ∈ (im φ hφ).objs := by rw [hφ']; apply mem_top_objs
rw [mem_im_objs_iff] at this
obtain ⟨c', rfl⟩ := this
have : g ∈ (im φ hφ).arrows (φ.obj c) (φ.obj c') := by rw [hφ']; trivial
rw [mem_im_iff] at this
obtain ⟨b, b', f, hb, hb', _, hf⟩ := this; cases hφ hb; cases hφ hb'
change Map.Arrows φ hφ S (φ.obj c') (φ.obj c') _
simp only [eqToHom_refl, Category.comp_id, Category.id_comp, inv_eq_inv]
suffices Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (φ.map <| Groupoid.inv f ≫ γ ≫ f) by
simp only [inv_eq_inv, Functor.map_comp, Functor.map_inv] at this; exact this
constructor; apply Sn.conj f γS }
