Kurosh Tree

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

@[instance_reducible]

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

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

Equations

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

theorem GraphCoveringTheory.Kurosh.Internal.rightAppendLastIdx {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (i : ι) (w : RightFactorWord i) (a : G i) (ha : a ≠ 1) : wordLastIdx (rightAppendCanonical i w a ha) = some i

theorem GraphCoveringTheory.Kurosh.Internal.factorCentralInjective {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {i i' : ι} {w : RightFactorWord i} {w' : RightFactorWord i'} {a : G i} {a' : G i'} (ha : a ≠ 1) (ha' : a' ≠ 1) (h : rightAppendCanonical i w a ha = rightAppendCanonical i' w' a' ha') : i = i' ∧ w ≍ w' ∧ a ≍ a'

@[reducible, inline]

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

All edges in the word model, bundled with their endpoints.

Equations

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

@[reducible, inline]

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

Nondependent codes for the two constructors of word-model edges.

Equations

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

def GraphCoveringTheory.Kurosh.Internal.bassEdgeCodeOf {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : bassAllEdge G → bassEdgeCode G

Encode a word-model edge without its dependent endpoint indices.

Equations

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

noncomputable def GraphCoveringTheory.Kurosh.Internal.bassEdgeOfCode {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : bassEdgeCode G → bassAllEdge G

Recover a bundled word-model edge from its constructor code.

Equations

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

theorem GraphCoveringTheory.Kurosh.Internal.bassEdgeCodeOf_ofCode {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (c : bassEdgeCode G) : bassEdgeCodeOf G (bassEdgeOfCode G c) = c

theorem GraphCoveringTheory.Kurosh.Internal.bassEdgeOfCode_of {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (e : bassAllEdge G) : bassEdgeOfCode G (bassEdgeCodeOf G e) = e

def GraphCoveringTheory.Kurosh.Internal.bassEdgeTarget {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : bassAllEdge G → BassSerreVertex G

The target of a bundled word-model edge.

Equations

• GraphCoveringTheory.Kurosh.Internal.bassEdgeTarget G e = e.snd.fst

noncomputable def GraphCoveringTheory.Kurosh.Internal.bassEdgeCodeTarget {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : bassEdgeCode G → BassSerreVertex G

Compute the target vertex directly from an edge code.

Equations

• GraphCoveringTheory.Kurosh.Internal.bassEdgeCodeTarget G (Sum.inl ⟨w, ⟨i, hw⟩⟩) = GraphCoveringTheory.Kurosh.BassSerreVertex.factor i ⟨w, hw⟩
• GraphCoveringTheory.Kurosh.Internal.bassEdgeCodeTarget G (Sum.inr ⟨i, ⟨w, ⟨a, ha⟩⟩⟩) = GraphCoveringTheory.Kurosh.BassSerreVertex.central (GraphCoveringTheory.Kurosh.rightAppendCanonical i w a ha)

theorem GraphCoveringTheory.Kurosh.Internal.bassEdgeTarget_ofCode {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (c : bassEdgeCode G) : bassEdgeTarget G (bassEdgeOfCode G c) = bassEdgeCodeTarget G c

theorem GraphCoveringTheory.Kurosh.Internal.bassEdgeCodeTarget_injective {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {c d : bassEdgeCode G} (h : bassEdgeCodeTarget G c = bassEdgeCodeTarget G d) : c = d

theorem GraphCoveringTheory.Kurosh.Internal.bassAllEdge_target_injective {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {e f : bassAllEdge G} (h : bassEdgeTarget G e = bassEdgeTarget G f) : e = f

theorem GraphCoveringTheory.Kurosh.Internal.bassUniqueIncoming {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {a b c : BassSerreVertex G} (e : a ⟶ c) (f : b ⟶ c) : a = b ∧ e ≍ f

theorem GraphCoveringTheory.Kurosh.Internal.wordLastIdx_exists {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (w : Monoid.CoprodI.Word G) (hw : w.toList ≠ []) : ∃ (i : ι), wordLastIdx w = some i

theorem GraphCoveringTheory.Kurosh.Internal.bassRootOrArrow {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (b : BassSerreVertex G) : b = BassSerreVertex.central Monoid.CoprodI.Word.empty ∨ ∃ (a : BassSerreVertex G), Nonempty (a ⟶ b)

def GraphCoveringTheory.Kurosh.Internal.bassHeight {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : BassSerreVertex G → ℕ

Twice the reduced-word length, plus one at factor vertices.

Equations

• GraphCoveringTheory.Kurosh.Internal.bassHeight G (GraphCoveringTheory.Kurosh.BassSerreVertex.central w) = 2 * w.toList.length
• GraphCoveringTheory.Kurosh.Internal.bassHeight G (GraphCoveringTheory.Kurosh.BassSerreVertex.factor i w) = 2 * (↑w).toList.length + 1

theorem GraphCoveringTheory.Kurosh.Internal.bassHeight_lt {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {a b : BassSerreVertex G} (e : a ⟶ b) : bassHeight G a < bassHeight G b

@[instance_reducible]

noncomputable def GraphCoveringTheory.Kurosh.Internal.bassSerreFullArborescence {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : Quiver.Arborescence (BassSerreVertex G)

The directed word model is an arborescence rooted at the empty word.

Equations

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

theorem GraphCoveringTheory.Kurosh.Internal.bassHeight_root {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : bassHeight G (BassSerreVertex.central Monoid.CoprodI.Word.empty) = 0

theorem GraphCoveringTheory.Kurosh.Internal.bassHeight_edge_eq_succ {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {a b : BassSerreVertex G} (e : a ⟶ b) : bassHeight G b = bassHeight G a + 1

def GraphCoveringTheory.Kurosh.Internal.bassSymmHeight {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (x : Quiver.Symmetrify (BassSerreVertex G)) : ℕ

The word-length height function on symmetrified word-model vertices.

Equations

• GraphCoveringTheory.Kurosh.Internal.bassSymmHeight G x = GraphCoveringTheory.Kurosh.Internal.bassHeight G x

theorem GraphCoveringTheory.Kurosh.Internal.bassHeight_symm_edge {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {a b : BassSerreVertex G} (e : a ⟶ b) : bassSymmHeight G b = bassSymmHeight G a + 1 ∨ bassSymmHeight G a = bassSymmHeight G b + 1

theorem GraphCoveringTheory.Kurosh.Internal.bassHeight_path_le {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {a b : BassSerreVertex G} (p : Quiver.Path a b) : bassSymmHeight G b ≤ bassSymmHeight G a + p.length

theorem GraphCoveringTheory.Kurosh.Internal.bassHeight_directed_path_eq {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {a b : BassSerreVertex G} (p : Quiver.Path a b) : bassHeight G b = bassHeight G a + p.length

theorem GraphCoveringTheory.Kurosh.Internal.bassHeight_zero_iff {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {b : BassSerreVertex G} : bassHeight G b = 0 ↔ b = BassSerreVertex.central Monoid.CoprodI.Word.empty

def GraphCoveringTheory.Kurosh.Internal.bassToSymm {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : BassSerreVertex G ⥤q Quiver.Symmetrify (BassSerreVertex G)

Include the directed word model into its symmetrification.

Equations

• GraphCoveringTheory.Kurosh.Internal.bassToSymm G = { obj := id, map := fun {X Y : GraphCoveringTheory.Kurosh.BassSerreVertex G} (e : X ⟶ Y) => e.toPos }

theorem GraphCoveringTheory.Kurosh.Internal.bassToSymm_mapPath_length {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {a b : BassSerreVertex G} (p : Quiver.Path a b) : ((bassToSymm G).mapPath p).length = p.length

theorem GraphCoveringTheory.Kurosh.Internal.bassSymmPath_of_length_eq {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {b : BassSerreVertex G} (p : Quiver.Path (BassSerreVertex.central Monoid.CoprodI.Word.empty) b) (hp : p.length = bassSymmHeight G b) : ∃ (q : Quiver.Path (BassSerreVertex.central Monoid.CoprodI.Word.empty) b), (bassToSymm G).mapPath q = p

theorem GraphCoveringTheory.Kurosh.Internal.bass_edge_mem_geodesicTree {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {a b : BassSerreVertex G} (e : a ⟶ b) : e.toPos ∈ bassSerreTree G a b

theorem GraphCoveringTheory.Kurosh.Internal.rightTailCanonical_factorCoset_eq {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (i : ι) (g h : FreeProduct G) (hc : factorCosetMk G i g = factorCosetMk G i h) : rightTailCanonical i (Monoid.CoprodI.Word.equiv g) = rightTailCanonical i (Monoid.CoprodI.Word.equiv h)

noncomputable def GraphCoveringTheory.Kurosh.Internal.rawCanonicalFactor {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (i : ι) (c : FactorCoset G i) : RightFactorWord i

Choose the canonical reduced-word representative of a factor coset.

Equations

• GraphCoveringTheory.Kurosh.Internal.rawCanonicalFactor G i c = GraphCoveringTheory.Kurosh.rightTailCanonical i (Monoid.CoprodI.Word.equiv (Quotient.out c))

noncomputable def GraphCoveringTheory.Kurosh.Internal.rawCanonicalVertex {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : RawBassSerreVertex G → BassSerreVertex G

Convert a group-and-coset vertex into its canonical word-model vertex.

Equations

• One or more equations did not get rendered due to their size.
• GraphCoveringTheory.Kurosh.Internal.rawCanonicalVertex G (GraphCoveringTheory.Kurosh.RawBassSerreVertex.central g) = GraphCoveringTheory.Kurosh.BassSerreVertex.central (Monoid.CoprodI.Word.equiv g)

def GraphCoveringTheory.Kurosh.Internal.bassToRawVertex {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : BassSerreVertex G → RawBassSerreVertex G

Evaluate a word-model vertex in the group-and-coset model.

Equations

• One or more equations did not get rendered due to their size.
• GraphCoveringTheory.Kurosh.Internal.bassToRawVertex G (GraphCoveringTheory.Kurosh.BassSerreVertex.central w) = GraphCoveringTheory.Kurosh.RawBassSerreVertex.central w.prod

theorem GraphCoveringTheory.Kurosh.Internal.rawCanonicalFactor_coset {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (i : ι) (c : FactorCoset G i) : factorCosetMk G i (↑(rawCanonicalFactor G i c)).prod = c

theorem GraphCoveringTheory.Kurosh.Internal.bassToRawVertex_rawCanonicalVertex {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (x : RawBassSerreVertex G) : bassToRawVertex G (rawCanonicalVertex G x) = x

theorem GraphCoveringTheory.Kurosh.Internal.rawCanonicalVertex_bassToRawVertex {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (x : BassSerreVertex G) : rawCanonicalVertex G (bassToRawVertex G x) = x

@[reducible]

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

The chosen word-model spanning tree on the ambient vertex type.

Equations

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

@[instance_reducible]

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

Equations

• GraphCoveringTheory.Kurosh.Internal.bassTreeQuiverArborescence G = id (GraphCoveringTheory.Kurosh.bassSerreTreeArborescence G)

noncomputable def GraphCoveringTheory.Kurosh.Internal.bassTreePath {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (x : BassSerreVertex G) : Quiver.Path (BassSerreVertex.central Monoid.CoprodI.Word.empty) x

The unique path in the chosen word-model tree from the empty word.

Equations

• GraphCoveringTheory.Kurosh.Internal.bassTreePath G x = default

def GraphCoveringTheory.Kurosh.Internal.bassTreePathMap {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {x y : BassSerreVertex G} : Quiver.Path x y → Quiver.Path x y

Forget membership in the chosen word-model spanning tree along a path.

Equations

• GraphCoveringTheory.Kurosh.Internal.bassTreePathMap G Quiver.Path.nil = Quiver.Path.nil
• GraphCoveringTheory.Kurosh.Internal.bassTreePathMap G (p.cons e) = (GraphCoveringTheory.Kurosh.Internal.bassTreePathMap G p).cons ↑e

theorem GraphCoveringTheory.Kurosh.Internal.bassTreePathMap_cons {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {x y z : BassSerreVertex G} (p : Quiver.Path x y) (e : y ⟶ z) : bassTreePathMap G (p.cons e) = (bassTreePathMap G p).cons ↑e

theorem GraphCoveringTheory.Kurosh.Internal.bassTreePathMap_edge_pos {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {x y : BassSerreVertex G} (e : x ⟶ y) (he : e.toPos ∈ bassSerreTree G x y) : bassTreePathMap G (bassTreePath G y) = (bassTreePathMap G (bassTreePath G x)).cons e.toPos

noncomputable def GraphCoveringTheory.Kurosh.Internal.bassPathHom {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {x y : BassSerreVertex G} : Quiver.Path x y → ((Quiver.FreeGroupoid.of (BassSerreVertex G)).obj x ⟶ (Quiver.FreeGroupoid.of (BassSerreVertex G)).obj y)

Interpret a symmetrified word-model path in its free groupoid.

Equations

• One or more equations did not get rendered due to their size.
• GraphCoveringTheory.Kurosh.Internal.bassPathHom G Quiver.Path.nil = CategoryTheory.CategoryStruct.id ((Quiver.FreeGroupoid.of (GraphCoveringTheory.Kurosh.BassSerreVertex G)).obj x)

theorem GraphCoveringTheory.Kurosh.Internal.bassPathHom_nil {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {x : BassSerreVertex G} : bassPathHom G Quiver.Path.nil = CategoryTheory.CategoryStruct.id ((Quiver.FreeGroupoid.of (BassSerreVertex G)).obj x)

theorem GraphCoveringTheory.Kurosh.Internal.bassPathHom_cons {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {x y z : BassSerreVertex G} (p : Quiver.Path x y) (e : y ⟶ z) : bassPathHom G (p.cons e) = CategoryTheory.CategoryStruct.comp (bassPathHom G p) (match e with | Sum.inl f => (Quiver.FreeGroupoid.of (BassSerreVertex G)).map f | Sum.inr f => CategoryTheory.Groupoid.inv ((Quiver.FreeGroupoid.of (BassSerreVertex G)).map f))

theorem GraphCoveringTheory.Kurosh.Internal.bassQuotientMap_cons {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {x y z : BassSerreVertex G} (p : Quiver.Path x y) (e : y ⟶ z) : (CategoryTheory.Quotient.functor Quiver.FreeGroupoid.redStep).map (p.cons e) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Quotient.functor Quiver.FreeGroupoid.redStep).map p) (match e with | Sum.inl f => (Quiver.FreeGroupoid.of (BassSerreVertex G)).map f | Sum.inr f => CategoryTheory.Groupoid.inv ((Quiver.FreeGroupoid.of (BassSerreVertex G)).map f))

theorem GraphCoveringTheory.Kurosh.Internal.bassPathHom_eq_quotient_map {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {x y : BassSerreVertex G} (p : Quiver.Path x y) : bassPathHom G p = (CategoryTheory.Quotient.functor Quiver.FreeGroupoid.redStep).map p

theorem GraphCoveringTheory.Kurosh.Internal.bassTreePathHom_edge_neg {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {x y : BassSerreVertex G} (e : x ⟶ y) (he : e.toPos ∈ bassSerreTree G x y) : CategoryTheory.CategoryStruct.comp (bassPathHom G (bassTreePathMap G (bassTreePath G y))) (CategoryTheory.Groupoid.inv ((Quiver.FreeGroupoid.of (BassSerreVertex G)).map e)) = bassPathHom G (bassTreePathMap G (bassTreePath G x))

theorem GraphCoveringTheory.Kurosh.Internal.bassPathHom_eq_tree {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {x : BassSerreVertex G} (p : Quiver.Path (BassSerreVertex.central Monoid.CoprodI.Word.empty) x) : bassPathHom G p = bassPathHom G (bassTreePathMap G (bassTreePath G x))

theorem GraphCoveringTheory.Kurosh.Internal.bassFreeGroupoid_end_subsingleton {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : Subsingleton (CategoryTheory.End ((Quiver.FreeGroupoid.of (BassSerreVertex G)).obj (BassSerreVertex.central Monoid.CoprodI.Word.empty)))

noncomputable def GraphCoveringTheory.Kurosh.Internal.freePathHom {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 symmetrified quiver path in the quiver's free groupoid.

Equations

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

theorem GraphCoveringTheory.Kurosh.Internal.freeGroupoid_isConnected_of_basedPaths {V : Type u} [q : Quiver V] (r : V) [Quiver.RootedConnected (have this := r; this)] : CategoryTheory.IsConnected (Quiver.FreeGroupoid V)

theorem GraphCoveringTheory.Kurosh.Internal.bassFreeGroupoid_end_subsingleton_at {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (x : Quiver.FreeGroupoid (BassSerreVertex G)) : Subsingleton (CategoryTheory.End x)

theorem GraphCoveringTheory.Kurosh.Internal.functor_map_injective_of_eq_id {C : Type u} [CategoryTheory.Category.{u_1, u} C] (F : CategoryTheory.Functor C C) (hF : F = CategoryTheory.Functor.id C) (x : C) : Function.Injective fun (f : CategoryTheory.End x) => F.map f

theorem GraphCoveringTheory.Kurosh.Internal.bass_factorCoset_append {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (i : ι) (w : RightFactorWord i) (a : G i) (ha : a ≠ 1) : factorCosetMk G i (rightAppendCanonical i w a ha).prod = factorCosetMk G i (↑w).prod

theorem GraphCoveringTheory.Kurosh.Internal.rawCanonicalVertex_factorCosetMk {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (i : ι) (g : FreeProduct G) : rawCanonicalVertex G (RawBassSerreVertex.factor i (factorCosetMk G i g)) = BassSerreVertex.factor i (rightTailCanonical i (Monoid.CoprodI.Word.equiv g))

noncomputable def GraphCoveringTheory.Kurosh.Internal.bassToRawPrefunctor {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : BassSerreVertex G ⥤q Quiver.FreeGroupoid (RawBassSerreVertex G)

Evaluate word-model edges as morphisms in the raw model's free groupoid.

Equations

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

noncomputable def GraphCoveringTheory.Kurosh.Internal.rawToBassPrefunctor {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : RawBassSerreVertex G ⥤q Quiver.FreeGroupoid (BassSerreVertex G)

Express group-and-coset edges as paths in the word model's free groupoid.

Equations

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

noncomputable def GraphCoveringTheory.Kurosh.Internal.bassToRawFunctor {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : CategoryTheory.Functor (Quiver.FreeGroupoid (BassSerreVertex G)) (Quiver.FreeGroupoid (RawBassSerreVertex G))

Extend word evaluation to a functor between the two free groupoids.

Equations

• GraphCoveringTheory.Kurosh.Internal.bassToRawFunctor G = Quiver.FreeGroupoid.lift (GraphCoveringTheory.Kurosh.Internal.bassToRawPrefunctor G)

noncomputable def GraphCoveringTheory.Kurosh.Internal.rawToBassFunctor {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : CategoryTheory.Functor (Quiver.FreeGroupoid (RawBassSerreVertex G)) (Quiver.FreeGroupoid (BassSerreVertex G))

Extend canonical word representatives to a functor between the two free groupoids.

Equations

• GraphCoveringTheory.Kurosh.Internal.rawToBassFunctor G = Quiver.FreeGroupoid.lift (GraphCoveringTheory.Kurosh.Internal.rawToBassPrefunctor G)

theorem GraphCoveringTheory.Kurosh.Internal.rawToBassFunctor_map_of {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {a b : RawBassSerreVertex G} (e : a ⟶ b) : Quiver.homOfEq ((rawToBassFunctor G).map ((Quiver.FreeGroupoid.of (RawBassSerreVertex G)).map e)) ⋯ ⋯ = (rawToBassPrefunctor G).map e

theorem GraphCoveringTheory.Kurosh.Internal.bassToRawFunctor_map_of {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] {a b : BassSerreVertex G} (e : a ⟶ b) : Quiver.homOfEq ((bassToRawFunctor G).map ((Quiver.FreeGroupoid.of (BassSerreVertex G)).map e)) ⋯ ⋯ = (bassToRawPrefunctor G).map e

theorem GraphCoveringTheory.Kurosh.Internal.bassToRawPrefunctor_map_centralFactor {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (g : FreeProduct G) (i : ι) (hw : wordLastIdx (Monoid.CoprodI.Word.equiv g) ≠ some i) : (bassToRawPrefunctor G).map (BassSerreEdge.centralFactor (Monoid.CoprodI.Word.equiv g) i hw) = (Quiver.FreeGroupoid.of (RawBassSerreVertex G)).map (RawBassSerreEdge.centralFactor (Monoid.CoprodI.Word.equiv g).prod i)

theorem GraphCoveringTheory.Kurosh.Internal.bassToRawPrefunctor_map_factorCentral {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (i : ι) (w : RightFactorWord i) (a : G i) (ha : a ≠ 1) (hv : RawBassSerreVertex.factor i (factorCosetMk G i (rightAppendCanonical i w a ha).prod) = bassToRawVertex G (BassSerreVertex.factor i w)) : (bassToRawPrefunctor G).map (BassSerreEdge.factorCentral i w a ha) = CategoryTheory.Groupoid.inv (Quiver.homOfEq ((Quiver.FreeGroupoid.of (RawBassSerreVertex G)).map (RawBassSerreEdge.centralFactor (rightAppendCanonical i w a ha).prod i)) ⋯ ⋯)

theorem GraphCoveringTheory.Kurosh.Internal.functor_map_homOfEq {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {X Y X' Y' : C} (F : CategoryTheory.Functor C D) (f : X ⟶ Y) (hX : X = X') (hY : Y = Y') : F.map (Quiver.homOfEq f hX hY) = Quiver.homOfEq (F.map f) ⋯ ⋯

theorem GraphCoveringTheory.Kurosh.Internal.groupoid_inv_homOfEq {C : Type u_1} [CategoryTheory.Groupoid C] {X Y X' Y' : C} (f : X ⟶ Y) (hX : X = X') (hY : Y = Y') : CategoryTheory.Groupoid.inv (Quiver.homOfEq f hX hY) = Quiver.homOfEq (CategoryTheory.Groupoid.inv f) hY hX

theorem GraphCoveringTheory.Kurosh.Internal.groupoid_inv_inv {C : Type u_1} [CategoryTheory.Groupoid C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Groupoid.inv (CategoryTheory.Groupoid.inv f) = f

theorem GraphCoveringTheory.Kurosh.Internal.groupoid_inv_inv_homOfEq {C : Type u_1} [CategoryTheory.Groupoid C] {X Y X' Y' : C} (f : X ⟶ Y) (hX : X = X') (hY : Y = Y') : CategoryTheory.Groupoid.inv (CategoryTheory.Groupoid.inv (Quiver.homOfEq f hX hY)) = Quiver.homOfEq f hX hY

theorem GraphCoveringTheory.Kurosh.Internal.homOfEq_transport {C : Type u_1} [Quiver C] {X Y X' Y' X'' Y'' : C} (f : X ⟶ Y) (g : X' ⟶ Y') (hX : X = X') (hY : Y = Y') (kX : X' = X'') (kY : Y' = Y'') (h : Quiver.homOfEq f hX hY = g) : Quiver.homOfEq f ⋯ ⋯ = Quiver.homOfEq g kX kY

theorem GraphCoveringTheory.Kurosh.Internal.homOfEq_transport' {C : Type u_1} [Quiver C] {X Y X' Y' X'' Y'' : C} (f : X ⟶ Y) (g : X' ⟶ Y') (hX : X = X') (hY : Y = Y') (kX : X' = X'') (kY : Y' = Y'') (lX : X = X'') (lY : Y = Y'') (h : Quiver.homOfEq f hX hY = g) : Quiver.homOfEq f lX lY = Quiver.homOfEq g kX kY

theorem GraphCoveringTheory.Kurosh.Internal.homOfEq_eq_of_heq {C : Type u_1} [Quiver C] {X Y X' Y' : C} {f : X ⟶ Y} {g : X' ⟶ Y'} (hX : X = X') (hY : Y = Y') (hfg : f ≍ g) : Quiver.homOfEq f hX hY = g

@[reducible, inline]

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

All edges of the group-and-coset model, bundled with their endpoints.

Equations

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

theorem GraphCoveringTheory.Kurosh.Internal.rawEdge_heq {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (g h : FreeProduct G) (i : ι) (gh : g = h) : RawBassSerreEdge.centralFactor g i ≍ RawBassSerreEdge.centralFactor h i

theorem GraphCoveringTheory.Kurosh.Internal.rawEdgeMap_heq {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (g h : FreeProduct G) (i : ι) (gh : g = h) : (Quiver.FreeGroupoid.of (RawBassSerreVertex G)).map (RawBassSerreEdge.centralFactor g i) ≍ (Quiver.FreeGroupoid.of (RawBassSerreVertex G)).map (RawBassSerreEdge.centralFactor h i)

theorem GraphCoveringTheory.Kurosh.Internal.rawBassRaw_obj {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (x : RawBassSerreVertex G) : ((rawToBassFunctor G).comp (bassToRawFunctor G)).obj ((Quiver.FreeGroupoid.of (RawBassSerreVertex G)).obj x) = (Quiver.FreeGroupoid.of (RawBassSerreVertex G)).obj x

noncomputable def GraphCoveringTheory.Kurosh.Internal.rawBassRawPrefunctor {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : RawBassSerreVertex G ⥤q Quiver.FreeGroupoid (RawBassSerreVertex G)

The composite converting raw edges to word-model paths and evaluating them back.

Equations

• GraphCoveringTheory.Kurosh.Internal.rawBassRawPrefunctor G = GraphCoveringTheory.Kurosh.Internal.rawToBassPrefunctor G ⋙q (GraphCoveringTheory.Kurosh.Internal.bassToRawFunctor G).toPrefunctor

theorem GraphCoveringTheory.Kurosh.Internal.rawBassRawPrefunctor_eq_of {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : rawBassRawPrefunctor G = Quiver.FreeGroupoid.of (RawBassSerreVertex G)

theorem GraphCoveringTheory.Kurosh.Internal.rawBassRawFunctor_eq_id {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : (rawToBassFunctor G).comp (bassToRawFunctor G) = CategoryTheory.Functor.id (Quiver.FreeGroupoid (RawBassSerreVertex G))

theorem GraphCoveringTheory.Kurosh.Internal.rawFreeGroupoid_end_subsingleton {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : Subsingleton (CategoryTheory.End ((Quiver.FreeGroupoid.of (RawBassSerreVertex G)).obj (RawBassSerreVertex.central 1)))

@[reducible, inline]

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

All quotient-graph edges bundled with their endpoints.

Equations

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

def GraphCoveringTheory.Kurosh.Internal.treeDataGeneratorSet {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : Set ↥H

The union of the vertex stabilizers and the quotient-edge labels inside H.

Equations

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

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

The subgroup generated by vertex stabilizers and quotient-edge labels.

Equations

• GraphCoveringTheory.Kurosh.Internal.treeDataGenerated G H = Subgroup.closure (GraphCoveringTheory.Kurosh.Internal.treeDataGeneratorSet G H)

@[reducible]

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

The raw model's chosen spanning tree on the ambient vertex type.

Equations

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

@[instance_reducible]

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

Equations

• GraphCoveringTheory.Kurosh.Internal.rawSpanningTreeQuiverArborescence G = id (GraphCoveringTheory.Kurosh.rawBassSerreTreeArborescence G)

theorem GraphCoveringTheory.Kurosh.Internal.treeDataGenerated_mem_vertex {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (a : RawBassSerreOrbitVertex G H) (x : ↥(treeVertexStabilizer G H a)) : ↑x ∈ treeDataGenerated G H

theorem GraphCoveringTheory.Kurosh.Internal.treeDataGenerated_mem_edge {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (e : orbitAllEdge G H) : quotientEdgeLabel G H e.snd.snd ∈ treeDataGenerated G H

theorem GraphCoveringTheory.Kurosh.Internal.rawEdgeMap_dataOf {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreVertex G} (e : a ⟶ b) : rawBassSerreOrbitEdgeMk G H (rawBassSerreEdgeDataOf G e) = ↑(rawBassSerreOrbitEdgeMap G H e)

noncomputable def GraphCoveringTheory.Kurosh.Internal.actionOrbitAlign {A X : Type w} [Group A] [MulAction A X] {x y : X} (h : actionOrbitMk A X x = actionOrbitMk A X y) : A

Choose a group element sending one point to another in the same orbit.

Equations

• GraphCoveringTheory.Kurosh.Internal.actionOrbitAlign h = Classical.choose ⋯

theorem GraphCoveringTheory.Kurosh.Internal.actionOrbitAlign_spec {A X : Type w} [Group A] [MulAction A X] {x y : X} (h : actionOrbitMk A X x = actionOrbitMk A X y) : actionOrbitAlign h • x = y

theorem GraphCoveringTheory.Kurosh.Internal.rawEdgeData_rep_orbit_eq {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreVertex G} (e : a ⟶ b) : actionOrbitMk (↥H) (rawBassSerreEdgeData G) (quotientEdgeRawData G H (rawBassSerreOrbitEdgeMap G H e)) = actionOrbitMk (↥H) (rawBassSerreEdgeData G) (rawBassSerreEdgeDataOf G e)

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

Align a raw edge with the chosen representative of its quotient edge.

Equations

• GraphCoveringTheory.Kurosh.Internal.rawEdgeOrbitAlign G H e = GraphCoveringTheory.Kurosh.Internal.actionOrbitAlign ⋯

theorem GraphCoveringTheory.Kurosh.Internal.rawEdgeOrbitAlign_spec {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreVertex G} (e : a ⟶ b) : rawEdgeOrbitAlign G H e • quotientEdgeRawData G H (rawBassSerreOrbitEdgeMap G H e) = rawBassSerreEdgeDataOf G e

theorem GraphCoveringTheory.Kurosh.Internal.rawTreeRepresentative_root {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : rawTreeRepresentative G H (rawBassSerreOrbitRoot G H) = RawBassSerreVertex.central 1

theorem GraphCoveringTheory.Kurosh.Internal.conjugate_mem_stabilizer {A X : Type w} [Group A] [MulAction A X] (x : X) (s k : A) (hk : k • x = x) : s * k * s⁻¹ ∈ MulAction.stabilizer A (s • x)

theorem GraphCoveringTheory.Kurosh.Internal.stabilizer_conjugate_eq {A : Type w} [Group A] (s k u r : A) : u * (s * k * s⁻¹) * s = r ↔ k = (u * s)⁻¹ * r

theorem GraphCoveringTheory.Kurosh.Internal.positive_step {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreVertex G} (e : a ⟶ b) (u : ↥H) (hu : ↑u • rawTreeRepresentative G H (actionOrbitMk (↥H) (RawBassSerreVertex G) a) = a) : ∃ (v : ↥(treeVertexStabilizer G H (actionOrbitMk (↥H) (RawBassSerreVertex G) a))), rawEdgeOrbitAlign G H e = u * ↑v * quotientEdgeCoherentSourceAlign G H (rawBassSerreOrbitEdgeMap G H e) ∧ b = ↑(u * ↑v * (quotientEdgeLabel G H (rawBassSerreOrbitEdgeMap G H e))⁻¹) • rawTreeRepresentative G H (actionOrbitMk (↥H) (RawBassSerreVertex G) b)

theorem GraphCoveringTheory.Kurosh.Internal.negative_step {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreVertex G} (e : a ⟶ b) (u : ↥H) (hu : ↑u • rawTreeRepresentative G H (actionOrbitMk (↥H) (RawBassSerreVertex G) b) = b) : ∃ (v : ↥(treeVertexStabilizer G H (actionOrbitMk (↥H) (RawBassSerreVertex G) b))), rawEdgeOrbitAlign G H e = u * ↑v * (quotientEdgeLabel G H (rawBassSerreOrbitEdgeMap G H e) * quotientEdgeCoherentSourceAlign G H (rawBassSerreOrbitEdgeMap G H e)) ∧ a = ↑(u * ↑v * quotientEdgeLabel G H (rawBassSerreOrbitEdgeMap G H e)) • rawTreeRepresentative G H (actionOrbitMk (↥H) (RawBassSerreVertex G) a)

noncomputable def GraphCoveringTheory.Kurosh.Internal.positiveStepVertex {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreVertex G} (e : a ⟶ b) (u : ↥H) (hu : ↑u • rawTreeRepresentative G H (actionOrbitMk (↥H) (RawBassSerreVertex G) a) = a) : ↥(treeVertexStabilizer G H (actionOrbitMk (↥H) (RawBassSerreVertex G) a))

The stabilizer correction required when traversing a positive raw edge.

Equations

• GraphCoveringTheory.Kurosh.Internal.positiveStepVertex G H e u hu = Classical.choose ⋯

theorem GraphCoveringTheory.Kurosh.Internal.positiveStepVertex_endpoint {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreVertex G} (e : a ⟶ b) (u : ↥H) (hu : ↑u • rawTreeRepresentative G H (actionOrbitMk (↥H) (RawBassSerreVertex G) a) = a) : b = ↑(u * ↑(positiveStepVertex G H e u hu) * (quotientEdgeLabel G H (rawBassSerreOrbitEdgeMap G H e))⁻¹) • rawTreeRepresentative G H (actionOrbitMk (↥H) (RawBassSerreVertex G) b)

noncomputable def GraphCoveringTheory.Kurosh.Internal.negativeStepVertex {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreVertex G} (e : a ⟶ b) (u : ↥H) (hu : ↑u • rawTreeRepresentative G H (actionOrbitMk (↥H) (RawBassSerreVertex G) b) = b) : ↥(treeVertexStabilizer G H (actionOrbitMk (↥H) (RawBassSerreVertex G) b))

The stabilizer correction required when traversing a negative raw edge.

Equations

• GraphCoveringTheory.Kurosh.Internal.negativeStepVertex G H e u hu = Classical.choose ⋯

theorem GraphCoveringTheory.Kurosh.Internal.negativeStepVertex_endpoint {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a b : RawBassSerreVertex G} (e : a ⟶ b) (u : ↥H) (hu : ↑u • rawTreeRepresentative G H (actionOrbitMk (↥H) (RawBassSerreVertex G) b) = b) : a = ↑(u * ↑(negativeStepVertex G H e u hu) * quotientEdgeLabel G H (rawBassSerreOrbitEdgeMap G H e)) • rawTreeRepresentative G H (actionOrbitMk (↥H) (RawBassSerreVertex G) a)

noncomputable def GraphCoveringTheory.Kurosh.Internal.rawPathAlignmentGenerated {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {x : RawBassSerreVertex G} : Quiver.Path (RawBassSerreVertex.central 1) x → { u : ↥H // x = ↑u • rawTreeRepresentative G H (actionOrbitMk (↥H) (RawBassSerreVertex G) x) ∧ u ∈ treeDataGenerated G H }

Align the endpoint of a rooted raw tree path using the subgroup generated by tree data.

Equations

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

noncomputable def GraphCoveringTheory.Kurosh.Internal.rawPathProduct {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {x : RawBassSerreVertex G} : Quiver.Path (RawBassSerreVertex.central 1) x → TreeKuroshProduct G H

The element of the tree Kurosh product reconstructed along a rooted raw tree path.

Equations

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

theorem GraphCoveringTheory.Kurosh.treeKuroshProductToH_testRawPathProduct {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {x : RawBassSerreVertex G} (p : Quiver.Path (RawBassSerreVertex.central 1) x) : (treeKuroshProductToH G H) (Internal.rawPathProduct G H p) = ↑(Internal.rawPathAlignmentGenerated G H p)

noncomputable def GraphCoveringTheory.Kurosh.Internal.rawSpanningTreePath {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (x : RawBassSerreVertex G) : Quiver.Path (RawBassSerreVertex.central 1) x

The unique path in the raw spanning tree from the identity vertex.

Equations

• GraphCoveringTheory.Kurosh.Internal.rawSpanningTreePath G x = default