The free-product data used by Kurosh's theorem

This file starts the Bass--Serre extension of the finite Schreier development. The ambient free product is Mathlib's Monoid.CoprodI; in particular, the reduced-word normal form is not redefined here. The definitions below keep the two pieces of Kurosh data explicit:

• the canonical copy of each factor in the free product; and
• the subgroup obtained by intersecting a conjugate of that copy with a subgroup of the ambient free product.

The main decomposition theorem will use these definitions rather than an unstructured existential statement. This makes the double-coset indexing, the factor embeddings, and the final free-product equivalence visible to the kernel checker and to the Palomar statement surface.

The orbit type is Mathlib's MulAction.orbitRel.Quotient. Proof scaffolding shared between this project's modules lives in GraphCoveringTheory.Kurosh.Internal.

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

@[instance_reducible]

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

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

Equations

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

@[reducible, inline]

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

The indexed free product of a family of groups.

Equations

• GraphCoveringTheory.Kurosh.FreeProduct G = Monoid.CoprodI G

def GraphCoveringTheory.Kurosh.factorInclusion {ι : Type u_1} (G : ι → Type u) [(i : ι) → Group (G i)] (i : ι) : G i →* FreeProduct G

The canonical inclusion of a factor into its free product.

Equations

• GraphCoveringTheory.Kurosh.factorInclusion G i = Monoid.CoprodI.of

@[simp]

theorem GraphCoveringTheory.Kurosh.factorInclusion_apply {ι : Type u_1} (G : ι → Type u) [(i : ι) → Group (G i)] (i : ι) (g : G i) : (factorInclusion G i) g = Monoid.CoprodI.of g

theorem GraphCoveringTheory.Kurosh.factorInclusion_injective {ι : Type u_1} (G : ι → Type u) [(i : ι) → Group (G i)] (i : ι) : Function.Injective ⇑(factorInclusion G i)

Conjugate intersections

The subgroup is deliberately defined inside the ambient group first. A later construction restricts it to the subgroup H, which gives the factors that appear literally in the Kurosh decomposition.

def GraphCoveringTheory.Kurosh.conjugateSubgroup {P : Type u} [Group P] (K : Subgroup P) (g : P) : Subgroup P

Conjugation of a subgroup by an ambient-group element.

Equations

• GraphCoveringTheory.Kurosh.conjugateSubgroup K g = Subgroup.map (↑(MulAut.conj g)) K

@[simp]

theorem GraphCoveringTheory.Kurosh.mem_conjugateSubgroup_iff {P : Type u} [Group P] (K : Subgroup P) (g x : P) : x ∈ conjugateSubgroup K g ↔ g⁻¹ * x * g ∈ K

