Kurosh Path Injective

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

@[instance_reducible]

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

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

Equations

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

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

Interpret a raw symmetrified Bass-Serre path in the path category.

Equations

• GraphCoveringTheory.Kurosh.rawPathToCat G p = p

theorem GraphCoveringTheory.Kurosh.rawPathToCat_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) : rawPathToCat G (catPathToRaw G p) = p

theorem GraphCoveringTheory.Kurosh.catPathToRaw_rawPathToCat {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {a b : Quiver.Symmetrify (RawBassSerreVertex G)} (p : Quiver.Path a b) : catPathToRaw G (rawPathToCat G p) = p

theorem GraphCoveringTheory.Kurosh.coverPathLiftData_eq_of_quotient_map_eq {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a : Quiver.Symmetrify (RawBassSerreVertex G)} (p q : Quiver.Path ((coverPrefunctor G H).symmetrify.obj (coverVertexMk G H (rawBassSerreOrbitRoot G H) 1)) a) (h : (CategoryTheory.Quotient.functor Quiver.FreeGroupoid.redStep).map (rawPathToCat G p) = (CategoryTheory.Quotient.functor Quiver.FreeGroupoid.redStep).map (rawPathToCat G q)) : (coverPathLiftData G H p).x = (coverPathLiftData G H q).x

theorem GraphCoveringTheory.Kurosh.Internal.rawFreeGroupoid_hom_subsingleton {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {x y : Quiver.FreeGroupoid (RawBassSerreVertex G)} : Subsingleton (x ⟶ y)

theorem GraphCoveringTheory.Kurosh.coverCatPathLiftData_eq_of_target_tree {ι : 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) : (coverPathLiftData G H (catPathToRaw G p)).x = (coverPathLiftData G H (catPathToRaw G q)).x