Kurosh Free Fiber

Adapted for Lean Pool from Arthur742Ramos/KuroshSubgroupTheorem, commit 911707126c8b9bb0c764bf853008fe1053c0aad9: imports, API compatibility, and proof organization were revised.

theorem GraphCoveringTheory.Kurosh.Internal.coverFreeGroupoidPathHom_eq_quotient_map {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (p : Quiver.Path a b) : coverFreeGroupoidPathHom G H p = (CategoryTheory.Quotient.functor Quiver.FreeGroupoid.redStep).map p

theorem GraphCoveringTheory.Kurosh.Internal.coverFreePath_exists {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (z : (Quiver.FreeGroupoid.of (RawBassSerreOrbitVertex G H)).obj a ⟶ (Quiver.FreeGroupoid.of (RawBassSerreOrbitVertex G H)).obj b) : ∃ (p : Quiver.Path a b), coverFreeGroupoidPathHom G H p = z