OAI/Algebra/Finitistic/Bar/RecursiveBlockIndex.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DerivedBar.RecursiveTotal.blocks line 11

   Source documentation

   Recursive total diagonals record exactly r+1 block lengths; the final input degree is the last block length.

   def blocks (r : ℕ) : {n : ℕ} → Index r n → Blocks r := by
   …

   Mentions: OAI.DerivedBar.RecursiveTotal.Index

2. theorem OAI.DerivedBar.RecursiveTotal.total_blocks line 16
3. def OAI.DerivedBar.RecursiveTotal.indexOfBlocks line 26

   Source documentation

   Recover the successive diagonal choices from the literal block lengths.

   def indexOfBlocks : (r : ℕ) → (b : Blocks r) → Index r (total r b)
     | 0, _ => ()
     | r+1, (i,b) => ⟨⟨⟨i,total r b⟩,rfl⟩,indexOfBlocks r b⟩

   Mentions: OAI.DerivedBar.RecursiveTotal.Index

4. def OAI.DerivedBar.RecursiveTotal.castIndex line 30
5. theorem OAI.DerivedBar.RecursiveTotal.blocks_castIndex line 32
6. theorem OAI.DerivedBar.RecursiveTotal.blocks_indexOfBlocks line 35
7. theorem OAI.DerivedBar.RecursiveTotal.blocks_injective line 44
8. def OAI.DerivedBar.RecursiveTotal.blockIndexEquiv line 60

   Source documentation

   Actual equivalence used to flatten the recursively nested finite diagonals.

   def blockIndexEquiv (r n : ℕ) : Index r n ≃ {b : Blocks r // total r b=n} where
   …

   Mentions: OAI.DerivedBar.RecursiveTotal.Index

9. def OAI.DerivedBar.RecursiveTotal.shapeIndexEquiv line 67

   Source documentation

   The recursive total index is exactly the manuscript's full-degree D/X shape.

   def shapeIndexEquiv (r n : ℕ) : Index r n ≃ Multibar.Indexed.Shape (r+n) r :=
   …

   Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.Multibar.Indexed.Shape