Kurosh Path Relation

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

@[instance_reducible]

noncomputable def GraphCoveringTheory.Kurosh.kuroshPathRelationDecidableEq (α : Type u_1) : DecidableEq α

Classical equality used locally in this part of the Kurosh construction.

Equations

• GraphCoveringTheory.Kurosh.kuroshPathRelationDecidableEq α = Classical.decEq α

def GraphCoveringTheory.Kurosh.catPathToRaw {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {a b : Quiver.Symmetrify (RawBassSerreVertex G)} (p : (CategoryTheory.Paths.of (Quiver.Symmetrify (RawBassSerreVertex G))).obj a ⟶ (CategoryTheory.Paths.of (Quiver.Symmetrify (RawBassSerreVertex G))).obj b) : Quiver.Path a b

Recover the raw symmetrified Bass-Serre path from a path-category morphism.

Equations

• GraphCoveringTheory.Kurosh.catPathToRaw G p = p