OAI/Topology/ArtinGroups/ParabolicIntersections/VisualNonVirtuallyCyclic.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Visual Artin splittings are not virtually cyclic. Powers of generators on opposite sides give nontrivial reduced commutators. This verifies the exception exclusion in the Minasyan--Osin amalgam criterion.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.visual_factor_not_base line 16
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.visual_opposite_powers_not_commute line 26
  3. theorem OAI.HarmonicArtin.ParabolicIntersections.visual_not_virtuallyCyclic line 57

    Source documentation

    A visual Artin splitting never gives the virtually cyclic exception.

    theorem visual_not_virtuallyCyclic : ¬Group.IsVirtuallyCyclic (Artin M) := by
…

    Mentions: OAI.HarmonicArtin.Artin