AcyclicTwistInput.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The published acyclic-evaluation input

Seidel--Thomas, Braid group actions on derived categories of coherent sheaves, Duke Math. J. 108 (2001), Definition 2.5 (equation (2.2)), and the first sentence of the proof of Proposition 2.12: https://arxiv.org/pdf/math/0001043, pp. 13 and 17. A twist is the cone of evaluation. If the entire evaluated Hom complex is acyclic, this cone is isomorphic to the original object. For bounded projective complexes the resulting isomorphism is a homotopy equivalence. Below is precisely this standard consequence in the existing vertex-test notation. It is independent of the Artin stabilizer argument.

structure OAI.HarmonicArtin.ParabolicIntersections.PublishedAcyclicTwist line 23
theorem OAI.HarmonicArtin.ParabolicIntersections.pointed_standard_fixes_of_acyclic_tests line 37
Source documentation
Acyclic tests make every generator, and hence the entire standard parabolic, fix the actual pointed family.
```
theorem pointed_standard_fixes_of_acyclic_tests (hAcyclic : PublishedAcyclicTwist Q)
    (Y : Set S) (x : Artin M)
    (h : ∀ H, ∀ α ∈ Set.range (unfoldedInclusion M Y), ∀ l c,
      ClassTestExact Q α l c (pointedFamily M f x H))
    (g : Artin M) (hg : g ∈ artinParabolic M Y) :
    pointedFamily M f (g*x)=pointedFamily M f x := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.PublishedAcyclicTwist, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.unfoldedInclusion, OAI.HarmonicArtin.ParabolicIntersections.pointedFamily, OAI.HarmonicArtin.artinParabolic