OAI/Topology/ArtinGroups/ParabolicIntersections/AcyclicTwist.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Discharging the acyclic-evaluation input by finite minimal reduction.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.minimal_scalar_exact_empty line 15
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.scalar_exact_empty_model line 34

    Source documentation

    An everywhere exact, one-color complex has an empty minimal model.

    lemma scalar_exact_empty_model {I : Type} [Fintype I] [DecidableEq I]
    (E : BasedComplex Q (K := ℂ) I) (α : V)
…
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.cone_empty_source_class line 50
  4. theorem OAI.HarmonicArtin.ParabolicIntersections.acyclic_twist_input line 59

    Source documentation

    The evaluation cone of an acyclic vertex test is homotopy equivalent to its target. This proves the Seidel--Thomas input in the actual model.

    theorem acyclic_twist_input : PublishedAcyclicTwist Q := by
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.PublishedAcyclicTwist