Kurosh Cover Lift

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

@[instance_reducible]

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

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

Equations

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

theorem GraphCoveringTheory.Kurosh.Internal.coverSymmCovering {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : (coverPrefunctor G H).symmetrify.IsCovering

noncomputable def GraphCoveringTheory.Kurosh.coverStarEquiv {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (u : CoverVertex G H) : Quiver.Star u ≃ Quiver.Star ((coverPrefunctor G H).symmetrify.obj u)

The covering projection induces an equivalence on symmetrified outgoing edges.

Equations

• GraphCoveringTheory.Kurosh.coverStarEquiv G H u = Equiv.ofBijective ((GraphCoveringTheory.Kurosh.coverPrefunctor G H).symmetrify.star u) ⋯

noncomputable def GraphCoveringTheory.Kurosh.coverStarLift {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (u : CoverVertex G H) {v : Quiver.Symmetrify (RawBassSerreVertex G)} (e : (coverPrefunctor G H).symmetrify.obj u ⟶ v) : Quiver.Star u

Lift a symmetrified outgoing edge using the star equivalence.

Equations

• GraphCoveringTheory.Kurosh.coverStarLift G H u e = (GraphCoveringTheory.Kurosh.coverStarEquiv G H u).symm ⟨v, e⟩

theorem GraphCoveringTheory.Kurosh.Internal.coverStarLift_map {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (u : CoverVertex G H) {v : Quiver.Symmetrify (RawBassSerreVertex G)} (e : (coverPrefunctor G H).symmetrify.obj u ⟶ v) : ∃ (h : (coverPrefunctor G H).symmetrify.obj (coverStarLift G H u e).fst = v), Quiver.Hom.cast ⋯ h ((coverPrefunctor G H).symmetrify.map (coverStarLift G H u e).snd) = e

theorem GraphCoveringTheory.Kurosh.Internal.coverStar_eq_mk_of_map_cast {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (u : CoverVertex G H) (s : Quiver.Star u) {v : Quiver.Symmetrify (RawBassSerreVertex G)} (e : (coverPrefunctor G H).symmetrify.obj u ⟶ v) (hobj : (coverPrefunctor G H).symmetrify.obj s.fst = v) (hmap : Quiver.Hom.cast ⋯ hobj ((coverPrefunctor G H).symmetrify.map s.snd) = e) : (coverPrefunctor G H).symmetrify.star u s = ⟨v, e⟩

theorem GraphCoveringTheory.Kurosh.Internal.hom_reverse_cast {U : Type u} [q : Quiver U] [Quiver.HasReverse U] {a b a' b' : U} (e : a ⟶ b) (ha : a = a') (hb : b = b') : Quiver.reverse (Quiver.Hom.cast ha hb e) = Quiver.Hom.cast hb ha (Quiver.reverse e)

theorem GraphCoveringTheory.Kurosh.Internal.coverReverseStar_map {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (u : CoverVertex G H) (d : Quiver.Star u) {v : Quiver.Symmetrify (RawBassSerreVertex G)} (e : (coverPrefunctor G H).symmetrify.obj u ⟶ v) (hobj : (coverPrefunctor G H).symmetrify.obj d.fst = v) (hmap : Quiver.Hom.cast ⋯ hobj ((coverPrefunctor G H).symmetrify.map d.snd) = e) : (coverPrefunctor G H).symmetrify.map (Quiver.reverse d.snd) = Quiver.Hom.cast ⋯ ⋯ (Quiver.reverse e)

theorem GraphCoveringTheory.Kurosh.Internal.coverReverseStar_map_transport {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (u : CoverVertex G H) (d : Quiver.Star u) {v w : Quiver.Symmetrify (RawBassSerreVertex G)} (e : v ⟶ w) (hobj : (coverPrefunctor G H).symmetrify.obj u = v) (htarget : (coverPrefunctor G H).symmetrify.obj d.fst = w) (hmap : Quiver.Hom.cast ⋯ htarget ((coverPrefunctor G H).symmetrify.map d.snd) = Quiver.Hom.cast ⋯ ⋯ e) : Quiver.Hom.cast ⋯ hobj ((coverPrefunctor G H).symmetrify.map (Quiver.reverse d.snd)) = Quiver.Hom.cast ⋯ ⋯ (Quiver.reverse e)

structure GraphCoveringTheory.Kurosh.CoverPathLiftData {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {v : Quiver.Symmetrify (RawBassSerreVertex G)} : Type (max (u + 1) (v + 1))

A lifted path from the auxiliary root together with its endpoint identification.

• x : CoverVertex G H

  The endpoint of the lifted path in the auxiliary covering graph.

• path : Quiver.Path (coverVertexMk G H (rawBassSerreOrbitRoot G H) 1) self.x

  The lifted path from the auxiliary covering root to x.

• endpoint : (coverPrefunctor G H).symmetrify.obj self.x = v

noncomputable def GraphCoveringTheory.Kurosh.coverPathLiftData {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {v : Quiver.Symmetrify (RawBassSerreVertex G)} : Quiver.Path ((coverPrefunctor G H).symmetrify.obj (coverVertexMk G H (rawBassSerreOrbitRoot G H) 1)) v → CoverPathLiftData G H

Lift a Bass-Serre path starting at the identity vertex to a path starting at the auxiliary covering root.

Equations

• One or more equations did not get rendered due to their size.

theorem GraphCoveringTheory.Kurosh.Internal.path_cast_cons_mid {U : Type u} [q : Quiver U] {a b c b' c' : U} (p : Quiver.Path a b) (e : b ⟶ c) (hb : b = b') (hc : c = c') : Quiver.Path.cast ⋯ hc (p.cons e) = (Quiver.Path.cast ⋯ hb p).cons (Quiver.Hom.cast hb hc e)

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

theorem GraphCoveringTheory.Kurosh.Internal.coverPathLiftData_backtrack_endpoint {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {v w : Quiver.Symmetrify (RawBassSerreVertex G)} (p : Quiver.Path ((coverPrefunctor G H).symmetrify.obj (coverVertexMk G H (rawBassSerreOrbitRoot G H) 1)) v) (e : v ⟶ w) : (coverPathLiftData G H ((p.cons e).cons (Quiver.reverse e))).x = (coverPathLiftData G H p).x

theorem GraphCoveringTheory.Kurosh.Internal.coverStarLift_fst_eq_of_heq {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (u u' : CoverVertex G H) {v : Quiver.Symmetrify (RawBassSerreVertex G)} (e : (coverPrefunctor G H).symmetrify.obj u ⟶ v) (e' : (coverPrefunctor G H).symmetrify.obj u' ⟶ v) (hu : u ≍ u') (he : e ≍ e') : (coverStarLift G H u e).fst = (coverStarLift G H u' e').fst

theorem GraphCoveringTheory.Kurosh.Internal.coverPathLiftData_append_edge_endpoint {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {v w : Quiver.Symmetrify (RawBassSerreVertex G)} (p q : Quiver.Path ((coverPrefunctor G H).symmetrify.obj (coverVertexMk G H (rawBassSerreOrbitRoot G H) 1)) v) (h : (coverPathLiftData G H p).x = (coverPathLiftData G H q).x) (e : v ⟶ w) : (coverPathLiftData G H (p.cons e)).x = (coverPathLiftData G H (q.cons e)).x

theorem GraphCoveringTheory.Kurosh.Internal.coverPathLiftData_append_endpoint {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {v w : Quiver.Symmetrify (RawBassSerreVertex G)} (p q : Quiver.Path ((coverPrefunctor G H).symmetrify.obj (coverVertexMk G H (rawBassSerreOrbitRoot G H) 1)) v) (h : (coverPathLiftData G H p).x = (coverPathLiftData G H q).x) (r : Quiver.Path v w) : (coverPathLiftData G H (p.comp r)).x = (coverPathLiftData G H (q.comp r)).x