Index Formula

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

@[instance_reducible]

noncomputable instance GraphCoveringTheory.actionCategoryFintype (M A : Type u) [Monoid M] [MulAction M A] [Fintype A] : Fintype (CategoryTheory.ActionCategory M A)

Equations

• GraphCoveringTheory.actionCategoryFintype M A = Fintype.ofEquiv A (CategoryTheory.ActionCategory.objEquiv M A)

@[instance_reducible]

noncomputable instance GraphCoveringTheory.coverHomFintype (α A : Type u) [MulAction (FreeGroup α) A] [Fintype α] (a b : CoverVertex α A) : Fintype (a ⟶ b)

Equations

• GraphCoveringTheory.coverHomFintype α A a b = Fintype.subtype {e : α | FreeGroup.of e • CategoryTheory.ActionCategory.back a = CategoryTheory.ActionCategory.back b} ⋯

def GraphCoveringTheory.coverGeneratorTotalEquiv (α A : Type u) [MulAction (FreeGroup α) A] : Quiver.Total (CoverVertex α A) ≃ A × α

A Schreier edge is determined by its source and its free generator.

Equations

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

def GraphCoveringTheory.freeActionGeneratorTotalEquiv (α A : Type u) [MulAction (FreeGroup α) A] : Quiver.Total (CoverVertex α A) ≃ A × α

The action groupoid's chosen generating edges are indexed by a point and a generator.

Equations

• GraphCoveringTheory.freeActionGeneratorTotalEquiv α A = GraphCoveringTheory.coverGeneratorTotalEquiv α A

noncomputable def GraphCoveringTheory.freeGroupoidTree (G : Type u) [CategoryTheory.Groupoid G] [IsFreeGroupoid G] [CategoryTheory.IsConnected G] (r : G) : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))

The geodesic spanning tree in the symmetrified generating quiver, rooted at r.

Equations

• GraphCoveringTheory.freeGroupoidTree G r = Quiver.geodesicSubtree (have this := r; this)

@[reducible]

noncomputable def GraphCoveringTheory.freeGroupoidTreeArborescence (G : Type u) [CategoryTheory.Groupoid G] [IsFreeGroupoid G] [CategoryTheory.IsConnected G] (r : G) : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) (freeGroupoidTree G r))

The chosen geodesic spanning tree is an arborescence rooted at r.

Equations

• GraphCoveringTheory.freeGroupoidTreeArborescence G r = id (Quiver.geodesicArborescence (have this := r; this))

@[reducible, inline]

noncomputable abbrev GraphCoveringTheory.freeGroupoidGeneratorSet (G : Type u) [CategoryTheory.Groupoid G] [IsFreeGroupoid G] [CategoryTheory.IsConnected G] (r : G) : Set (Quiver.Total (IsFreeGroupoid.Generators G))

The generators outside the chosen geodesic spanning tree.

Equations

• GraphCoveringTheory.freeGroupoidGeneratorSet G r = (Quiver.wideSubquiverEquivSetTotal (Quiver.wideSubquiverSymmetrify (GraphCoveringTheory.freeGroupoidTree G r)))ᶜ

@[instance_reducible]

noncomputable instance GraphCoveringTheory.freeGroupoidGeneratorSetFintype (G : Type u) [CategoryTheory.Groupoid G] [IsFreeGroupoid G] [CategoryTheory.IsConnected G] [Fintype (IsFreeGroupoid.Generators G)] [(a b : IsFreeGroupoid.Generators G) → Fintype (a ⟶ b)] (r : G) : Fintype ↑(freeGroupoidGeneratorSet G r)

Equations

• GraphCoveringTheory.freeGroupoidGeneratorSetFintype G r = inferInstance

@[reducible, inline]

noncomputable abbrev GraphCoveringTheory.generatorComplement (G : Type u) [CategoryTheory.Groupoid G] [IsFreeGroupoid G] (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) : Set (Quiver.Total (IsFreeGroupoid.Generators G))

The generating edges outside a given wide subquiver and its reverse.

Equations

• GraphCoveringTheory.generatorComplement G T = (Quiver.wideSubquiverEquivSetTotal (Quiver.wideSubquiverSymmetrify T))ᶜ

@[instance_reducible]

