The universal cover of the quotient graph of groups.

The source group is the explicit free product of the vertex stabilizers and the quotient free part. A cover vertex is a quotient-graph vertex together with a right coset of its source vertex group. This is the standard Bass--Serre construction, with the edge group trivial.

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

@[instance_reducible]

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

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

Equations

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

@[reducible, inline]

abbrev GraphCoveringTheory.Kurosh.CoverSource {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : Type (max (max u v) (u + 1) (v + 1))

The tree Kurosh product acting on the auxiliary covering graph.

Equations

• GraphCoveringTheory.Kurosh.CoverSource G H = GraphCoveringTheory.Kurosh.TreeKuroshProduct G H

@[reducible, inline]

abbrev GraphCoveringTheory.Kurosh.CoverVertexCoset {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (a : RawBassSerreOrbitVertex G H) : Type (max (max (u + 1) (v + 1)) u_1)

Cosets of the image of a vertex stabilizer in the tree Kurosh product.

Equations

• GraphCoveringTheory.Kurosh.CoverVertexCoset G H a = GraphCoveringTheory.Kurosh.RightCoset (GraphCoveringTheory.Kurosh.treeKuroshVertexInclusion G H a).range

@[reducible, inline]

abbrev GraphCoveringTheory.Kurosh.CoverVertex {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : Type (max (max u v) (max u_1 (v + 1)) (u + 1))

Vertices of the auxiliary cover, given by a quotient vertex and a stabilizer coset.

Equations

• GraphCoveringTheory.Kurosh.CoverVertex G H = ((a : GraphCoveringTheory.Kurosh.RawBassSerreOrbitVertex G H) × GraphCoveringTheory.Kurosh.CoverVertexCoset G H a)

@[reducible, inline]

abbrev GraphCoveringTheory.Kurosh.CoverEdge {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : Type (max u v)

An edge of the quotient graph, bundled with its endpoints.

Equations

• GraphCoveringTheory.Kurosh.CoverEdge G H = ((a : GraphCoveringTheory.Kurosh.RawBassSerreOrbitVertex G H) × (b : GraphCoveringTheory.Kurosh.RawBassSerreOrbitVertex G H) × (a ⟶ b))

noncomputable def GraphCoveringTheory.Kurosh.coverEdgeLetter {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (e : CoverEdge G H) : CoverSource G H

The based loop of a quotient edge included in the free factor of the covering group.

Equations

• GraphCoveringTheory.Kurosh.coverEdgeLetter G H e = (GraphCoveringTheory.Kurosh.treeKuroshFreeInclusion G H) (GraphCoveringTheory.Kurosh.quotientEdgeLoop G H e.snd.snd)

noncomputable def GraphCoveringTheory.Kurosh.coverEdgeSource {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (d : CoverSource G H × CoverEdge G H) : CoverVertex G H

The source coset of an edge labeled by a covering-group element.

Equations

• GraphCoveringTheory.Kurosh.coverEdgeSource G H d = ⟨d.2.fst, GraphCoveringTheory.Kurosh.rightCosetMk (GraphCoveringTheory.Kurosh.treeKuroshVertexInclusion G H d.2.fst).range d.1⟩

noncomputable def GraphCoveringTheory.Kurosh.coverEdgeTarget {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (d : CoverSource G H × CoverEdge G H) : CoverVertex G H

The target coset after multiplication by the inverse edge letter.

Equations

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

@[reducible]

def GraphCoveringTheory.Kurosh.coverQuiver {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : Quiver (CoverVertex G H)

The auxiliary quiver of stabilizer cosets and labeled quotient edges.

Equations

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

@[instance_reducible]

instance GraphCoveringTheory.Kurosh.coverQuiverInst {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : Quiver (CoverVertex G H)

Equations

• GraphCoveringTheory.Kurosh.coverQuiverInst G H = GraphCoveringTheory.Kurosh.coverQuiver G H

@[instance_reducible]

noncomputable instance GraphCoveringTheory.Kurosh.coverSourceMulAction {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : MulAction (CoverSource G H) (CoverVertex G H)

Equations

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

@[simp]

theorem GraphCoveringTheory.Kurosh.coverSourceMulAction_mk {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (p : CoverSource G H) (a : RawBassSerreOrbitVertex G H) (q : CoverVertexCoset G H a) : p • ⟨a, q⟩ = ⟨a, rightCosetMk (treeKuroshVertexInclusion G H a).range (p * Quotient.out q)⟩

theorem GraphCoveringTheory.Kurosh.coverSource_vertexRange_smul {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (a : RawBassSerreOrbitVertex G H) (k : ↥(treeKuroshVertexInclusion G H a).range) : ↑((treeKuroshProductToH G H) ↑k) • rawTreeRepresentative G H a = rawTreeRepresentative G H a

noncomputable def GraphCoveringTheory.Kurosh.coverVertexMap {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : CoverVertex G H → RawBassSerreVertex G

Evaluate a covering coset on the chosen representative in the Bass-Serre graph.

Equations

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

@[simp]

theorem GraphCoveringTheory.Kurosh.coverVertexMap_mk {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (a : RawBassSerreOrbitVertex G H) (p : CoverSource G H) : coverVertexMap G H ⟨a, rightCosetMk (treeKuroshVertexInclusion G H a).range p⟩ = ↑((treeKuroshProductToH G H) p) • rawTreeRepresentative G H a

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

Project an auxiliary covering edge to the Bass-Serre graph.

Equations

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

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

Construct an auxiliary covering vertex from a quotient vertex and a group element.

Equations

• GraphCoveringTheory.Kurosh.coverVertexMk G H a p = ⟨a, GraphCoveringTheory.Kurosh.rightCosetMk (GraphCoveringTheory.Kurosh.treeKuroshVertexInclusion G H a).range p⟩

def GraphCoveringTheory.Kurosh.coverBaseEdge {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (e : a ⟶ b) : CoverEdge G H

Bundle a quotient edge with its source and target.

Equations

• GraphCoveringTheory.Kurosh.coverBaseEdge G H e = ⟨a, ⟨b, e⟩⟩

noncomputable def GraphCoveringTheory.Kurosh.coverPositiveLiftEdge {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (e : a ⟶ b) (p : CoverSource G H) : coverVertexMk G H a p ⟶ coverVertexMk G H b (p * (coverEdgeLetter G H (coverBaseEdge G H e))⁻¹)

Lift a positively oriented quotient edge from a specified group representative.

Equations

• GraphCoveringTheory.Kurosh.coverPositiveLiftEdge G H e p = ⟨(p, GraphCoveringTheory.Kurosh.coverBaseEdge G H e), ⋯⟩

noncomputable def GraphCoveringTheory.Kurosh.coverNegativeLiftEdge {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (e : a ⟶ b) (p : CoverSource G H) : coverVertexMk G H b p ⟶ coverVertexMk G H a (p * coverEdgeLetter G H (coverBaseEdge G H e))

Lift a negatively oriented quotient edge from a specified group representative.

Equations

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

noncomputable def GraphCoveringTheory.Kurosh.coverGraphLabelPrefunctor {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : RawBassSerreOrbitVertex G H ⥤q CategoryTheory.SingleObj (CoverSource G H)ᵐᵒᵖ

Label quotient edges in the opposite covering group to respect path composition.

Equations

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

def GraphCoveringTheory.Kurosh.coverFreeGroupoidPathHom {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} : Quiver.Path a b → ((Quiver.FreeGroupoid.of (RawBassSerreOrbitVertex G H)).obj a ⟶ (Quiver.FreeGroupoid.of (RawBassSerreOrbitVertex G H)).obj b)

Interpret a raw symmetrified quotient path in its free groupoid.

Equations

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

theorem GraphCoveringTheory.Kurosh.coverFreeGroupoidPathHom_cons {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b c : RawBassSerreOrbitVertex G H} (p : Quiver.Path a b) (e : b ⟶ c) : coverFreeGroupoidPathHom G H (p.cons e) = CategoryTheory.CategoryStruct.comp (coverFreeGroupoidPathHom G H p) (match e with | Sum.inl f => (Quiver.FreeGroupoid.of (RawBassSerreOrbitVertex G H)).map f | Sum.inr f => CategoryTheory.Groupoid.inv ((Quiver.FreeGroupoid.of (RawBassSerreOrbitVertex G H)).map f))

noncomputable def GraphCoveringTheory.Kurosh.coverPathValueOpp {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (p : Quiver.Path a b) : (CoverSource G H)ᵐᵒᵖ

Evaluate a quotient path in the opposite covering group.

Equations

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

noncomputable def GraphCoveringTheory.Kurosh.coverPathValue {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (p : Quiver.Path a b) : CoverSource G H

The covering-group value obtained by evaluating a quotient path.

Equations

• One or more equations did not get rendered due to their size.
• GraphCoveringTheory.Kurosh.coverPathValue G H Quiver.Path.nil = 1

theorem GraphCoveringTheory.Kurosh.coverPathValueOpp_nil {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a : RawBassSerreOrbitVertex G H} : coverPathValueOpp G H Quiver.Path.nil = 1

theorem GraphCoveringTheory.Kurosh.coverPathValueOpp_pos {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (p : Quiver.Path (rawBassSerreOrbitRoot G H) a) (e : a ⟶ b) : coverPathValueOpp G H (p.cons e.toPos) = MulOpposite.op (coverEdgeLetter G H (coverBaseEdge G H e))⁻¹ * coverPathValueOpp G H p

theorem GraphCoveringTheory.Kurosh.coverPathValueOpp_neg {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (p : Quiver.Path (rawBassSerreOrbitRoot G H) b) (e : a ⟶ b) : coverPathValueOpp G H (p.cons e.toNeg) = MulOpposite.op (coverEdgeLetter G H (coverBaseEdge G H e)) * coverPathValueOpp G H p

theorem GraphCoveringTheory.Kurosh.coverPathValue_nil {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a : RawBassSerreOrbitVertex G H} : coverPathValue G H Quiver.Path.nil = 1

theorem GraphCoveringTheory.Kurosh.coverPathValue_pos {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (p : Quiver.Path (rawBassSerreOrbitRoot G H) a) (e : a ⟶ b) : coverPathValue G H (p.cons e.toPos) = coverPathValue G H p * (coverEdgeLetter G H (coverBaseEdge G H e))⁻¹

theorem GraphCoveringTheory.Kurosh.coverPathValue_neg {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (p : Quiver.Path (rawBassSerreOrbitRoot G H) b) (e : a ⟶ b) : coverPathValue G H (p.cons e.toNeg) = coverPathValue G H p * coverEdgeLetter G H (coverBaseEdge G H e)

noncomputable def GraphCoveringTheory.Kurosh.coverPathFreeLoop {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a : RawBassSerreOrbitVertex G H} (p : Quiver.Path (rawBassSerreOrbitRoot G H) a) : KuroshFreePart G H

The free-part loop determined by a path based at the quotient root.

Equations

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

theorem GraphCoveringTheory.Kurosh.coverQuotientTreePathHom_root {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : quotientTreePathHom G H (rawBassSerreOrbitRoot G H) = CategoryTheory.CategoryStruct.id ((Quiver.FreeGroupoid.of (RawBassSerreOrbitVertex G H)).obj (rawBassSerreOrbitRoot G H))

theorem GraphCoveringTheory.Kurosh.coverPathValue_formula {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a : RawBassSerreOrbitVertex G H} (p : Quiver.Path (rawBassSerreOrbitRoot G H) a) : coverPathValue G H p = ((treeKuroshFreeInclusion G H) (coverPathFreeLoop G H p))⁻¹

noncomputable def GraphCoveringTheory.Kurosh.coverPathLift {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (p : CoverSource G H) {a : RawBassSerreOrbitVertex G H} : Quiver.Path (rawBassSerreOrbitRoot G H) a → (q : CoverSource G H) × Quiver.Path (coverVertexMk G H (rawBassSerreOrbitRoot G H) p) (coverVertexMk G H a q)

Lift a quotient path starting from the coset of a given covering-group element.

Equations

• One or more equations did not get rendered due to their size.
• GraphCoveringTheory.Kurosh.coverPathLift G H p Quiver.Path.nil = ⟨p, Quiver.Path.nil⟩

theorem GraphCoveringTheory.Kurosh.coverPathLift_value {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (p : CoverSource G H) {a : RawBassSerreOrbitVertex G H} (q : Quiver.Path (rawBassSerreOrbitRoot G H) a) : (coverPathLift G H p q).fst = p * coverPathValue G H q

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

The projection from the auxiliary covering quiver to the Bass-Serre quiver.

Equations

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

theorem GraphCoveringTheory.Kurosh.treeKuroshVertexInclusion_injective {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (a : RawBassSerreOrbitVertex G H) : Function.Injective ⇑(treeKuroshVertexInclusion G H a)