OAI/CategoryTheory/Thomason/Chains/NormalizedTuples.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Thomason.Construction.SimplexComplex.mapBasis_congr line 21

   Source documentation

   The image chain depends only on the composite vertex function.

   theorem mapBasis_congr {m n p : ℕ} (f : Fin (m + 1) →o Fin (n + 1))
       (s t : Basis m p) (h : ∀ i, f (s i) = f (t i)) :
       mapBasis f p s = mapBasis f p t := by
   …

   Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.mapBasis

2. theorem OAI.Thomason.Construction.SimplexComplex.mapBasis_delete_strict line 28

   Source documentation

   A nondegenerate image commutes with deleting a vertex.

   theorem mapBasis_delete_strict {m n p : ℕ} (f : Fin (m + 1) →o Fin (n + 1))
       (s : Basis m (p + 1)) (hf : StrictMono (fun i => f (s i))) (i : Fin (p + 2)) :
       mapBasis f p (deleteVertex s i) =
         Finsupp.single (deleteVertex (OrderEmbedding.ofStrictMono _ hf) i) 1 := by
   …

   Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.mapBasis, OAI.Thomason.Construction.SimplexComplex.deleteVertex

3. theorem OAI.Thomason.Construction.SimplexComplex.mapBasis_delete_equal line 38

   Source documentation

   Deleting either member of an adjacent equal pair gives the same image.

   theorem mapBasis_delete_equal {m n p : ℕ} (f : Fin (m + 1) →o Fin (n + 1))
       (s : Basis m (p + 1)) (i : Fin (p + 1)) (hi : f (s i.castSucc) = f (s i.succ)) :
       mapBasis f p (deleteVertex s i.castSucc) =
         mapBasis f p (deleteVertex s i.succ) := by
   …

   Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.mapBasis, OAI.Thomason.Construction.SimplexComplex.deleteVertex

4. theorem OAI.Thomason.Construction.SimplexComplex.mapBasis_delete_vanish line 53

   Source documentation

   A face which retains an equal pair has zero normalized image.

   theorem mapBasis_delete_vanish {m n p : ℕ} (f : Fin (m + 1) →o Fin (n + 1))
       (s : Basis m (p + 1)) (i : Fin (p + 1)) (hi : f (s i.castSucc) = f (s i.succ))
       (j : Fin (p + 2)) (hja : j ≠ i.castSucc) (hjb : j ≠ i.succ) :
       mapBasis f p (deleteVertex s j) = 0 := by
   …

   Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.mapBasis, OAI.Thomason.Construction.SimplexComplex.deleteVertex

5. theorem OAI.Thomason.Construction.SimplexComplex.exists_adjacent_equal line 70

   Source documentation

   Any degenerate monotone image has an adjacent equal pair.

   theorem exists_adjacent_equal {m n p : ℕ} (f : Fin (m + 1) →o Fin (n + 1))
       (s : Basis m (p + 1)) (hf : ¬StrictMono (fun i => f (s i))) :
       ∃ i : Fin (p + 1), f (s i.castSucc) = f (s i.succ) := by
   …

   Mentions: OAI.Thomason.Construction.SimplexComplex.Basis

6. theorem OAI.Thomason.Construction.SimplexComplex.differential_mapBasis line 80

   Source documentation

   Naturality on one nondegenerate source simplex, including degenerate images.

   theorem differential_mapBasis {m n p : ℕ} (f : Fin (m + 1) →o Fin (n + 1))
       (s : Basis m (p + 1)) :
       mapChains f p (differentialBasis m p s) = differential n p (mapBasis f (p + 1) s) := by
   …

   Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.mapChains, OAI.Thomason.Construction.SimplexComplex.differentialBasis, OAI.Thomason.Construction.SimplexComplex.differential, OAI.Thomason.Construction.SimplexComplex.mapBasis

7. theorem OAI.Thomason.Construction.SimplexComplex.boundaryNaturality line 111

   Source documentation

   The concrete normalized differential is natural under every monotone map.

   theorem boundaryNaturality {m n : ℕ} (f : Fin (m + 1) →o Fin (n + 1)) :
       BoundaryNaturality f := by
   …

   Mentions: OAI.Thomason.Construction.SimplexComplex.BoundaryNaturality

8. theorem OAI.Thomason.Construction.normalizedSimplexIdentities line 122

   Source documentation

   The normalized simplex differential squares to zero and is natural.

   theorem normalizedSimplexIdentities : NormalizedSimplexIdentities where
   …

   Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities

9. def OAI.Thomason.Construction.SimplexComplex.top line 145

   Source documentation

   The top basis simplex on its own set of vertices.

   def top (p : ℕ) : Basis p p := (OrderIso.refl _).toOrderEmbedding

   Mentions: OAI.Thomason.Construction.SimplexComplex.Basis

10. def OAI.Thomason.Construction.SimplexComplex.tuple line 148

    Source documentation

    The normalized chain represented by a weakly increasing tuple.

    noncomputable def tuple {n p : ℕ} (f : Fin (p + 1) →o Fin (n + 1)) : Chains n p :=
    …

    Mentions: OAI.Thomason.Construction.SimplexComplex.Chains

