Kurosh Path Endpoint

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

@[instance_reducible]

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

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

Equations

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

theorem GraphCoveringTheory.Kurosh.Internal.coverVertexMap_root {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : (coverPrefunctor G H).symmetrify.obj (coverVertexMk G H (rawBassSerreOrbitRoot G H) 1) = RawBassSerreVertex.central 1

theorem GraphCoveringTheory.Kurosh.Internal.coverPathLiftData_endpoint_eq_of_mapPath {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {x : CoverVertex G H} (s : Quiver.Path (coverVertexMk G H (rawBassSerreOrbitRoot G H) 1) x) {v : Quiver.Symmetrify (RawBassSerreVertex G)} (p : Quiver.Path ((coverPrefunctor G H).symmetrify.obj (coverVertexMk G H (rawBassSerreOrbitRoot G H) 1)) v) (hobj : (coverPrefunctor G H).symmetrify.obj x = v) (hmap : Quiver.Path.cast ⋯ hobj ((coverPrefunctor G H).symmetrify.mapPath s) = p) : x = (coverPathLiftData G H p).x

theorem GraphCoveringTheory.Kurosh.Internal.coverPathLiftData_closed_endpoint {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {p : Quiver.Path ((coverPrefunctor G H).symmetrify.obj (coverVertexMk G H (rawBassSerreOrbitRoot G H) 1)) ((coverPrefunctor G H).symmetrify.obj (coverVertexMk G H (rawBassSerreOrbitRoot G H) 1))} : (coverPathLiftData G H p).x = coverVertexMk G H (rawBassSerreOrbitRoot G H) 1

theorem GraphCoveringTheory.Kurosh.Internal.coverVertexMk_eq_root_of_treeKuroshProductToH_eq_one {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (z : CoverSource G H) (hz : (treeKuroshProductToH G H) z = 1) : coverVertexMk G H (rawBassSerreOrbitRoot G H) z = coverVertexMk G H (rawBassSerreOrbitRoot G H) 1