Kurosh Path Relation Invariant

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

@[instance_reducible]

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

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

Equations

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

theorem GraphCoveringTheory.Kurosh.catStep {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {b c d : Quiver.Symmetrify (RawBassSerreVertex G)} (p : (CategoryTheory.Paths.of (Quiver.Symmetrify (RawBassSerreVertex G))).obj ((coverPrefunctor G H).symmetrify.obj (coverVertexMk G H (rawBassSerreOrbitRoot G H) 1)) ⟶ (CategoryTheory.Paths.of (Quiver.Symmetrify (RawBassSerreVertex G))).obj b) (e : b ⟶ c) (q : (CategoryTheory.Paths.of (Quiver.Symmetrify (RawBassSerreVertex G))).obj b ⟶ (CategoryTheory.Paths.of (Quiver.Symmetrify (RawBassSerreVertex G))).obj d) : have ep := e.toPath; have en := (Quiver.reverse e).toPath; (coverPathLiftData G H (catPathToRaw G (CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id ((CategoryTheory.Paths.of (Quiver.Symmetrify (RawBassSerreVertex G))).obj b)) q)))).x = (coverPathLiftData G H (catPathToRaw G (CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ep en) q)))).x

theorem GraphCoveringTheory.Kurosh.catEqv {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a : Quiver.Symmetrify (RawBassSerreVertex G)} (p q : (CategoryTheory.Paths.of (Quiver.Symmetrify (RawBassSerreVertex G))).obj ((coverPrefunctor G H).symmetrify.obj (coverVertexMk G H (rawBassSerreOrbitRoot G H) 1)) ⟶ (CategoryTheory.Paths.of (Quiver.Symmetrify (RawBassSerreVertex G))).obj a) (h : Relation.EqvGen (CategoryTheory.HomRel.CompClosure Quiver.FreeGroupoid.redStep) p q) : (coverPathLiftData G H (catPathToRaw G p)).x = (coverPathLiftData G H (catPathToRaw G q)).x