MultiHNN.lean`

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

def OAI.KaplanskyCounterexample.MultipleHNN.con line 16
abbrev OAI.KaplanskyCounterexample.MultipleHNN.Extension line 20
instance OAI.KaplanskyCounterexample.MultipleHNN.(instance at line 22) line 22
def OAI.KaplanskyCounterexample.MultipleHNN.of line 24
def OAI.KaplanskyCounterexample.MultipleHNN.letter line 26
lemma OAI.KaplanskyCounterexample.MultipleHNN.letter_mul_of line 28
def OAI.KaplanskyCounterexample.MultipleHNN.lift line 32
lemma OAI.KaplanskyCounterexample.MultipleHNN.lift_of line 38
lemma OAI.KaplanskyCounterexample.MultipleHNN.lift_letter line 44
theorem OAI.KaplanskyCounterexample.MultipleHNN.finite_partial_realization line 52
Source documentation
Extend any finite sublist of the required conjugacies one at a time. Mathlib's complete Britton-lemma proof supplies the embedding at each step.
```
theorem finite_partial_realization (S : Finset I) :
    ∃ (G : Type (max u v)) (_ : Group G) (f : H →* G),
      Function.Injective f ∧ ∃ t : I → G,
        ∀ i ∈ S, ∀ a : A i, t i * f a = f (φ i a) * t i := by
…
```
theorem OAI.KaplanskyCounterexample.MultipleHNN.of_injective line 81
theorem OAI.KaplanskyCounterexample.MultipleHNN.induction_on line 90
Source documentation
The presentation is generated by the base group and the stable letters.
```
theorem induction_on {P : Extension A B φ → Prop} (x : Extension A B φ)
    (hof : ∀ h, P (of A B φ h)) (ht : ∀ i, P (letter A B φ i))
    (hmul : ∀ x y, P x → P y → P (x * y)) (hinv : ∀ x, P x → P x⁻¹) : P x := by
…
```
Mentions: OAI.KaplanskyCounterexample.MultipleHNN.Extension, OAI.KaplanskyCounterexample.MultipleHNN.of, OAI.KaplanskyCounterexample.MultipleHNN.letter
theorem OAI.KaplanskyCounterexample.MultipleHNN.of_central line 105
Source documentation
A central base element fixed in every associated subgroup stays central.
```
theorem of_central (z : H) (hz : ∀ h : H, Commute h z)
    (ha : ∀ i, z ∈ A i) (hφ : ∀ i, (φ i ⟨z, ha i⟩ : H) = z) :
    ∀ x : Extension A B φ, Commute x (of A B φ z) := by
…
```
Mentions: OAI.KaplanskyCounterexample.MultipleHNN.Extension, OAI.KaplanskyCounterexample.MultipleHNN.of
instance OAI.KaplanskyCounterexample.MultipleHNN.(instance at line 119) line 119
Source documentation
Finite generation of the exact multiple-HNN presentation.
```
instance [Finite I] [Group.FG H] : Group.FG (Extension A B φ) := by
…
```
Mentions: OAI.KaplanskyCounterexample.MultipleHNN.Extension