def GraphCoveringTheory.Kurosh.intersectionFactor {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (i : ι) (g : FreeProduct G) : Subgroup (FreeProduct G)

The ambient subgroup obtained from a Kurosh factor.

Equations

• GraphCoveringTheory.Kurosh.intersectionFactor H i g = H ⊓ GraphCoveringTheory.Kurosh.conjugateSubgroup (GraphCoveringTheory.Kurosh.factorInclusion G i).range g

def GraphCoveringTheory.Kurosh.intersectionFactorInH {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (i : ι) (g : FreeProduct G) : Subgroup ↥H

The same factor regarded as a subgroup of H, so its inclusion into H is canonical.

Equations

• GraphCoveringTheory.Kurosh.intersectionFactorInH H i g = Subgroup.comap H.subtype (GraphCoveringTheory.Kurosh.intersectionFactor H i g)

theorem GraphCoveringTheory.Kurosh.intersectionFactorInH_coe_mem {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (i : ι) (g : FreeProduct G) (x : ↥(intersectionFactorInH H i g)) : ↑↑x ∈ intersectionFactor H i g

The double-coset indexing type

Mathlib's DoubleCoset.Quotient is exactly H \ G / K. Defining the factor index this way records the classical indexing without choosing representatives prematurely. Representatives are selected only when the decomposition construction needs them.

@[reducible, inline]

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

Double cosets of H and the image of the indexed free factor.

Equations

• GraphCoveringTheory.Kurosh.DoubleCosetIndex H i = DoubleCoset.Quotient ↑H ↑(GraphCoveringTheory.Kurosh.factorInclusion G i).range

noncomputable def GraphCoveringTheory.Kurosh.doubleCosetRepresentative {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (i : ι) (q : DoubleCosetIndex H i) : FreeProduct G

A chosen representative of a double coset.

Equations

• GraphCoveringTheory.Kurosh.doubleCosetRepresentative H i q = Quotient.out q

@[simp]

theorem GraphCoveringTheory.Kurosh.doubleCosetRepresentative_mk {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (i : ι) (g : FreeProduct G) : DoubleCoset.mk H (factorInclusion G i).range (doubleCosetRepresentative H i (DoubleCoset.mk H (factorInclusion G i).range g)) = DoubleCoset.mk H (factorInclusion G i).range g

theorem GraphCoveringTheory.Kurosh.doubleCosetIndex_eq_iff {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (i : ι) (g h : FreeProduct G) : DoubleCoset.mk H (factorInclusion G i).range g = DoubleCoset.mk H (factorInclusion G i).range h ↔ ∃ a ∈ H, ∃ b ∈ (factorInclusion G i).range, h = a * g * b

Right-coset normal forms

The Bass--Serre action is a left action on right cosets. The indexed coproduct API exposes the first syllable directly, so right-coset normal forms are obtained by applying the same operation to the inverse word. The small word reversal API here is useful independently of the later tree construction.

def GraphCoveringTheory.Kurosh.wordInv {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (w : Monoid.CoprodI.Word G) : Monoid.CoprodI.Word G

Invert a reduced word by reversing its letters and inverting each letter.

Equations

• GraphCoveringTheory.Kurosh.wordInv w = { toList := List.map (fun (x : (i : ι) × G i) => ⟨x.fst, x.snd⁻¹⟩) w.toList.reverse, ne_one := ⋯, chain_ne := ⋯ }

@[simp]

theorem GraphCoveringTheory.Kurosh.wordInv_toList {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (w : Monoid.CoprodI.Word G) : (wordInv w).toList = List.map (fun (x : (i : ι) × G i) => ⟨x.fst, x.snd⁻¹⟩) w.toList.reverse

theorem GraphCoveringTheory.Kurosh.wordInv_prod {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (w : Monoid.CoprodI.Word G) : (wordInv w).prod = w.prod⁻¹

@[simp]

theorem GraphCoveringTheory.Kurosh.wordInv_wordInv {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (w : Monoid.CoprodI.Word G) : wordInv (wordInv w) = w

def GraphCoveringTheory.Kurosh.wordLastIdx {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (w : Monoid.CoprodI.Word G) : Option ι

The factor index of the last letter, or none for the empty word.

Equations

• GraphCoveringTheory.Kurosh.wordLastIdx w = (GraphCoveringTheory.Kurosh.wordInv w).fstIdx

theorem GraphCoveringTheory.Kurosh.wordLastIdx_ne_iff {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (w : Monoid.CoprodI.Word G) (i : ι) : wordLastIdx w ≠ some i ↔ ∀ l ∈ w.toList.getLast?, i ≠ l.fst

Removing a rightmost syllable

This is the right-coset counterpart of Word.equivPair: the inverse word is split at its first syllable and then inverted again. It supplies the canonical representative of a right coset of a factor.

noncomputable def GraphCoveringTheory.Kurosh.rightTail {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (i : ι) (w : Monoid.CoprodI.Word G) : Monoid.CoprodI.Word G

Remove the terminal letter in factor i, if present.

Equations

• GraphCoveringTheory.Kurosh.rightTail i w = GraphCoveringTheory.Kurosh.wordInv ((Monoid.CoprodI.Word.equivPair i) (GraphCoveringTheory.Kurosh.wordInv w)).tail

noncomputable def GraphCoveringTheory.Kurosh.rightHead {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (i : ι) (w : Monoid.CoprodI.Word G) : G i

The terminal factor-i letter, or the identity if the word ends in another factor.

Equations

• GraphCoveringTheory.Kurosh.rightHead i w = ((Monoid.CoprodI.Word.equivPair i) (GraphCoveringTheory.Kurosh.wordInv w)).head⁻¹

theorem GraphCoveringTheory.Kurosh.rightTail_lastIdx_ne {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (i : ι) (w : Monoid.CoprodI.Word G) : wordLastIdx (rightTail i w) ≠ some i

@[reducible, inline]

abbrev GraphCoveringTheory.Kurosh.RightFactorWord {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (i : ι) : Type (max 0 u u_1)

Reduced words representing cosets g * Gᵢ, obtained by removing the terminal i-factor.

Equations

• GraphCoveringTheory.Kurosh.RightFactorWord i = { w : Monoid.CoprodI.Word G // GraphCoveringTheory.Kurosh.wordLastIdx w ≠ some i }

noncomputable def GraphCoveringTheory.Kurosh.rightTailCanonical {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (i : ι) (w : Monoid.CoprodI.Word G) : RightFactorWord i

The right tail bundled with the fact that its last index differs from i.

Equations

• GraphCoveringTheory.Kurosh.rightTailCanonical i w = ⟨GraphCoveringTheory.Kurosh.rightTail i w, ⋯⟩

theorem GraphCoveringTheory.Kurosh.rightTail_of_lastIdx_ne {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (i : ι) (w : Monoid.CoprodI.Word G) (hw : wordLastIdx w ≠ some i) : rightTail i w = w

theorem GraphCoveringTheory.Kurosh.equivPair_head_ne_one_of_fstIdx_eq {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (i : ι) (w : Monoid.CoprodI.Word G) (hwi : w.fstIdx = some i) : ((Monoid.CoprodI.Word.equivPair i) w).head ≠ 1

theorem GraphCoveringTheory.Kurosh.rightHead_ne_one_of_lastIdx_eq {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (i : ι) (w : Monoid.CoprodI.Word G) (hwi : wordLastIdx w = some i) : rightHead i w ≠ 1

theorem GraphCoveringTheory.Kurosh.right_syllable_decomposition {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (i : ι) (w : Monoid.CoprodI.Word G) : w.prod = (rightTail i w).prod * Monoid.CoprodI.of (rightHead i w)

noncomputable def GraphCoveringTheory.Kurosh.rightAppend {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (i : ι) (w : Monoid.CoprodI.Word G) (a : G i) (ha : a ≠ 1) (hw : wordLastIdx w ≠ some i) : Monoid.CoprodI.Word G

Append a nonidentity factor-i letter to a word ending in a different factor.

Equations

• GraphCoveringTheory.Kurosh.rightAppend i w a ha hw = GraphCoveringTheory.Kurosh.wordInv (Monoid.CoprodI.Word.cons a⁻¹ (GraphCoveringTheory.Kurosh.wordInv w) ⋯ ⋯)

theorem GraphCoveringTheory.Kurosh.wordInv_cons_rightAppend {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (i : ι) (a : G i) (w : Monoid.CoprodI.Word G) (hw : w.fstIdx ≠ some i) (ha : a ≠ 1) : rightAppend i (↑⟨wordInv w, ⋯⟩) a⁻¹ ⋯ ⋯ = wordInv (Monoid.CoprodI.Word.cons a w hw ha)

@[simp]

theorem GraphCoveringTheory.Kurosh.rightAppend_prod {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (i : ι) (w : Monoid.CoprodI.Word G) (a : G i) (ha : a ≠ 1) (hw : wordLastIdx w ≠ some i) : (rightAppend i w a ha hw).prod = w.prod * Monoid.CoprodI.of a

theorem GraphCoveringTheory.Kurosh.rightAppend_rightTail {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (i : ι) (w : Monoid.CoprodI.Word G) (a : G i) (ha : a ≠ 1) (hw : wordLastIdx w ≠ some i) : rightTail i (rightAppend i w a ha hw) = w

theorem GraphCoveringTheory.Kurosh.rightAppend_rightHead {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (i : ι) (w : Monoid.CoprodI.Word G) (a : G i) (ha : a ≠ 1) (hw : wordLastIdx w ≠ some i) : rightHead i (rightAppend i w a ha hw) = a

theorem GraphCoveringTheory.Kurosh.word_equiv_mul_rightAppend {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (i : ι) (w : RightFactorWord i) (a : G i) (ha : a ≠ 1) : Monoid.CoprodI.Word.equiv ((↑w).prod * Monoid.CoprodI.of a) = rightAppend i (↑w) a ha ⋯

theorem GraphCoveringTheory.Kurosh.rightTail_equiv_mul_factor {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (i : ι) (w : RightFactorWord i) (a : G i) : rightTail i (Monoid.CoprodI.Word.equiv ((↑w).prod * Monoid.CoprodI.of a)) = ↑w

theorem GraphCoveringTheory.Kurosh.rightTail_eq_of_prod_eq_mul_factor {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (i : ι) (w w' : RightFactorWord i) (a a' : G i) (h : (↑w).prod * Monoid.CoprodI.of a = (↑w').prod * Monoid.CoprodI.of a') : ↑w = ↑w'

noncomputable def GraphCoveringTheory.Kurosh.rightAppendCanonical {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (i : ι) (w : RightFactorWord i) (a : G i) (ha : a ≠ 1) : Monoid.CoprodI.Word G

Append a nonidentity letter to a canonical representative for its factor coset.

Equations

• GraphCoveringTheory.Kurosh.rightAppendCanonical i w a ha = GraphCoveringTheory.Kurosh.rightAppend i (↑w) a ha ⋯

theorem GraphCoveringTheory.Kurosh.rightAppendCanonical_of_lastIdx_eq {ι : Type u_1} {G : ι → Type u} [(i : ι) → Group (G i)] (i : ι) (w : Monoid.CoprodI.Word G) (hwi : wordLastIdx w = some i) : rightAppendCanonical i (rightTailCanonical i w) (rightHead i w) ⋯ = w

The explicit Bass--Serre tree

The central vertices are reduced words. A factor vertex records a reduced word which is already canonical on the right for one factor. The two edge families are the central-to-factor edge and the edge obtained by appending a nontrivial factor syllable. This is the usual normal-form model of the Bass--Serre tree of an indexed free product.

inductive GraphCoveringTheory.Kurosh.BassSerreVertex {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : Type (max u v)

The word model of Bass-Serre vertices: reduced words and canonical factor-coset words.

• central {ι : Type v} {G : ι → Type u} [(i : ι) → Group (G i)] (w : Monoid.CoprodI.Word G) : BassSerreVertex G
• factor {ι : Type v} {G : ι → Type u} [(i : ι) → Group (G i)] (i : ι) (w : RightFactorWord i) : BassSerreVertex G

inductive GraphCoveringTheory.Kurosh.BassSerreEdge {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : BassSerreVertex G → BassSerreVertex G → Type (max u v)

The directed edges of the word model, oriented away from the empty word.

• centralFactor {ι : Type v} {G : ι → Type u} [(i : ι) → Group (G i)] (w : Monoid.CoprodI.Word G) (i : ι) (hw : wordLastIdx w ≠ some i) : BassSerreEdge G (BassSerreVertex.central w) (BassSerreVertex.factor i ⟨w, hw⟩)
• factorCentral {ι : Type v} {G : ι → Type u} [(i : ι) → Group (G i)] (i : ι) (w : RightFactorWord i) (a : G i) (ha : a ≠ 1) : BassSerreEdge G (BassSerreVertex.factor i w) (BassSerreVertex.central (rightAppendCanonical i w a ha))

@[instance_reducible]

instance GraphCoveringTheory.Kurosh.bassSerreQuiver {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : Quiver (BassSerreVertex G)

Equations

• GraphCoveringTheory.Kurosh.bassSerreQuiver G = { Hom := GraphCoveringTheory.Kurosh.BassSerreEdge G }

theorem GraphCoveringTheory.Kurosh.bassSerreWord_path {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (w : Monoid.CoprodI.Word G) : Nonempty (Quiver.Path (BassSerreVertex.central Monoid.CoprodI.Word.empty) (BassSerreVertex.central w))

theorem GraphCoveringTheory.Kurosh.bassSerreFactor_path {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (i : ι) (w : RightFactorWord i) : Nonempty (Quiver.Path (BassSerreVertex.central Monoid.CoprodI.Word.empty) (BassSerreVertex.factor i w))

theorem GraphCoveringTheory.Kurosh.bassSerre_rootedConnected {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : Quiver.RootedConnected (have this := BassSerreVertex.central Monoid.CoprodI.Word.empty; this)

noncomputable def GraphCoveringTheory.Kurosh.bassSerreTree {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : WideSubquiver (Quiver.Symmetrify (BassSerreVertex G))

A geodesic spanning tree of the symmetrified word model.

Equations

• GraphCoveringTheory.Kurosh.bassSerreTree G = Quiver.geodesicSubtree (GraphCoveringTheory.Kurosh.BassSerreVertex.central Monoid.CoprodI.Word.empty)

@[instance_reducible]

noncomputable instance GraphCoveringTheory.Kurosh.bassSerreTreeArborescence {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (BassSerreVertex G)) (bassSerreTree G))

Equations

• GraphCoveringTheory.Kurosh.bassSerreTreeArborescence G = Quiver.geodesicArborescence (GraphCoveringTheory.Kurosh.BassSerreVertex.central Monoid.CoprodI.Word.empty)

Right cosets and the natural action

The canonical-word vertices above are convenient for connectivity proofs. For the group action it is cleaner to use the quotient of a group by right multiplication by a subgroup. The quotient is kept elementary here so that the stabilizer calculation does not depend on a choice of representatives.

def GraphCoveringTheory.Kurosh.rightCosetSetoid {P : Type w} [Group P] (K : Subgroup P) : Setoid P

Equivalence under multiplication on the right by an element of K.

Equations

• GraphCoveringTheory.Kurosh.rightCosetSetoid K = { r := fun (a b : P) => ∃ (k : ↥K), a * ↑k = b, iseqv := ⋯ }

@[reducible, inline]

abbrev GraphCoveringTheory.Kurosh.RightCoset {P : Type w} [Group P] (K : Subgroup P) : Type w

Cosets represented by a * K, using the right-multiplication equivalence relation.

Equations

• GraphCoveringTheory.Kurosh.RightCoset K = Quotient (GraphCoveringTheory.Kurosh.rightCosetSetoid K)

def GraphCoveringTheory.Kurosh.rightCosetMk {P : Type w} [Group P] (K : Subgroup P) (a : P) : RightCoset K

The coset represented by a group element.

Equations

• GraphCoveringTheory.Kurosh.rightCosetMk K a = ⟦a⟧

theorem GraphCoveringTheory.Kurosh.rightCosetMk_eq_iff {P : Type w} [Group P] (K : Subgroup P) (a b : P) : rightCosetMk K a = rightCosetMk K b ↔ ∃ (k : ↥K), a * ↑k = b

@[instance_reducible]

instance GraphCoveringTheory.Kurosh.rightCosetMulAction {P : Type w} [Group P] (K : Subgroup P) : MulAction P (RightCoset K)

Equations

• GraphCoveringTheory.Kurosh.rightCosetMulAction K = { smul := fun (g : P) => Quotient.lift (fun (a : P) => GraphCoveringTheory.Kurosh.rightCosetMk K (g * a)) ⋯, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem GraphCoveringTheory.Kurosh.rightCosetMk_smul {P : Type w} [Group P] (K : Subgroup P) (g a : P) : g • rightCosetMk K a = rightCosetMk K (g * a)

theorem GraphCoveringTheory.Kurosh.rightCoset_stabilizer_iff {P : Type w} [Group P] (K : Subgroup P) (g a : P) : g • rightCosetMk K a = rightCosetMk K a ↔ a⁻¹ * g * a ∈ K

@[reducible, inline]

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

Cosets of the image of a free factor in the ambient free product.

Equations

• GraphCoveringTheory.Kurosh.FactorCoset G i = GraphCoveringTheory.Kurosh.RightCoset (GraphCoveringTheory.Kurosh.factorInclusion G i).range

def GraphCoveringTheory.Kurosh.factorCosetMk {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (i : ι) (g : FreeProduct G) : FactorCoset G i

The factor coset represented by an element of the free product.

Equations

• GraphCoveringTheory.Kurosh.factorCosetMk G i g = GraphCoveringTheory.Kurosh.rightCosetMk (GraphCoveringTheory.Kurosh.factorInclusion G i).range g

theorem GraphCoveringTheory.Kurosh.factorCoset_mul_factor {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (i : ι) (g : FreeProduct G) (a : G i) : factorCosetMk G i (g * Monoid.CoprodI.of a) = factorCosetMk G i g

inductive GraphCoveringTheory.Kurosh.RawBassSerreVertex {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : Type (max u v)

Bass-Serre vertices represented by group elements and factor cosets.

• central {ι : Type v} {G : ι → Type u} [(i : ι) → Group (G i)] (g : FreeProduct G) : RawBassSerreVertex G
• factor {ι : Type v} {G : ι → Type u} [(i : ι) → Group (G i)] (i : ι) (c : FactorCoset G i) : RawBassSerreVertex G

inductive GraphCoveringTheory.Kurosh.RawBassSerreEdge {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : RawBassSerreVertex G → RawBassSerreVertex G → Type (max u v)

An edge joins an ambient group element to its coset in a free factor.

• centralFactor {ι : Type v} {G : ι → Type u} [(i : ι) → Group (G i)] (g : FreeProduct G) (i : ι) : RawBassSerreEdge G (RawBassSerreVertex.central g) (RawBassSerreVertex.factor i (factorCosetMk G i g))

@[instance_reducible]

instance GraphCoveringTheory.Kurosh.rawBassSerreQuiver {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : Quiver (RawBassSerreVertex G)

Equations

• GraphCoveringTheory.Kurosh.rawBassSerreQuiver G = { Hom := GraphCoveringTheory.Kurosh.RawBassSerreEdge G }

theorem GraphCoveringTheory.Kurosh.rawBassSerreWord_path {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (g : FreeProduct G) : Nonempty (Quiver.Path (RawBassSerreVertex.central 1) (RawBassSerreVertex.central g))

theorem GraphCoveringTheory.Kurosh.rawBassSerreFactor_path {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (i : ι) (c : FactorCoset G i) : Nonempty (Quiver.Path (RawBassSerreVertex.central 1) (RawBassSerreVertex.factor i c))

theorem GraphCoveringTheory.Kurosh.rawBassSerre_rootedConnected {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : Quiver.RootedConnected (have this := RawBassSerreVertex.central 1; this)

noncomputable def GraphCoveringTheory.Kurosh.rawBassSerreTree {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : WideSubquiver (Quiver.Symmetrify (RawBassSerreVertex G))

A geodesic spanning tree of the symmetrified group-and-coset model.

Equations

• GraphCoveringTheory.Kurosh.rawBassSerreTree G = Quiver.geodesicSubtree (GraphCoveringTheory.Kurosh.RawBassSerreVertex.central 1)

@[instance_reducible]

noncomputable instance GraphCoveringTheory.Kurosh.rawBassSerreTreeArborescence {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (RawBassSerreVertex G)) (rawBassSerreTree G))

Equations

• GraphCoveringTheory.Kurosh.rawBassSerreTreeArborescence G = Quiver.geodesicArborescence (GraphCoveringTheory.Kurosh.RawBassSerreVertex.central 1)

@[instance_reducible]

instance GraphCoveringTheory.Kurosh.rawBassSerreVertexMulAction {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : MulAction (FreeProduct G) (RawBassSerreVertex G)

Equations

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

theorem GraphCoveringTheory.Kurosh.rawBassSerre_factor_fixed_iff {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (i : ι) (g : FreeProduct G) (h : ↥H) : ↑h • RawBassSerreVertex.factor i (factorCosetMk G i g) = RawBassSerreVertex.factor i (factorCosetMk G i g) ↔ ↑h ∈ intersectionFactor H i g

theorem GraphCoveringTheory.Kurosh.rawBassSerre_factor_orbit_iff {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (i : ι) (g h : FreeProduct G) : (∃ (k : ↥H), ↑k • RawBassSerreVertex.factor i (factorCosetMk G i g) = RawBassSerreVertex.factor i (factorCosetMk G i h)) ↔ DoubleCoset.mk H (factorInclusion G i).range g = DoubleCoset.mk H (factorInclusion G i).range h

@[reducible, inline]

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

Pairs of a free-factor index and a corresponding double coset.

Equations

• GraphCoveringTheory.Kurosh.KuroshFactorIndex G H = ((i : ι) × GraphCoveringTheory.Kurosh.DoubleCosetIndex H i)

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

The chosen ambient group element for an indexed double coset.

Equations

• GraphCoveringTheory.Kurosh.kuroshFactorRepresentative G H q = GraphCoveringTheory.Kurosh.doubleCosetRepresentative H q.fst q.snd

noncomputable def GraphCoveringTheory.Kurosh.kuroshFactorSubgroup {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (q : KuroshFactorIndex G H) : Subgroup ↥H

The intersection with a conjugate free factor, regarded as a subgroup of H.

Equations

• GraphCoveringTheory.Kurosh.kuroshFactorSubgroup G H q = GraphCoveringTheory.Kurosh.intersectionFactorInH H q.fst (GraphCoveringTheory.Kurosh.kuroshFactorRepresentative G H q)

theorem GraphCoveringTheory.Kurosh.rawBassSerre_central_fixed_iff {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (g h : FreeProduct G) : h • RawBassSerreVertex.central g = RawBassSerreVertex.central g ↔ h = 1

A central Bass–Serre vertex has trivial stabilizer.

theorem GraphCoveringTheory.Kurosh.kurosh_factor_subgroup_is_stabilizer {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (q : KuroshFactorIndex G H) (h : ↥H) : h ∈ kuroshFactorSubgroup G H q ↔ ↑h • RawBassSerreVertex.factor q.fst (factorCosetMk G q.fst (kuroshFactorRepresentative G H q)) = RawBassSerreVertex.factor q.fst (factorCosetMk G q.fst (kuroshFactorRepresentative G H q))

The quotient graph seen by the subgroup

The raw tree is the universal Bass--Serre tree. The next layer records the quotient graph without choosing representatives of its vertices or edges. This is the graph on which the free part of the Kurosh decomposition is the fundamental-group contribution; the factor vertices retain the stabilizers defined above.

@[reducible, inline]

abbrev GraphCoveringTheory.Kurosh.ActionOrbit (A X : Type w) [Group A] [MulAction A X] : Type w

The standard Mathlib quotient of an action by its orbit relation.

Equations

• GraphCoveringTheory.Kurosh.ActionOrbit A X = MulAction.orbitRel.Quotient A X

def GraphCoveringTheory.Kurosh.actionOrbitMk (A X : Type w) [Group A] [MulAction A X] (x : X) : ActionOrbit A X

Send a point to its group-action orbit.

Equations

• GraphCoveringTheory.Kurosh.actionOrbitMk A X x = ⟦x⟧

@[simp]

theorem GraphCoveringTheory.Kurosh.actionOrbitMk_eq_iff (A X : Type w) [Group A] [MulAction A X] (x y : X) : actionOrbitMk A X x = actionOrbitMk A X y ↔ ∃ (a : A), a • x = y

Orbit equality expressed by an element carrying the first point to the second. Mathlib's orbit relation uses the reverse orientation.

theorem GraphCoveringTheory.Kurosh.actionOrbitMk_smul (A X : Type w) [Group A] [MulAction A X] (a : A) (x : X) : actionOrbitMk A X (a • x) = actionOrbitMk A X x

def GraphCoveringTheory.Kurosh.rawBassSerreEdgeData {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : Type (max (max v u) v)

An unbundled Bass-Serre edge is a group element paired with a factor index.

Equations

• GraphCoveringTheory.Kurosh.rawBassSerreEdgeData G = (GraphCoveringTheory.Kurosh.FreeProduct G × ι)

def GraphCoveringTheory.Kurosh.rawBassSerreEdgeDataSource {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (e : rawBassSerreEdgeData G) : RawBassSerreVertex G

The central vertex at the source of an unbundled edge.

Equations

• GraphCoveringTheory.Kurosh.rawBassSerreEdgeDataSource G e = GraphCoveringTheory.Kurosh.RawBassSerreVertex.central e.1

def GraphCoveringTheory.Kurosh.rawBassSerreEdgeDataTarget {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (e : rawBassSerreEdgeData G) : RawBassSerreVertex G

The factor coset at the target of an unbundled edge.

Equations

• GraphCoveringTheory.Kurosh.rawBassSerreEdgeDataTarget G e = GraphCoveringTheory.Kurosh.RawBassSerreVertex.factor e.2 (GraphCoveringTheory.Kurosh.factorCosetMk G e.2 e.1)

def GraphCoveringTheory.Kurosh.rawBassSerreEdgeDataAction {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (a : FreeProduct G) (e : rawBassSerreEdgeData G) : rawBassSerreEdgeData G

Translate an unbundled edge by left multiplication on its group coordinate.

Equations

• GraphCoveringTheory.Kurosh.rawBassSerreEdgeDataAction G a e = (a * e.1, e.2)

@[instance_reducible]

instance GraphCoveringTheory.Kurosh.rawBassSerreEdgeDataMulAction {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : MulAction (FreeProduct G) (rawBassSerreEdgeData G)

Equations

• GraphCoveringTheory.Kurosh.rawBassSerreEdgeDataMulAction G = { smul := GraphCoveringTheory.Kurosh.rawBassSerreEdgeDataAction G, mul_smul := ⋯, one_smul := ⋯ }

theorem GraphCoveringTheory.Kurosh.rawBassSerreEdgeData_source_action {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (a : FreeProduct G) (e : rawBassSerreEdgeData G) : rawBassSerreEdgeDataSource G (a • e) = a • rawBassSerreEdgeDataSource G e

theorem GraphCoveringTheory.Kurosh.rawBassSerreEdgeData_target_action {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (a : FreeProduct G) (e : rawBassSerreEdgeData G) : rawBassSerreEdgeDataTarget G (a • e) = a • rawBassSerreEdgeDataTarget G e

@[instance_reducible]

instance GraphCoveringTheory.Kurosh.rawBassSerreVertexSubgroupMulAction {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : MulAction (↥H) (RawBassSerreVertex G)

Equations

• GraphCoveringTheory.Kurosh.rawBassSerreVertexSubgroupMulAction G H = { smul := fun (h : ↥H) (x : GraphCoveringTheory.Kurosh.RawBassSerreVertex G) => ↑h • x, mul_smul := ⋯, one_smul := ⋯ }

@[instance_reducible]

instance GraphCoveringTheory.Kurosh.rawBassSerreEdgeDataSubgroupMulAction {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : MulAction (↥H) (rawBassSerreEdgeData G)

Equations

• GraphCoveringTheory.Kurosh.rawBassSerreEdgeDataSubgroupMulAction G H = { smul := fun (h : ↥H) (e : GraphCoveringTheory.Kurosh.rawBassSerreEdgeData G) => ↑h • e, mul_smul := ⋯, one_smul := ⋯ }

def GraphCoveringTheory.Kurosh.rawBassSerreEdgeDataOf {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {a b : RawBassSerreVertex G} (e : a ⟶ b) : rawBassSerreEdgeData G

Forget the endpoints of a bundled Bass-Serre edge.

Equations

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

theorem GraphCoveringTheory.Kurosh.rawBassSerreEdgeDataOf_source {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {a b : RawBassSerreVertex G} (e : a ⟶ b) : rawBassSerreEdgeDataSource G (rawBassSerreEdgeDataOf G e) = a

theorem GraphCoveringTheory.Kurosh.rawBassSerreEdgeDataOf_target {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {a b : RawBassSerreVertex G} (e : a ⟶ b) : rawBassSerreEdgeDataTarget G (rawBassSerreEdgeDataOf G e) = b

def GraphCoveringTheory.Kurosh.rawBassSerreEdgeAction {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (g : FreeProduct G) {a b : RawBassSerreVertex G} (e : a ⟶ b) : g • a ⟶ g • b

Translate a Bass-Serre edge and both endpoints by a group element.

Equations

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

def GraphCoveringTheory.Kurosh.rawBassSerreSymmEdgeAction {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (g : FreeProduct G) {a b : RawBassSerreVertex G} (e : a ⟶ b) : g • a ⟶ g • b

Translate either orientation of a Bass-Serre edge.

Equations

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

def GraphCoveringTheory.Kurosh.rawBassSerrePathAction {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (g : FreeProduct G) {a b : RawBassSerreVertex G} : Quiver.Path a b → Quiver.Path (g • a) (g • b)

Translate every edge and endpoint of a symmetrified Bass-Serre path.

Equations

• GraphCoveringTheory.Kurosh.rawBassSerrePathAction G g Quiver.Path.nil = Quiver.Path.nil
• GraphCoveringTheory.Kurosh.rawBassSerrePathAction G g (p.cons e) = (GraphCoveringTheory.Kurosh.rawBassSerrePathAction G g p).cons (GraphCoveringTheory.Kurosh.rawBassSerreSymmEdgeAction G g e)

@[reducible, inline]

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

Vertex orbits for the action of the subgroup H on the Bass-Serre graph.

Equations

• GraphCoveringTheory.Kurosh.RawBassSerreOrbitVertex G H = GraphCoveringTheory.Kurosh.ActionOrbit (↥H) (GraphCoveringTheory.Kurosh.RawBassSerreVertex G)

@[reducible, inline]

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

Edge orbits for the action of the subgroup H on the Bass-Serre graph.

Equations

• GraphCoveringTheory.Kurosh.RawBassSerreOrbitEdge G H = GraphCoveringTheory.Kurosh.ActionOrbit (↥H) (GraphCoveringTheory.Kurosh.rawBassSerreEdgeData G)

noncomputable def GraphCoveringTheory.Kurosh.kuroshFactorOrbitVertex {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (q : KuroshFactorIndex G H) : RawBassSerreOrbitVertex G H

The factor vertex in the quotient graph represented by a Kurosh index.

Equations

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

theorem GraphCoveringTheory.Kurosh.kuroshFactorOrbitVertex_eq_iff {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (q r : KuroshFactorIndex G H) : kuroshFactorOrbitVertex G H q = kuroshFactorOrbitVertex G H r ↔ q = r

def GraphCoveringTheory.Kurosh.rawBassSerreOrbitEdgeSource {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (e : RawBassSerreOrbitEdge G H) : RawBassSerreOrbitVertex G H

The source vertex orbit of an edge orbit.

Equations

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

def GraphCoveringTheory.Kurosh.rawBassSerreOrbitEdgeTarget {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (e : RawBassSerreOrbitEdge G H) : RawBassSerreOrbitVertex G H

The target vertex orbit of an edge orbit.

Equations

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

@[reducible]

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

The quotient quiver whose edges are subgroup orbits with prescribed endpoints.

Equations

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

@[instance_reducible]

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

Equations

• GraphCoveringTheory.Kurosh.rawBassSerreOrbitQuiver.inst G H = GraphCoveringTheory.Kurosh.rawBassSerreOrbitQuiver G H

def GraphCoveringTheory.Kurosh.rawBassSerreOrbitEdgeMk {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (e : rawBassSerreEdgeData G) : RawBassSerreOrbitEdge G H

The subgroup orbit of an unbundled Bass-Serre edge.

Equations

• GraphCoveringTheory.Kurosh.rawBassSerreOrbitEdgeMk G H e = GraphCoveringTheory.Kurosh.actionOrbitMk (↥H) (GraphCoveringTheory.Kurosh.rawBassSerreEdgeData G) e

def GraphCoveringTheory.Kurosh.rawBassSerreOrbitQuiverEdge {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (e : rawBassSerreEdgeData G) : rawBassSerreOrbitEdgeSource G H (rawBassSerreOrbitEdgeMk G H e) ⟶ rawBassSerreOrbitEdgeTarget G H (rawBassSerreOrbitEdgeMk G H e)

Bundle an edge orbit with its source and target vertex orbits.

Equations

• GraphCoveringTheory.Kurosh.rawBassSerreOrbitQuiverEdge G H e = ⟨GraphCoveringTheory.Kurosh.rawBassSerreOrbitEdgeMk G H e, ⋯⟩

theorem GraphCoveringTheory.Kurosh.rawBassSerreOrbitEdgeSource_mk {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (e : rawBassSerreEdgeData G) : rawBassSerreOrbitEdgeSource G H (rawBassSerreOrbitEdgeMk G H e) = actionOrbitMk (↥H) (RawBassSerreVertex G) (rawBassSerreEdgeDataSource G e)

theorem GraphCoveringTheory.Kurosh.rawBassSerreOrbitEdgeTarget_mk {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (e : rawBassSerreEdgeData G) : rawBassSerreOrbitEdgeTarget G H (rawBassSerreOrbitEdgeMk G H e) = actionOrbitMk (↥H) (RawBassSerreVertex G) (rawBassSerreEdgeDataTarget G e)

def GraphCoveringTheory.Kurosh.rawBassSerreOrbitEdgeMap {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreVertex G} (e : a ⟶ b) : actionOrbitMk (↥H) (RawBassSerreVertex G) a ⟶ actionOrbitMk (↥H) (RawBassSerreVertex G) b

Project a Bass-Serre edge to the quotient quiver.

Equations

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

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

The projection from the Bass-Serre quiver to its subgroup-orbit quiver.

Equations

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

def GraphCoveringTheory.Kurosh.rawBassSerreOrbitPrefunctorToSymm {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : RawBassSerreVertex G ⥤q Quiver.Symmetrify (RawBassSerreOrbitVertex G H)

The orbit projection with values in the symmetrified quotient quiver.

Equations

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

def GraphCoveringTheory.Kurosh.rawBassSerreOrbitSymmPrefunctor {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : Quiver.Symmetrify (RawBassSerreVertex G) ⥤q Quiver.Symmetrify (RawBassSerreOrbitVertex G H)

Extend the orbit projection to both edge orientations.

Equations

• GraphCoveringTheory.Kurosh.rawBassSerreOrbitSymmPrefunctor G H = Quiver.Symmetrify.lift (GraphCoveringTheory.Kurosh.rawBassSerreOrbitPrefunctorToSymm G H)

theorem GraphCoveringTheory.Kurosh.rawBassSerreOrbitQuiver_rootedConnected {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : Quiver.RootedConnected (have this := actionOrbitMk (↥H) (RawBassSerreVertex G) (RawBassSerreVertex.central 1); this)

noncomputable def GraphCoveringTheory.Kurosh.rawBassSerreOrbitTree {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : WideSubquiver (Quiver.Symmetrify (RawBassSerreOrbitVertex G H))

A geodesic spanning tree of the symmetrified quotient graph.

Equations

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

@[instance_reducible]

noncomputable instance GraphCoveringTheory.Kurosh.rawBassSerreOrbitTreeArborescence {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (RawBassSerreOrbitVertex G H)) (rawBassSerreOrbitTree G H))

Equations

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

@[instance_reducible]

noncomputable def GraphCoveringTheory.Kurosh.rawTreeUniquePath {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (b : WideSubquiver.toType (Quiver.Symmetrify (RawBassSerreOrbitVertex G H)) (rawBassSerreOrbitTree G H)) : Unique (Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (RawBassSerreOrbitVertex G H)) (rawBassSerreOrbitTree G H))) b)

The unique path from the chosen root to a vertex of the quotient spanning tree.

Equations

• GraphCoveringTheory.Kurosh.rawTreeUniquePath G H b = Quiver.Arborescence.uniquePath b

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

The subgroup orbit of the central vertex represented by the identity.

Equations

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

noncomputable def GraphCoveringTheory.Kurosh.rawOrbitAlign {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {x y : RawBassSerreVertex G} (h : actionOrbitMk (↥H) (RawBassSerreVertex G) x = actionOrbitMk (↥H) (RawBassSerreVertex G) y) : ↥H

Choose an element of H carrying one representative of an orbit to another.

Equations

• GraphCoveringTheory.Kurosh.rawOrbitAlign G H h = Classical.choose ⋯

theorem GraphCoveringTheory.Kurosh.rawOrbitAlign_spec {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {x y : RawBassSerreVertex G} (h : actionOrbitMk (↥H) (RawBassSerreVertex G) x = actionOrbitMk (↥H) (RawBassSerreVertex G) y) : ↑(rawOrbitAlign G H h) • x = y

def GraphCoveringTheory.Kurosh.wideSubquiverInclusion {V : Type u} [Quiver V] (W : WideSubquiver V) : WideSubquiver.toType V W ⥤q V

The prefunctor forgetting membership in a wide subquiver.

Equations

• GraphCoveringTheory.Kurosh.wideSubquiverInclusion W = { obj := id, map := fun {X Y : WideSubquiver.toType V W} (e : X ⟶ Y) => ↑e }

def GraphCoveringTheory.Kurosh.rawTreeInclusion {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : WideSubquiver.toType (Quiver.Symmetrify (RawBassSerreOrbitVertex G H)) (rawBassSerreOrbitTree G H) ⥤q Quiver.Symmetrify (RawBassSerreOrbitVertex G H)

Include the quotient spanning tree into the symmetrified quotient graph.

Equations

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

def GraphCoveringTheory.Kurosh.rawTreeEdgeMap {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : WideSubquiver.toType (Quiver.Symmetrify (RawBassSerreOrbitVertex G H)) (rawBassSerreOrbitTree G H)} (e : a ⟶ b) : (have this := a; this) ⟶ have this := b; this

Forget a quotient-tree edge's membership proof.

Equations

• GraphCoveringTheory.Kurosh.rawTreeEdgeMap G H e = (GraphCoveringTheory.Kurosh.rawTreeInclusion G H).map e

@[reducible]

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

The quotient spanning tree expressed as a quiver on the ambient vertex type.

Equations

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

@[instance_reducible]

noncomputable instance GraphCoveringTheory.Kurosh.rawTreeQuiverArborescence {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : Quiver.Arborescence (RawBassSerreOrbitVertex G H)

Equations

• GraphCoveringTheory.Kurosh.rawTreeQuiverArborescence G H = id (GraphCoveringTheory.Kurosh.rawBassSerreOrbitTreeArborescence G H)

@[irreducible]

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

Forget tree-membership proofs along a path in the quotient spanning tree.

Equations

• GraphCoveringTheory.Kurosh.rawTreePathMap G H Quiver.Path.nil = Quiver.Path.nil
• GraphCoveringTheory.Kurosh.rawTreePathMap G H (p.cons e) = (GraphCoveringTheory.Kurosh.rawTreePathMap G H p).cons ↑e

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

The root of the quotient spanning tree on the ambient vertex type.

Equations

• GraphCoveringTheory.Kurosh.rawTreeQuiverRoot G H = Quiver.Arborescence.root

theorem GraphCoveringTheory.Kurosh.rawTreeQuiverRoot_eq {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : rawTreeQuiverRoot G H = rawBassSerreOrbitRoot G H

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

The unique rooted tree path to a quotient vertex.

Equations

• GraphCoveringTheory.Kurosh.rawTreePath G H a = default

theorem GraphCoveringTheory.Kurosh.rawTreePathMap_cons_raw {ι : 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) : rawTreePathMap G H (p.cons e) = (rawTreePathMap G H p).cons (have this := ↑e; this)

noncomputable def GraphCoveringTheory.Kurosh.rawTreeLiftPath {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {b : RawBassSerreOrbitVertex G H} (_p : Quiver.Path (rawBassSerreOrbitRoot G H) b) : { x : RawBassSerreVertex G // actionOrbitMk (↥H) (RawBassSerreVertex G) x = b }

Choose a representative of a path endpoint by successively lifting quotient edges.

Equations

• One or more equations did not get rendered due to their size.
• GraphCoveringTheory.Kurosh.rawTreeLiftPath G H Quiver.Path.nil = ⟨GraphCoveringTheory.Kurosh.RawBassSerreVertex.central 1, ⋯⟩

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

The orbit representative obtained by lifting the chosen rooted tree path.

Equations

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

theorem GraphCoveringTheory.Kurosh.rawTreeRepresentative_orbit {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (b : RawBassSerreOrbitVertex G H) : actionOrbitMk (↥H) (RawBassSerreVertex G) (rawTreeRepresentative G H b) = b

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

Choose an unbundled representative of an edge in the quotient graph.

Equations

• GraphCoveringTheory.Kurosh.quotientEdgeRawData G H e = Quotient.out ↑e

theorem GraphCoveringTheory.Kurosh.quotientEdgeRawData_mk {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (e : a ⟶ b) : rawBassSerreOrbitEdgeMk G H (quotientEdgeRawData G H e) = ↑e

theorem GraphCoveringTheory.Kurosh.quotientEdgeSource_orbit {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (e : a ⟶ b) : actionOrbitMk (↥H) (RawBassSerreVertex G) (rawBassSerreEdgeDataSource G (quotientEdgeRawData G H e)) = a

theorem GraphCoveringTheory.Kurosh.quotientEdgeTarget_orbit {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (e : a ⟶ b) : actionOrbitMk (↥H) (RawBassSerreVertex G) (rawBassSerreEdgeDataTarget G (quotientEdgeRawData G H e)) = b

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

Align an edge representative's source with the chosen orbit representative.

Equations

• GraphCoveringTheory.Kurosh.quotientEdgeSourceAlign G H e = GraphCoveringTheory.Kurosh.rawOrbitAlign G H ⋯

theorem GraphCoveringTheory.Kurosh.quotientEdgeSourceAlign_spec {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (e : a ⟶ b) : ↑(quotientEdgeSourceAlign G H e) • rawBassSerreEdgeDataSource G (quotientEdgeRawData G H e) = rawTreeRepresentative G H a

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

The target after translating an edge to align its source.

Equations

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

theorem GraphCoveringTheory.Kurosh.quotientEdgeAlignedTarget_orbit {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (e : a ⟶ b) : actionOrbitMk (↥H) (RawBassSerreVertex G) (quotientEdgeAlignedTarget G H e) = b

theorem GraphCoveringTheory.Kurosh.rawTreeRepresentative_of_tree_edge {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (e : a ⟶ b) (he : e.toPos ∈ rawBassSerreOrbitTree G H a b) : rawTreeRepresentative G H b = quotientEdgeAlignedTarget G H e

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

Align the source-adjusted target with its chosen orbit representative.

Equations

• GraphCoveringTheory.Kurosh.quotientEdgeTargetAlign G H e = GraphCoveringTheory.Kurosh.rawOrbitAlign G H ⋯

theorem GraphCoveringTheory.Kurosh.quotientEdgeTargetAlign_spec {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (e : a ⟶ b) : ↑(quotientEdgeTargetAlign G H e) • quotientEdgeAlignedTarget G H e = rawTreeRepresentative G H b

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

Align the raw target directly with its chosen orbit representative.

Equations

• GraphCoveringTheory.Kurosh.quotientEdgeDirectTargetAlign G H e = GraphCoveringTheory.Kurosh.rawOrbitAlign G H ⋯

theorem GraphCoveringTheory.Kurosh.quotientEdgeDirectTargetAlign_spec {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (e : a ⟶ b) : ↑(quotientEdgeDirectTargetAlign G H e) • rawBassSerreEdgeDataTarget G (quotientEdgeRawData G H e) = rawTreeRepresentative G H b

theorem GraphCoveringTheory.Kurosh.rawTreeRepresentative_of_tree_edge_neg {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (e : a ⟶ b) (he : e.toNeg ∈ rawBassSerreOrbitTree G H b a) : rawTreeRepresentative G H a = ↑(quotientEdgeDirectTargetAlign G H e) • rawBassSerreEdgeDataSource G (quotientEdgeRawData G H e)

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

The subgroup label of a quotient edge, normalized to the identity on tree edges.

Equations

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

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

Choose a source alignment compatible with the normalized edge label.

Equations

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

theorem GraphCoveringTheory.Kurosh.quotientEdgeCoherentSourceAlign_spec {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (e : a ⟶ b) : ↑(quotientEdgeCoherentSourceAlign G H e) • rawBassSerreEdgeDataSource G (quotientEdgeRawData G H e) = rawTreeRepresentative G H a

theorem GraphCoveringTheory.Kurosh.quotientEdgeLabel_transport_coherent {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (e : a ⟶ b) : ↑(quotientEdgeLabel G H e) • ↑(quotientEdgeCoherentSourceAlign G H e) • rawBassSerreEdgeDataTarget G (quotientEdgeRawData G H e) = rawTreeRepresentative G H b

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

Label quotient edges by subgroup elements in the one-object groupoid.

Equations

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

def GraphCoveringTheory.Kurosh.freeGroupoidPathHom {V : Type u} [q : Quiver V] {a b : V} : Quiver.Path a b → ((Quiver.FreeGroupoid.of V).obj a ⟶ (Quiver.FreeGroupoid.of V).obj b)

Interpret a symmetric quiver path as a morphism in its free groupoid.

Equations

• One or more equations did not get rendered due to their size.
• GraphCoveringTheory.Kurosh.freeGroupoidPathHom Quiver.Path.nil = CategoryTheory.CategoryStruct.id ((Quiver.FreeGroupoid.of V).obj a)
• GraphCoveringTheory.Kurosh.freeGroupoidPathHom (p.cons (Sum.inl f)) = CategoryTheory.CategoryStruct.comp (GraphCoveringTheory.Kurosh.freeGroupoidPathHom p) ((Quiver.FreeGroupoid.of V).map f)

theorem GraphCoveringTheory.Kurosh.freeGroupoidPathHom_nil_public {V : Type u} [q : Quiver V] {a : V} : freeGroupoidPathHom Quiver.Path.nil = CategoryTheory.CategoryStruct.id ((Quiver.FreeGroupoid.of V).obj a)

def GraphCoveringTheory.Kurosh.freeGroupoidBaseObj {V : Type u} [q : Quiver V] (a : Quiver.FreeGroupoid V) : V

Recover the original vertex from an object of the free groupoid.

Equations

• GraphCoveringTheory.Kurosh.freeGroupoidBaseObj a = a.as

@[instance_reducible]

def GraphCoveringTheory.Kurosh.freeGroupoidCategoryQuiver {V : Type u} [q : Quiver V] : Quiver (Quiver.FreeGroupoid V)

The quiver underlying the category structure of the free groupoid.

Equations

• GraphCoveringTheory.Kurosh.freeGroupoidCategoryQuiver = inferInstance

@[instance_reducible]

def GraphCoveringTheory.Kurosh.freeGroupoidGeneratorQuiver {V : Type u} [q : Quiver V] : Quiver (Quiver.FreeGroupoid V)

Original quiver arrows, lifted to the universe of free groupoid morphisms.

Equations

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

def GraphCoveringTheory.Kurosh.freeGroupoidGeneratorArrow {V : Type u} [q : Quiver V] {a b : Quiver.FreeGroupoid V} (e : ULift.{u, v} (freeGroupoidBaseObj a ⟶ freeGroupoidBaseObj b)) : a ⟶ b

Include a lifted generating arrow into the free groupoid.

Equations

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

@[instance_reducible]

instance GraphCoveringTheory.Kurosh.freeGroupoidIsFreeGroupoid {V : Type u} [q : Quiver V] : IsFreeGroupoid (Quiver.FreeGroupoid V)

Equations

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

@[reducible, inline]

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

The free group contributed by loops in the quotient Bass--Serre graph.

Equations

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

noncomputable def GraphCoveringTheory.Kurosh.kuroshFreePartHom {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : KuroshFreePart G H →* ↥H

Evaluate loops in the quotient graph as elements of the subgroup H.

Equations

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

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

The chosen tree path as a morphism in the quotient graph's free groupoid.

Equations

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

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

Close a quotient edge to a based loop using the chosen tree paths.

Equations

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

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

Evaluate a morphism of the quotient free groupoid using subgroup edge labels.

Equations

• GraphCoveringTheory.Kurosh.quotientPathValue G H p = (Quiver.FreeGroupoid.lift (GraphCoveringTheory.Kurosh.quotientGraphLabelPrefunctor G H)).map p

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

The subgroup label of an oriented quotient edge, inverted for reverse edges.

Equations

• GraphCoveringTheory.Kurosh.quotientSymmEdgeLabel G H (Sum.inl f) = GraphCoveringTheory.Kurosh.quotientEdgeLabel G H f
• GraphCoveringTheory.Kurosh.quotientSymmEdgeLabel G H (Sum.inr f) = (GraphCoveringTheory.Kurosh.quotientEdgeLabel G H f)⁻¹

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

Multiply the labels along a symmetrified quotient path.

Equations

• GraphCoveringTheory.Kurosh.quotientRawPathValue G H p = GraphCoveringTheory.Kurosh.quotientPathValue G H (GraphCoveringTheory.Kurosh.freeGroupoidPathHom p)

theorem GraphCoveringTheory.Kurosh.quotientPathValue_of {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (e : a ⟶ b) : quotientPathValue G H ((Quiver.FreeGroupoid.of (RawBassSerreOrbitVertex G H)).map e) = quotientEdgeLabel G H e

theorem GraphCoveringTheory.Kurosh.quotientPathValue_comp {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b c : RawBassSerreOrbitVertex G H} (p : (Quiver.FreeGroupoid.of (RawBassSerreOrbitVertex G H)).obj a ⟶ (Quiver.FreeGroupoid.of (RawBassSerreOrbitVertex G H)).obj b) (q : (Quiver.FreeGroupoid.of (RawBassSerreOrbitVertex G H)).obj b ⟶ (Quiver.FreeGroupoid.of (RawBassSerreOrbitVertex G H)).obj c) : quotientPathValue G H (CategoryTheory.CategoryStruct.comp p q) = quotientPathValue G H q * quotientPathValue G H p

theorem GraphCoveringTheory.Kurosh.quotientPathValue_inv {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (p : (Quiver.FreeGroupoid.of (RawBassSerreOrbitVertex G H)).obj a ⟶ (Quiver.FreeGroupoid.of (RawBassSerreOrbitVertex G H)).obj b) : quotientPathValue G H (CategoryTheory.Groupoid.inv p) = (quotientPathValue G H p)⁻¹

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

theorem GraphCoveringTheory.Kurosh.quotientRawPathValue_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) : quotientRawPathValue G H (p.cons e) = quotientSymmEdgeLabel G H e * quotientRawPathValue G H p

theorem GraphCoveringTheory.Kurosh.quotientGraphFunctor_map_pos {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (e : a ⟶ b) : (CategoryTheory.SingleObj.toEnd ↥H).symm ((Quiver.FreeGroupoid.lift (quotientGraphLabelPrefunctor G H)).map ((Quiver.FreeGroupoid.of (RawBassSerreOrbitVertex G H)).map e)) = quotientEdgeLabel G H e

theorem GraphCoveringTheory.Kurosh.rawBassSerreOrbitTree_root_eq {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (RawBassSerreOrbitVertex G H)) (rawBassSerreOrbitTree G H)) = rawBassSerreOrbitRoot G H

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

The root of the quotient spanning tree as an ambient quotient vertex.

Equations

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

def GraphCoveringTheory.Kurosh.rawTreeInclusionMapPathAsRaw {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : WideSubquiver.toType (Quiver.Symmetrify (RawBassSerreOrbitVertex G H)) (rawBassSerreOrbitTree G H)} (p : Quiver.Path a b) : Quiver.Path (have this := a; this) (have this := b; this)

Map a tree path to the symmetrified quotient graph without bundled tree vertices.

Equations

• GraphCoveringTheory.Kurosh.rawTreeInclusionMapPathAsRaw G H p = (GraphCoveringTheory.Kurosh.rawTreeInclusion G H).mapPath p

@[simp]

theorem GraphCoveringTheory.Kurosh.rawTreeInclusion_mapPath_asRaw_nil {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a : WideSubquiver.toType (Quiver.Symmetrify (RawBassSerreOrbitVertex G H)) (rawBassSerreOrbitTree G H)} : rawTreeInclusionMapPathAsRaw G H Quiver.Path.nil = Quiver.Path.nil

@[simp]

theorem GraphCoveringTheory.Kurosh.rawTreeInclusion_mapPath_asRaw_cons {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b c : WideSubquiver.toType (Quiver.Symmetrify (RawBassSerreOrbitVertex G H)) (rawBassSerreOrbitTree G H)} (p : Quiver.Path a b) (e : b ⟶ c) : rawTreeInclusionMapPathAsRaw G H (p.cons e) = (rawTreeInclusionMapPathAsRaw G H p).cons ((rawTreeInclusion G H).map e)

def GraphCoveringTheory.Kurosh.rawTreeRootPath {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a : WideSubquiver.toType (Quiver.Symmetrify (RawBassSerreOrbitVertex G H)) (rawBassSerreOrbitTree G H)} (p : Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (RawBassSerreOrbitVertex G H)) (rawBassSerreOrbitTree G H))) a) : Quiver.Path (rawBassSerreOrbitRoot G H) (have this := a; this)

Include a rooted tree path and transport its source to the specified quotient root.

Equations

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

@[simp]

theorem GraphCoveringTheory.Kurosh.rawTreeRootPath_nil {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : rawTreeRootPath G H Quiver.Path.nil = Quiver.Path.nil

@[simp]

theorem GraphCoveringTheory.Kurosh.rawTreeRootPath_cons {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {b c : WideSubquiver.toType (Quiver.Symmetrify (RawBassSerreOrbitVertex G H)) (rawBassSerreOrbitTree G H)} (p : Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (RawBassSerreOrbitVertex G H)) (rawBassSerreOrbitTree G H))) b) (e : b ⟶ c) : rawTreeRootPath G H (p.cons e) = (rawTreeRootPath G H p).cons (rawTreeEdgeMap G H e)

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

The chosen quotient-tree path with its source transported to the specified root.

Equations

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

theorem GraphCoveringTheory.Kurosh.rawTreePathAtRoot_eq_rawTreePath {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (a : RawBassSerreOrbitVertex G H) : rawTreePathAtRoot G H a = rawTreePath G H a

theorem GraphCoveringTheory.Kurosh.rawTreePathAtRoot_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) : rawTreePathMap G H (p.cons e) = (rawTreePathMap G H p).cons (have this := ↑e; this)

theorem GraphCoveringTheory.Kurosh.quotientTreePathHom_eq_rawTreePathAtRoot {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (a : RawBassSerreOrbitVertex G H) : quotientTreePathHom G H a = freeGroupoidPathHom (rawTreePathMap G H (rawTreePathAtRoot G H a))

theorem GraphCoveringTheory.Kurosh.quotientSymmEdgeLabel_tree {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (e : a ⟶ b) (he : e ∈ rawBassSerreOrbitTree G H a b) : quotientSymmEdgeLabel G H e = 1

theorem GraphCoveringTheory.Kurosh.quotientRawPathValue_tree {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (p : Quiver.Path a b) : quotientRawPathValue G H (rawTreePathMap G H p) = 1

theorem GraphCoveringTheory.Kurosh.quotientTreePathValue_one {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (a : RawBassSerreOrbitVertex G H) : quotientPathValue G H (quotientTreePathHom G H a) = 1

theorem GraphCoveringTheory.Kurosh.kuroshFreePartHom_apply {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (x : KuroshFreePart G H) : (kuroshFreePartHom G H) x = quotientPathValue G H x

theorem GraphCoveringTheory.Kurosh.kuroshFreePartHom_quotientEdgeLoop {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (e : a ⟶ b) : (kuroshFreePartHom G H) (quotientEdgeLoop G H e) = quotientEdgeLabel G H e

theorem GraphCoveringTheory.Kurosh.quotientEdgeLoop_tree_pos {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (e : a ⟶ b) (he : e.toPos ∈ rawBassSerreOrbitTree G H a b) : quotientEdgeLoop G H e = CategoryTheory.CategoryStruct.id ((Quiver.FreeGroupoid.of (RawBassSerreOrbitVertex G H)).obj (rawBassSerreOrbitRoot G H))

theorem GraphCoveringTheory.Kurosh.quotientEdgeLoop_tree_neg {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (e : a ⟶ b) (he : e.toNeg ∈ rawBassSerreOrbitTree G H b a) : quotientEdgeLoop G H e = CategoryTheory.CategoryStruct.id ((Quiver.FreeGroupoid.of (RawBassSerreOrbitVertex G H)).obj (rawBassSerreOrbitRoot G H))

theorem GraphCoveringTheory.Kurosh.kuroshFreePartHom_quotientEdgeLoop_tree_pos {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (e : a ⟶ b) (he : e.toPos ∈ rawBassSerreOrbitTree G H a b) : (kuroshFreePartHom G H) (quotientEdgeLoop G H e) = 1

theorem GraphCoveringTheory.Kurosh.kuroshFreePartHom_quotientEdgeLoop_tree_neg {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreOrbitVertex G H} (e : a ⟶ b) (he : e.toNeg ∈ rawBassSerreOrbitTree G H b a) : (kuroshFreePartHom G H) (quotientEdgeLoop G H e) = 1

instance GraphCoveringTheory.Kurosh.kuroshFreePart_isFree {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : IsFreeGroup (KuroshFreePart G H)

@[reducible, inline]

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

Index set for the visible Kurosh factors together with the free part.

Equations

• GraphCoveringTheory.Kurosh.KuroshComponentIndex G H = (GraphCoveringTheory.Kurosh.KuroshFactorIndex G H ⊕ PUnit.{?u.1 + 1})

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

The component group at a Kurosh factor or at the free quotient graph.

Equations

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

@[instance_reducible]

noncomputable instance GraphCoveringTheory.Kurosh.kuroshComponentGroup {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (q : KuroshComponentIndex G H) : Group (KuroshComponent G H q)

Equations

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

The vertex-group version is the convenient graph-of-groups presentation. It retains the (trivial) central vertex groups until the final reduction to the usual factor-only Kurosh indexing.

@[reducible, inline]

noncomputable abbrev GraphCoveringTheory.Kurosh.treeVertexStabilizer {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (a : RawBassSerreOrbitVertex G H) : Subgroup ↥H

The stabilizer in H of the chosen representative of a quotient vertex.

Equations

• GraphCoveringTheory.Kurosh.treeVertexStabilizer G H a = MulAction.stabilizer (↥H) (GraphCoveringTheory.Kurosh.rawTreeRepresentative G H a)

@[reducible, inline]

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

All quotient vertices, together with one additional index for the free part.

Equations

• GraphCoveringTheory.Kurosh.TreeKuroshComponentIndex G H = (GraphCoveringTheory.Kurosh.RawBassSerreOrbitVertex G H ⊕ PUnit.{?u.1 + 1})

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

The family of vertex stabilizers together with the quotient graph's loop group.

Equations

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

@[instance_reducible]

noncomputable instance GraphCoveringTheory.Kurosh.treeKuroshComponentGroup {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (q : TreeKuroshComponentIndex G H) : Group (TreeKuroshComponent G H q)

Equations

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

@[reducible, inline]

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

The free product of all vertex stabilizers and the free part.

Equations

• GraphCoveringTheory.Kurosh.TreeKuroshProduct G H = GraphCoveringTheory.Kurosh.FreeProduct (GraphCoveringTheory.Kurosh.TreeKuroshComponent G H)

noncomputable def GraphCoveringTheory.Kurosh.treeKuroshComponentHom {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (q : TreeKuroshComponentIndex G H) : TreeKuroshComponent G H q →* ↥H

Map each stabilizer by inclusion and the free part by evaluation in H.

Equations

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

noncomputable def GraphCoveringTheory.Kurosh.treeKuroshProductToH {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : TreeKuroshProduct G H →* ↥H

The homomorphism induced by the stabilizer inclusions and free-part evaluation.

Equations

• GraphCoveringTheory.Kurosh.treeKuroshProductToH G H = Monoid.CoprodI.lift (GraphCoveringTheory.Kurosh.treeKuroshComponentHom G H)

noncomputable def GraphCoveringTheory.Kurosh.treeKuroshVertexInclusion {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (a : RawBassSerreOrbitVertex G H) : ↥(treeVertexStabilizer G H a) →* TreeKuroshProduct G H

Include a vertex stabilizer as a factor in the tree Kurosh product.

Equations

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

noncomputable def GraphCoveringTheory.Kurosh.treeKuroshFreeInclusion {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : KuroshFreePart G H →* TreeKuroshProduct G H

Include the quotient graph's loop group as the free factor in the tree product.

Equations

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

@[simp]

theorem GraphCoveringTheory.Kurosh.treeKuroshProductToH_vertex {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (a : RawBassSerreOrbitVertex G H) (x : ↥(treeVertexStabilizer G H a)) : (treeKuroshProductToH G H) ((treeKuroshVertexInclusion G H a) x) = ↑x

@[simp]

theorem GraphCoveringTheory.Kurosh.treeKuroshProductToH_free {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (x : KuroshFreePart G H) : (treeKuroshProductToH G H) ((treeKuroshFreeInclusion G H) x) = (kuroshFreePartHom G H) x

@[reducible, inline]

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

The explicit free product whose factors are the Kurosh stabilizers and free part.

Equations

• GraphCoveringTheory.Kurosh.KuroshProduct G H = GraphCoveringTheory.Kurosh.FreeProduct (GraphCoveringTheory.Kurosh.KuroshComponent G H)