Kurosh Kernel

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

@[instance_reducible]

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

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

Equations

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

theorem GraphCoveringTheory.Kurosh.Internal.treeKuroshRootStabilizer_subsingleton {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (x : ↥(treeVertexStabilizer G H (rawBassSerreOrbitRoot G H))) : x = 1

theorem GraphCoveringTheory.Kurosh.Internal.treeKuroshProductToH_kernel {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (z : CoverSource G H) (hz : (treeKuroshProductToH G H) z = 1) : z = 1

theorem GraphCoveringTheory.Kurosh.Internal.treeDataGenerated_eq_top_for_kernel {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : treeDataGenerated G H = ⊤

theorem GraphCoveringTheory.Kurosh.Internal.treeKuroshProductToH_surjective_for_kernel {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : Function.Surjective ⇑(treeKuroshProductToH G H)

theorem GraphCoveringTheory.Kurosh.Internal.treeKuroshProductToH_injective {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : Function.Injective ⇑(treeKuroshProductToH G H)

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

The tree Kurosh decomposition, induced by the actual stabilizer inclusions.

Equations

• GraphCoveringTheory.Kurosh.treeKuroshProductMulEquivH G H = MulEquiv.ofBijective (GraphCoveringTheory.Kurosh.treeKuroshProductToH G H) ⋯

theorem GraphCoveringTheory.Kurosh.Internal.treeVertexStabilizer_central_or_factor {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (a : RawBassSerreOrbitVertex G H) : (∃ (g : FreeProduct G), rawTreeRepresentative G H a = RawBassSerreVertex.central g ∧ treeVertexStabilizer G H a = ⊥) ∨ ∃ (i : ι) (g : FreeProduct G), rawTreeRepresentative G H a = RawBassSerreVertex.factor i (factorCosetMk G i g) ∧ treeVertexStabilizer G H a = intersectionFactorInH H i g