OAI/Topology/ArtinGroups/ParabolicIntersections/AmalgamAcyclic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The Bass--Serre coset graph is a tree: a cycle would be a nonempty reduced word in the amalgam equal to an element of the edge group.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.adj_representatives line 13
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.vertex_eq_iff line 18
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.base_le_factor line 22
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.vertex_eq_of_base line 26
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.other_endpoint_eq line 30
  6. theorem OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.acyclic line 43

    Source documentation

    No cycle is possible in the coset graph of an injective amalgam.

    theorem acyclic (hφ : ∀ b, Function.Injective (φ b)) : (graph φ).IsAcyclic := by
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.graph

  7. theorem OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.isTree line 95

    Source documentation

    The Bass--Serre tree of an injective two-factor amalgam.

    theorem isTree (hφ : ∀ b, Function.Injective (φ b)) : (graph φ).IsTree :=
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.graph