OAI/Topology/ArtinGroups/ParabolicIntersections/SphericalCochain.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The ordinary cochain bound in Lemma 7.2 of paper 082-03.

  1. def OAI.HarmonicArtin.ParabolicIntersections.ClassTestCochainUpper line 15

    Source documentation

    Unlike ClassTestUpper, this bounds ordinary cochain degree, uniformly in total degree.

    def ClassTestCochainUpper (x : FiniteHomotopyClass Q (K := K)) (U : Set V) (m : ℤ) : Prop :=
…
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.classTestCochainUpper_mono line 18
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.classTestCochainUpper_positive line 23
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.positiveWord_cochain_bounds line 35
  5. theorem OAI.HarmonicArtin.ParabolicIntersections.positiveWord_complete_cochain_drop line 58

    Source documentation

    A pass containing every operated vertex lowers the ordinary cochain bound by one. This is proved from the actual twist test formulas.

    theorem positiveWord_complete_cochain_drop (hn : ∀ a, Q.source a ≠ Q.target a)
    (w : List V) (x : FiniteHomotopyClass Q (K := K)) (U : Set V)
…
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.scalarExact_of_absent_cochain line 66
  7. theorem OAI.HarmonicArtin.ParabolicIntersections.classTestCochainUpper_exists line 77

    Source documentation

    Every bounded family admits an ordinary cochain upper bound.

    theorem classTestCochainUpper_exists (x : FiniteHomotopyClass Q (K := K)) (U : Set V) :
…