Kurosh Cover Connected

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

@[instance_reducible]

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

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

Equations

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

theorem GraphCoveringTheory.Kurosh.Internal.coverFreeFactorLoopPath {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (x : KuroshFreePart G H) : Nonempty (Quiver.Path (coverVertexMk G H (rawBassSerreOrbitRoot G H) 1) (coverVertexMk G H (rawBassSerreOrbitRoot G H) ((treeKuroshFreeInclusion G H) x)))

theorem GraphCoveringTheory.Kurosh.Internal.coverFactorLoopPath_rawTree {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (a : RawBassSerreOrbitVertex G H) (k : ↥(treeVertexStabilizer G H a)) : Nonempty (Quiver.Path (coverVertexMk G H (rawBassSerreOrbitRoot G H) 1) (coverVertexMk G H (rawBassSerreOrbitRoot G H) ((treeKuroshVertexInclusion G H a) k)))

theorem GraphCoveringTheory.Kurosh.Internal.coverRootFiberPath {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (p : CoverSource G H) : Nonempty (Quiver.Path (coverVertexMk G H (rawBassSerreOrbitRoot G H) 1) (coverVertexMk G H (rawBassSerreOrbitRoot G H) p))

theorem GraphCoveringTheory.Kurosh.Internal.coverSource_rootedConnected {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : Quiver.RootedConnected (have this := coverVertexMk G H (rawBassSerreOrbitRoot G H) 1; this)