Deck transformations of a regular finite Schreier action

The finite coset action used in the index-formula proof has a second useful interpretation. Its automorphisms as a G-set are the deck transformations of the corresponding regular Schreier cover. This file proves the regular case directly: for a finite-index normal subgroup, right translation gives all deck transformations, so the deck group is the quotient group.

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

@[reducible, inline]

abbrev GraphCoveringTheory.SchreierAction (G : Type u) [Group G] (H : Subgroup G) [Fintype (G ⧸ H)] : Action FintypeCat G

The finite G-set underlying the Schreier cover of a subgroup H.

Equations

• GraphCoveringTheory.SchreierAction G H = Action.FintypeCat.ofMulAction G ↧(G ⧸ H)

@[reducible, inline]

abbrev GraphCoveringTheory.SchreierDeckGroup (G : Type u) [Group G] (H : Subgroup G) [Fintype (G ⧸ H)] : Type u

Automorphisms of the finite Schreier action, i.e. its deck transformations.

Equations

• GraphCoveringTheory.SchreierDeckGroup G H = CategoryTheory.Aut (GraphCoveringTheory.SchreierAction G H)

noncomputable def GraphCoveringTheory.quotientDeckEndHom (G : Type u) [Group G] (H : Subgroup G) [H.Normal] [Fintype (G ⧸ H)] : G ⧸ H →* CategoryTheory.End (SchreierAction G H)

The quotient acts on its coset space by the right translations induced from G.

Equations

• GraphCoveringTheory.quotientDeckEndHom G H = QuotientGroup.lift H (Action.FintypeCat.toEndHom H) ⋯

@[simp]

theorem GraphCoveringTheory.quotientDeckEndHom_mk (G : Type u) [Group G] (H : Subgroup G) [H.Normal] [Fintype (G ⧸ H)] (g h : G) : (CategoryTheory.ConcreteCategory.hom ((quotientDeckEndHom G H) ↑g).hom) ⟦h⟧ = ⟦h * g⁻¹⟧

@[simp]

theorem GraphCoveringTheory.quotientDeckEndHom_apply_one (G : Type u) [Group G] (H : Subgroup G) [H.Normal] [Fintype (G ⧸ H)] (q : G ⧸ H) : (CategoryTheory.ConcreteCategory.hom ((quotientDeckEndHom G H) q).hom) 1 = q⁻¹

noncomputable def GraphCoveringTheory.quotientDeckUnitsHom (G : Type u) [Group G] (H : Subgroup G) [H.Normal] [Fintype (G ⧸ H)] : G ⧸ H →* (CategoryTheory.End (SchreierAction G H))ˣ

Right translations by inverse quotient elements, viewed as invertible equivariant endomorphisms.

Equations

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

The Aut/Units conversion is only packaging: the underlying action map is still the explicit right-translation endomorphism above.

noncomputable def GraphCoveringTheory.quotientDeckHom (G : Type u) [Group G] (H : Subgroup G) [H.Normal] [Fintype (G ⧸ H)] : G ⧸ H →* SchreierDeckGroup G H

The homomorphism from the quotient group to automorphisms of its Schreier action.

Equations

• GraphCoveringTheory.quotientDeckHom G H = (CategoryTheory.Aut.unitsEndEquivAut (GraphCoveringTheory.SchreierAction G H)).toMonoidHom.comp (GraphCoveringTheory.quotientDeckUnitsHom G H)

theorem GraphCoveringTheory.quotientDeckHom_hom (G : Type u) [Group G] (H : Subgroup G) [H.Normal] [Fintype (G ⧸ H)] (q : G ⧸ H) : ((quotientDeckHom G H) q).hom.hom = ((quotientDeckEndHom G H) q).hom

@[simp]

theorem GraphCoveringTheory.quotientDeckHom_apply_one (G : Type u) [Group G] (H : Subgroup G) [H.Normal] [Fintype (G ⧸ H)] (q : G ⧸ H) : (CategoryTheory.ConcreteCategory.hom ((quotientDeckHom G H) q).hom.hom) 1 = q⁻¹

theorem GraphCoveringTheory.quotientDeckHom_injective (G : Type u) [Group G] (H : Subgroup G) [H.Normal] [Fintype (G ⧸ H)] : Function.Injective ⇑(quotientDeckHom G H)

theorem GraphCoveringTheory.quotientDeckHom_surjective (G : Type u) [Group G] (H : Subgroup G) [H.Normal] [Fintype (G ⧸ H)] : Function.Surjective ⇑(quotientDeckHom G H)

noncomputable def GraphCoveringTheory.quotientDeckGroupEquiv (G : Type u) [Group G] (H : Subgroup G) [H.Normal] [Fintype (G ⧸ H)] : G ⧸ H ≃* SchreierDeckGroup G H

The deck group of a finite regular Schreier cover is its quotient group.

Equations

• GraphCoveringTheory.quotientDeckGroupEquiv G H = MulEquiv.ofBijective (GraphCoveringTheory.quotientDeckHom G H) ⋯

noncomputable def GraphCoveringTheory.finiteIndexQuotientDeckGroupEquiv (G : Type u) [Group G] (H : Subgroup G) [H.Normal] [H.FiniteIndex] : G ⧸ H ≃* SchreierDeckGroup G H

The same deck-group identification stated with Mathlib's finite-index class.

Equations

• GraphCoveringTheory.finiteIndexQuotientDeckGroupEquiv G H = GraphCoveringTheory.quotientDeckGroupEquiv G H