noncomputable instance GraphCoveringTheory.generatorComplementFintype (G : Type u) [CategoryTheory.Groupoid G] [IsFreeGroupoid G] [Fintype (IsFreeGroupoid.Generators G)] [(a b : IsFreeGroupoid.Generators G) → Fintype (a ⟶ b)] (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) : Fintype ↑(generatorComplement G T)

Equations

• GraphCoveringTheory.generatorComplementFintype G T = inferInstance

theorem GraphCoveringTheory.generatorComplement_card (G : Type u) [CategoryTheory.Groupoid G] [IsFreeGroupoid G] [Fintype (IsFreeGroupoid.Generators G)] [(a b : IsFreeGroupoid.Generators G) → Fintype (a ⟶ b)] (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) [Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] : Fintype.card ↑(generatorComplement G T) = Fintype.card (Quiver.Total (IsFreeGroupoid.Generators G)) + 1 - Fintype.card (IsFreeGroupoid.Generators G)

theorem GraphCoveringTheory.freeGroupoidGeneratorSet_card (G : Type u) [CategoryTheory.Groupoid G] [IsFreeGroupoid G] [CategoryTheory.IsConnected G] [Fintype (IsFreeGroupoid.Generators G)] [(a b : IsFreeGroupoid.Generators G) → Fintype (a ⟶ b)] (r : G) : Fintype.card ↑(freeGroupoidGeneratorSet G r) = Fintype.card (Quiver.Total (IsFreeGroupoid.Generators G)) + 1 - Fintype.card (IsFreeGroupoid.Generators G)

theorem GraphCoveringTheory.freeGroupoid_end_free_basis (G : Type u) [CategoryTheory.Groupoid G] [IsFreeGroupoid G] [CategoryTheory.IsConnected G] [Fintype (IsFreeGroupoid.Generators G)] [(a b : IsFreeGroupoid.Generators G) → Fintype (a ⟶ b)] (r : G) : Nonempty (FreeGroupBasis (Fin (Fintype.card (Quiver.Total (IsFreeGroupoid.Generators G)) + 1 - Fintype.card (IsFreeGroupoid.Generators G))) (CategoryTheory.End r))

theorem GraphCoveringTheory.freeGroupoid_end_free_rank (G : Type u) [CategoryTheory.Groupoid G] [IsFreeGroupoid G] [CategoryTheory.IsConnected G] [Fintype (IsFreeGroupoid.Generators G)] [(a b : IsFreeGroupoid.Generators G) → Fintype (a ⟶ b)] (r : G) : Nonempty (CategoryTheory.End r ≃* FreeGroup (Fin (Fintype.card (Quiver.Total (IsFreeGroupoid.Generators G)) + 1 - Fintype.card (IsFreeGroupoid.Generators G))))

theorem GraphCoveringTheory.schreier_basis_fintype (α : Type u) [Fintype α] (H : Subgroup (FreeGroup α)) [H.FiniteIndex] : Nonempty (FreeGroupBasis (Fin (H.index * Fintype.card α + 1 - H.index)) ↥H)

theorem GraphCoveringTheory.schreier_index_formula_fintype (α : Type u) [Fintype α] (H : Subgroup (FreeGroup α)) [H.FiniteIndex] : Nonempty (↥H ≃* FreeGroup (Fin (H.index * Fintype.card α + 1 - H.index)))

theorem GraphCoveringTheory.schreier_index_formula_nat (n : ℕ) (H : Subgroup (FreeGroup (Fin n))) [H.FiniteIndex] : Nonempty (↥H ≃* FreeGroup (Fin (H.index * n + 1 - H.index)))

theorem GraphCoveringTheory.schreier_basis_fintype_proved (α : Type u) [Fintype α] [Nonempty α] (H : Subgroup (FreeGroup α)) [H.FiniteIndex] : Nonempty (FreeGroupBasis (Fin (1 + H.index * (Fintype.card α - 1))) ↥H)

theorem GraphCoveringTheory.schreier_index_formula_fintype_proved (α : Type u) [Fintype α] [Nonempty α] (H : Subgroup (FreeGroup α)) [H.FiniteIndex] : Nonempty (↥H ≃* FreeGroup (Fin (1 + H.index * (Fintype.card α - 1))))

theorem GraphCoveringTheory.schreier_index_formula_proved (n : ℕ) (H : Subgroup (FreeGroup (Fin n))) [H.FiniteIndex] (hn : 0 < n) : Nonempty (↥H ≃* FreeGroup (Fin (1 + H.index * (n - 1))))