OAI/AlgebraicTopology/Simplicial/Chains.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimplicialChains.Chains line 14
  2. def OAI.SimplicialChains.front line 16
  3. theorem OAI.SimplicialChains.front_single line 17
  4. def OAI.SimplicialChains.boundaryTerm line 20
  5. def OAI.SimplicialChains.boundary line 23
  6. theorem OAI.SimplicialChains.boundary_single line 24
  7. theorem OAI.SimplicialChains.boundaryTerm_nil line 26
  8. theorem OAI.SimplicialChains.boundaryTerm_cons line 27
  9. def OAI.SimplicialChains.includeVec line 30
  10. theorem OAI.SimplicialChains.includeVec_single line 32
  11. theorem OAI.SimplicialChains.map_ext_single line 40
  12. def OAI.SimplicialChains.Valid line 48
  13. def OAI.SimplicialChains.chains line 50
  14. structure OAI.SimplicialChains.Contraction line 54

    Source documentation

    An augmented chain contraction on the actual ordered cliques.

    structure Contraction where
…
  15. theorem OAI.SimplicialChains.valid_sublist line 63
  16. theorem OAI.SimplicialChains.includeVec_supported line 66
  17. structure OAI.SimplicialChains.TwoDimensionalIndices line 85

    Source documentation

    Explicit finite index data for vertices, edges and triangles. Every geometric field is an indexing identity, not an acyclicity assumption.

    structure TwoDimensionalIndices (E T : Type*) where
…
  18. def OAI.SimplicialChains.TwoDimensionalIndices.vList line 105
  19. def OAI.SimplicialChains.TwoDimensionalIndices.eList line 106
  20. def OAI.SimplicialChains.TwoDimensionalIndices.tList line 107
  21. def OAI.SimplicialChains.TwoDimensionalIndices.fillTerm line 112
  22. def OAI.SimplicialChains.TwoDimensionalIndices.fill line 118
  23. theorem OAI.SimplicialChains.TwoDimensionalIndices.fill_single line 120
  24. theorem OAI.SimplicialChains.TwoDimensionalIndices.fill_include_vertex line 123
  25. theorem OAI.SimplicialChains.TwoDimensionalIndices.fill_include_edge line 135
  26. theorem OAI.SimplicialChains.TwoDimensionalIndices.fill_include_triangle line 144
  27. theorem OAI.SimplicialChains.TwoDimensionalIndices.boundary_include_edge line 159
  28. theorem OAI.SimplicialChains.TwoDimensionalIndices.boundary_include_triangle line 169
  29. theorem OAI.SimplicialChains.TwoDimensionalIndices.fill_degree line 180
  30. theorem OAI.SimplicialChains.TwoDimensionalIndices.vertex_identity line 205
  31. theorem OAI.SimplicialChains.TwoDimensionalIndices.edge_identity line 213
  32. theorem OAI.SimplicialChains.TwoDimensionalIndices.triangle_identity line 227
  33. def OAI.SimplicialChains.TwoDimensionalIndices.contraction line 240

    Source documentation

    All finite matrix certificate equations are used to obtain a genuine augmented contraction of every actual clique of the graph.

    def contraction : Contraction L where
…

    Mentions: OAI.SimplicialChains.Contraction

  34. def OAI.SimplicialChains.reindex line 271
  35. theorem OAI.SimplicialChains.reindex_single line 273
  36. theorem OAI.SimplicialChains.reindex_front line 275
  37. theorem OAI.SimplicialChains.reindex_boundaryTerm line 282
  38. theorem OAI.SimplicialChains.reindex_boundary line 288
  39. theorem OAI.SimplicialChains.reindex_inverse line 295
  40. theorem OAI.SimplicialChains.reindex_degree line 303
  41. def OAI.SimplicialChains.Contraction.reindex line 315

    Source documentation

    Transport a genuine augmented contraction along a graph/order reindexing.

    def Contraction.reindex (K : Contraction L) (e : V ≃ W)
    (hf : ∀ w, Valid L w → Valid M (w.map e))
    (hb : ∀ w, Valid M w → Valid L (w.map e.symm)) : Contraction M where
…

    Mentions: OAI.SimplicialChains.Contraction, OAI.SimplicialChains.Valid