PositiveHeadProduct.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The greedy head of a product with a simple left factor.

theorem OAI.HarmonicArtin.ParabolicIntersections.positive_head_product line 15

Source documentation

If h is the greatest simple prefix of b, the greatest simple prefix of a*b is a*g, where g is the gcd of the complement of a and h. This is the local normal-form step used in folding.

theorem positive_head_product
    (cancel : ∀ a b c : PositiveArtin M, a*b=a*c → b=c)
    (z : M.Group) (hz : ∀ w, M.toCoxeterSystem.length w ≤ M.toCoxeterSystem.length z)
    (a h g : M.Group) (b : PositiveArtin M)
    (hh : PositivePrefix M (positiveSimpleLift M h) b)
    (hhead : ∀ w, PositivePrefix M (positiveSimpleLift M w) b →
      PositivePrefix M (positiveSimpleLift M w) (positiveSimpleLift M h))
    (hgc : PositivePrefix M (positiveSimpleLift M g) (positiveSimpleLift M (a⁻¹*z)))
    (hgh : PositivePrefix M (positiveSimpleLift M g) (positiveSimpleLift M h))
    (hgreat : ∀ e, PositivePrefix M e (positiveSimpleLift M (a⁻¹*z)) →
      PositivePrefix M e (positiveSimpleLift M h) → PositivePrefix M e (positiveSimpleLift M g)) :
    ∃ k : M.Group, positiveSimpleLift M k=positiveSimpleLift M a*positiveSimpleLift M g ∧
…

Mentions: OAI.HarmonicArtin.PositiveArtin, OAI.HarmonicArtin.PositivePrefix, OAI.HarmonicArtin.positiveSimpleLift