11. def OAI.Thomason.Construction.SimplexComplex.deleteTuple line 152

    Source documentation

    Delete one entry of a weakly increasing tuple.

    def deleteTuple {n p : ℕ} (f : Fin (p + 2) →o Fin (n + 1)) (i : Fin (p + 2)) :
        Fin (p + 1) →o Fin (n + 1) := f.comp (Fin.succAboveOrderEmb i).toOrderHom

12. theorem OAI.Thomason.Construction.SimplexComplex.mapBasis_eq_tuple line 155
13. theorem OAI.Thomason.Construction.SimplexComplex.mapChains_tuple line 159

    Source documentation

    Composition acts on normalized tuples, including zero/degenerate tuples.

    theorem mapChains_tuple {m n p : ℕ} (f : Fin (p + 1) →o Fin (m + 1))
        (g : Fin (m + 1) →o Fin (n + 1)) :
        mapChains g p (tuple f) = tuple (g.comp f) := mapBasis_comp f g (top p)

    Mentions: OAI.Thomason.Construction.SimplexComplex.mapChains, OAI.Thomason.Construction.SimplexComplex.tuple, OAI.Thomason.Construction.SimplexComplex.mapBasis_comp, OAI.Thomason.Construction.SimplexComplex.top

14. theorem OAI.Thomason.Construction.SimplexComplex.differential_tuple line 165

    Source documentation

    The usual alternating boundary formula remains valid for every monotone list. This includes degenerate lists, for which the nonzero faces cancel.

    theorem differential_tuple (h : NormalizedSimplexIdentities) {n p : ℕ}
        (f : Fin (p + 2) →o Fin (n + 1)) :
        differential n p (tuple f) =
          ∑ i : Fin (p + 2), ((-1 : ℤ) ^ (i : ℕ)) • tuple (deleteTuple f i) := by
    …

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.differential, OAI.Thomason.Construction.SimplexComplex.tuple, OAI.Thomason.Construction.SimplexComplex.deleteTuple

15. theorem OAI.Thomason.Construction.SimplexComplex.tuple_eq_zero_of_repeat line 177

    Source documentation

    A tuple with two specified equal entries is zero in normalized chains.

    theorem tuple_eq_zero_of_repeat {n p : ℕ} (f : Fin (p + 1) →o Fin (n + 1))
        {i j : Fin (p + 1)} (hij : i < j) (he : f i = f j) : tuple f = 0 := by
    …

    Mentions: OAI.Thomason.Construction.SimplexComplex.tuple

16. theorem OAI.Thomason.Construction.SimplexComplex.tuple_nonneg line 186
17. def OAI.Thomason.Construction.SimplexComplex.append line 190

    Source documentation

    Append one upper vertex to a monotone tuple.

    def append {n p : ℕ} (f : Fin (p + 1) →o Fin (n + 1)) (b : Fin (n + 1))
        (hb : f (Fin.last p) ≤ b) : Fin (p + 2) →o Fin (n + 1) where
    …

18. theorem OAI.Thomason.Construction.SimplexComplex.append_castSucc line 197
19. theorem OAI.Thomason.Construction.SimplexComplex.append_last line 203
20. def OAI.Thomason.Construction.SimplexComplex.initial line 208
21. theorem OAI.Thomason.Construction.SimplexComplex.initial_apply line 212
22. theorem OAI.Thomason.Construction.SimplexComplex.append_initial line 215
23. theorem OAI.Thomason.Construction.SimplexComplex.tuple_append_eq_zero line 225

    Source documentation

    Appending a repeated final vertex gives the zero normalized chain.

    theorem tuple_append_eq_zero {n p : ℕ} (f : Fin (p + 1) →o Fin (n + 1)) (b) (hb)
        (he : f (Fin.last p) = b) : tuple (append f b hb) = 0 := by
    …

    Mentions: OAI.Thomason.Construction.SimplexComplex.tuple, OAI.Thomason.Construction.SimplexComplex.append

24. theorem OAI.Thomason.Construction.SimplexComplex.delete_append_last line 230
25. theorem OAI.Thomason.Construction.SimplexComplex.delete_append_castSucc line 238
26. theorem OAI.Thomason.Construction.SimplexComplex.prism_last_face_cancel line 257

    Source documentation

    The two exceptional faces in the relative prism cancel to the target endpoint. The alternatives express exactly the old-initial/new-tail split.

    theorem prism_last_face_cancel {n p : ℕ}
        (f g : Fin (p + 2) →o Fin (n + 1)) (hfg : ∀ i, f i ≤ g i)
        (hcases : (∀ i : Fin (p + 1), f i.castSucc = g i.castSucc) ∨
          g (Fin.last (p + 1)) = g (Fin.last p).castSucc) :
        tuple (append (initial f) (g (Fin.last (p + 1)))
          ((hfg _).trans (g.monotone (Fin.le_last _)))) -
        tuple (append (initial f) (g (Fin.last p).castSucc) (hfg _)) = tuple g := by
    …

    Mentions: OAI.Thomason.Construction.SimplexComplex.tuple, OAI.Thomason.Construction.SimplexComplex.append, OAI.Thomason.Construction.SimplexComplex.initial