Kurosh Active

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

@[instance_reducible]

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

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

Equations

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

@[reducible, inline]

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

Quotient vertices whose chosen representatives have nontrivial stabilizers.

Equations

• GraphCoveringTheory.Kurosh.KuroshActiveVertexIndex G H = { a : GraphCoveringTheory.Kurosh.RawBassSerreOrbitVertex G H // GraphCoveringTheory.Kurosh.treeVertexStabilizer G H a ≠ ⊥ }

@[reducible, inline]

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

Nontrivial stabilizer indices together with the free-part index.

Equations

• GraphCoveringTheory.Kurosh.KuroshActiveComponentIndex G H = (GraphCoveringTheory.Kurosh.KuroshActiveVertexIndex G H ⊕ PUnit.{?u.1 + 1})

def GraphCoveringTheory.Kurosh.KuroshActiveComponent {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : KuroshActiveComponentIndex G H → Type (max (u + 1) (v + 1))

The nontrivial vertex stabilizers together with the free part.

Equations

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

@[instance_reducible]

noncomputable instance GraphCoveringTheory.Kurosh.kuroshActiveComponentGroup {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (q : KuroshActiveComponentIndex G H) : Group (KuroshActiveComponent G H q)

Equations

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

@[reducible, inline]

abbrev GraphCoveringTheory.Kurosh.KuroshActiveProduct {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : Type (max (max (max u v) u_1) (u + 1) (v + 1))

The Kurosh free product after omitting trivial vertex stabilizers.

Equations

• GraphCoveringTheory.Kurosh.KuroshActiveProduct G H = GraphCoveringTheory.Kurosh.FreeProduct (GraphCoveringTheory.Kurosh.KuroshActiveComponent G H)

noncomputable def GraphCoveringTheory.Kurosh.treeVertexComponentToActive {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (a : RawBassSerreOrbitVertex G H) : TreeKuroshComponent G H (Sum.inl a) →* KuroshActiveProduct G H

Include a nontrivial stabilizer in the active product, collapsing trivial ones.

Equations

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

noncomputable def GraphCoveringTheory.Kurosh.activeVertexComponentToTree {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (j : KuroshActiveVertexIndex G H) : KuroshActiveComponent G H (Sum.inl j) →* TreeKuroshProduct G H

Include an active vertex stabilizer in the product of all components.

Equations

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

noncomputable def GraphCoveringTheory.Kurosh.treeFreeComponentToActive {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : TreeKuroshComponent G H (Sum.inr PUnit.unit) →* KuroshActiveProduct G H

Include the free component in the active product.

Equations

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

noncomputable def GraphCoveringTheory.Kurosh.activeFreeComponentToTree {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : KuroshActiveComponent G H (Sum.inr PUnit.unit) →* TreeKuroshProduct G H

Include the active free component in the product of all components.

Equations

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

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

Map every tree component to the product with trivial stabilizers removed.

Equations

• GraphCoveringTheory.Kurosh.treeComponentToActive G H (Sum.inl a) = GraphCoveringTheory.Kurosh.treeVertexComponentToActive G H a
• GraphCoveringTheory.Kurosh.treeComponentToActive G H (Sum.inr val) = GraphCoveringTheory.Kurosh.treeFreeComponentToActive G H

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

Map an active component back into the product of all tree components.

Equations

• GraphCoveringTheory.Kurosh.activeComponentToTree G H (Sum.inl j) = GraphCoveringTheory.Kurosh.activeVertexComponentToTree G H j
• GraphCoveringTheory.Kurosh.activeComponentToTree G H (Sum.inr val) = GraphCoveringTheory.Kurosh.activeFreeComponentToTree G H

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

The homomorphism that removes trivial stabilizer factors.

Equations

• GraphCoveringTheory.Kurosh.treeProductToActive G H = Monoid.CoprodI.lift (GraphCoveringTheory.Kurosh.treeComponentToActive G H)

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

The homomorphism reinserting the active factors into the full tree product.

Equations

• GraphCoveringTheory.Kurosh.activeProductToTree G H = Monoid.CoprodI.lift (GraphCoveringTheory.Kurosh.activeComponentToTree G H)

theorem GraphCoveringTheory.Kurosh.Internal.activeProductToTree_comp_treeProductToActive {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : (activeProductToTree G H).comp (treeProductToActive G H) = MonoidHom.id (TreeKuroshProduct G H)

theorem GraphCoveringTheory.Kurosh.Internal.treeProductToActive_comp_activeProductToTree {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : (treeProductToActive G H).comp (activeProductToTree G H) = MonoidHom.id (KuroshActiveProduct G H)

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

Removing trivial stabilizer factors preserves the Kurosh product up to isomorphism.

Equations

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

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

The factor-only Kurosh product is isomorphic to the subgroup.

Equations

• GraphCoveringTheory.Kurosh.kuroshActiveEquivH G H = (GraphCoveringTheory.Kurosh.treeProductActiveEquiv G H).symm.trans (GraphCoveringTheory.Kurosh.treeKuroshProductMulEquivH G H)

theorem GraphCoveringTheory.Kurosh.kurosh_active_vertex_intersection {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (j : KuroshActiveVertexIndex G H) : ∃ (i : ι) (g : FreeProduct G), treeVertexStabilizer G H ↑j = intersectionFactorInH H i g