OAI/Topology/ArtinGroups/ParabolicIntersections/MeshNaturality.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A prefix operator commutes with contraction of the final backtrack.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.meshContraction_insert line 10
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.meshContraction_no_return line 29
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.meshExtend_twice_insert line 43
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.meshExtend_twice_no_return line 63
  5. theorem OAI.HarmonicArtin.ParabolicIntersections.meshContraction_naturality line 85

    Source documentation

    No property of the prefix operator is needed: the final pair is disjoint from it, so contraction is natural for every endpoint family.

    theorem meshContraction_naturality (μ : V → ℝ) {m n : ℕ}
    (A : ∀ v, Matrix (MeshPaths G m v) (MeshPaths G n v) ℂ) (v : V) :
    meshContractionMatrix G μ m v * meshExtendMatrix G (meshExtendMatrix G A) v =
      A v * meshContractionMatrix G μ n v := by
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.MeshPaths, OAI.HarmonicArtin.ParabolicIntersections.meshContractionMatrix, OAI.HarmonicArtin.ParabolicIntersections.meshExtendMatrix

  6. theorem OAI.HarmonicArtin.ParabolicIntersections.meshContraction_adjacent_right line 112
  7. theorem OAI.HarmonicArtin.ParabolicIntersections.meshContraction_naturality_adjoint line 120