OAI/Topology/ArtinGroups/ParabolicIntersections/AmalgamReduced.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.reduced_word_not_base line 14

   Source documentation

   The normal-form theorem, expressed using a list of actual factor elements.

   lemma reduced_word_not_base (hφ : ∀ b, Function.Injective (φ b))
       (w : List (Σ b, G b)) (hw : w≠[])
       (hchain : w.IsChain (fun a b => a.1≠b.1))
       (hred : ∀ a∈w, a.2∉(φ a.1).range) :
       (w.map (fun a => PushoutI.of (φ := φ) a.1 a.2)).prod∉(PushoutI.base φ).range := by
   …

2. lemma OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.transition_product line 30
3. theorem OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.transition_not_base line 42

   Source documentation

   Consecutive edges with distinct edge cosets give a nontrivial reduced word, provided their common vertex types alternate.

   theorem transition_not_base (hφ : ∀ b, Function.Injective (φ b))
       (e : ℕ → Amalgam φ) (b : ℕ → Bool) (n : ℕ) (hn : 0<n)
       (hfactor : ∀ i<n, (e i)⁻¹*e (i+1)∈Factor φ (b i))
       (hdistinct : ∀ i<n, (e i)⁻¹*e (i+1)∉(PushoutI.base φ).range)
       (halt : ∀ i, i+1<n → b i≠b (i+1)) :
       (e 0)⁻¹*e n∉(PushoutI.base φ).range := by
   …

   Mentions: OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.Amalgam, OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.Factor