Kurosh Cover Action

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

@[instance_reducible]

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

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

Equations

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

theorem GraphCoveringTheory.Kurosh.Internal.rightCosetMk_mul_out_mk {P : Type u} [Group P] (K : Subgroup P) (p r : P) : rightCosetMk K (p * Quotient.out (rightCosetMk K r)) = rightCosetMk K (p * r)

theorem GraphCoveringTheory.Kurosh.Internal.coverEdgeSource_smul {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (p q : CoverSource G H) (e : CoverEdge G H) : coverEdgeSource G H (p * q, e) = p • coverEdgeSource G H (q, e)

theorem GraphCoveringTheory.Kurosh.Internal.coverEdgeTarget_smul {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (p q : CoverSource G H) (e : CoverEdge G H) : coverEdgeTarget G H (p * q, e) = p • coverEdgeTarget G H (q, e)

noncomputable def GraphCoveringTheory.Kurosh.coverEdgeAction {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (p : CoverSource G H) {x y : CoverVertex G H} (d : x ⟶ y) : p • x ⟶ p • y

Translate an auxiliary covering edge by a covering-group element.

Equations

• GraphCoveringTheory.Kurosh.coverEdgeAction G H p d = ⟨(p * (↑d).1, (↑d).2), ⋯⟩

noncomputable def GraphCoveringTheory.Kurosh.coverActionPrefunctor {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (p : CoverSource G H) : CoverVertex G H ⥤q CoverVertex G H

Translation by a covering-group element as a quiver prefunctor.

Equations

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

noncomputable def GraphCoveringTheory.Kurosh.coverActionSymmPrefunctor {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (p : CoverSource G H) : Quiver.Symmetrify (CoverVertex G H) ⥤q Quiver.Symmetrify (CoverVertex G H)

Extend covering-group translation to both edge orientations.

Equations

• GraphCoveringTheory.Kurosh.coverActionSymmPrefunctor G H p = (GraphCoveringTheory.Kurosh.coverActionPrefunctor G H p).symmetrify

noncomputable def GraphCoveringTheory.Kurosh.coverPathAction {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (p : CoverSource G H) {x y : CoverVertex G H} (q : Quiver.Path x y) : Quiver.Path (p • x) (p • y)

Translate a symmetrified path in the auxiliary covering graph.

Equations

• GraphCoveringTheory.Kurosh.coverPathAction G H p q = (GraphCoveringTheory.Kurosh.coverActionSymmPrefunctor G H p).mapPath q

theorem GraphCoveringTheory.Kurosh.Internal.coverPathAction_nil {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (p : CoverSource G H) (x : CoverVertex G H) : coverPathAction G H p Quiver.Path.nil = Quiver.Path.nil

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

theorem GraphCoveringTheory.Kurosh.Internal.coverVertexRange_action_one {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (a : RawBassSerreOrbitVertex G H) (k : ↥(treeVertexStabilizer G H a)) : (treeKuroshVertexInclusion G H a) k • coverVertexMk G H a 1 = coverVertexMk G H a 1

theorem GraphCoveringTheory.Kurosh.Internal.coverFactorLoopPath {ι : 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.coverFactorLoopPath_value {ι : 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)))