Theorems · Definition · group theory

HNNExtension

(G : Type u_1) → [inst : Group G] → (A B : Subgroup G) → ↥A ≃* ↥B → Type u_1

The HNN Extension of a group G, HNNExtension G A B φ. Given a group G, subgroups A and B and an isomorphism φ of A and B, we adjoin a letter t to G, such that for any a ∈ A, the conjugate of of a by t is of (φ a), where of is the canonical map from G into the HNNExtension.

Defined in

Mathlib.GroupTheory.HNNExtension

Cited by

26 results in Mathlib

Foundations

Depth 49 from the axioms · uses propext, Quot.sound

Assumes

Group