OAI/Topology/ArtinGroups/ParabolicIntersections/MeshMatrixAction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Evaluating complex path matrices in an arbitrary complex module.

  1. def OAI.HarmonicArtin.ParabolicIntersections.meshApply line 11
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.meshApply_sub line 15
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.meshApply_smul line 21
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.meshApply_mul line 27
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.meshApply_one line 39
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.meshApply_zero line 44
  7. lemma OAI.HarmonicArtin.ParabolicIntersections.meshApply_zero_right line 49
  8. lemma OAI.HarmonicArtin.ParabolicIntersections.meshApply_extend line 57

    Source documentation

    Extending a prefix matrix commutes with a linear last-edge operation.

    lemma meshApply_extend {m n : ℕ}
    (A : ∀ v, Matrix (MeshPaths G m v) (MeshPaths G n v) ℂ)
    (f : ∀ v, MeshPaths G m v → R) (v : V)
    (L : ∀ _u : {u : V // G.Adj u v}, R →ₗ[ℂ] R) :
    meshApply (meshExtendMatrix G A v)
      (fun p : MeshPaths G (m+1) v => L p.1 (f p.1.val p.2)) =
      fun q : MeshPaths G (n+1) v => L q.1 (meshApply (A q.1.val) (f q.1.val) q.2) := by
…

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