Kurosh Free Corollary

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

@[instance_reducible]

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

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

Equations

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

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

Kill every stabilizer component and retain the free component.

Equations

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

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

The projection of the tree Kurosh product onto its free component.

Equations

• GraphCoveringTheory.Kurosh.treeKuroshProductToFreePart G H = id (Monoid.CoprodI.lift (GraphCoveringTheory.Kurosh.treeKuroshComponentToFreePart G H))

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

@[simp]

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

theorem GraphCoveringTheory.Kurosh.treeKuroshProductToH_factor_through_freePart {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (htriv : ∀ (a : RawBassSerreOrbitVertex G H), Subsingleton ↥(treeVertexStabilizer G H a)) : treeKuroshProductToH G H = (kuroshFreePartHom G H).comp (treeKuroshProductToFreePart G H)

theorem GraphCoveringTheory.Kurosh.kuroshFreePartHom_surjective_of_trivial_stabilizers {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (htriv : ∀ (a : RawBassSerreOrbitVertex G H), Subsingleton ↥(treeVertexStabilizer G H a)) : Function.Surjective ⇑(kuroshFreePartHom G H)

noncomputable def GraphCoveringTheory.Kurosh.kuroshFreePartEquivOfTrivialStabilizers {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (htriv : ∀ (a : RawBassSerreOrbitVertex G H), Subsingleton ↥(treeVertexStabilizer G H a)) : KuroshFreePart G H ≃* ↥H

When all vertex stabilizers are trivial, free-part evaluation is an isomorphism onto H.

Equations

• GraphCoveringTheory.Kurosh.kuroshFreePartEquivOfTrivialStabilizers G H htriv = MulEquiv.ofBijective (GraphCoveringTheory.Kurosh.kuroshFreePartHom G H) ⋯

theorem GraphCoveringTheory.Kurosh.kurosh_subgroup_is_free_of_trivial_stabilizers {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (htriv : ∀ (a : RawBassSerreOrbitVertex G H), Subsingleton ↥(treeVertexStabilizer G H a)) : IsFreeGroup ↥H