OAI/Algebra/Finitistic/Bar/RecursiveTotalFlatten.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DerivedBar.RecursiveTotal.Diagonal line 13
2. def OAI.DerivedBar.RecursiveTotal.Index line 16

   Source documentation

   Every index records every bar length and the final input degree.

   def Index : ℕ → ℕ → Type
     | 0, _ => Unit
     | r+1, n => (p : Diagonal n) × Index r p.val.2

   Mentions: OAI.DerivedBar.RecursiveTotal.Diagonal

3. instance OAI.DerivedBar.RecursiveTotal.indexFinite line 20
4. abbrev OAI.DerivedBar.RecursiveTotal.degreeFunctor line 33
5. def OAI.DerivedBar.RecursiveTotal.bicomplex line 38
6. def OAI.DerivedBar.RecursiveTotal.iter line 43

   Source documentation

   Successively totalize the given module-to-chain functors.

   def iter : ℕ → ChainComplex (ModuleCat.{u} D) ℕ
     | 0 => Z
     | r+1 => (bicomplex B r (iter r)).total c
   
   /-- Literal nested terms, before any coproducts are taken. -/

   Mentions: OAI.DerivedBar.RecursiveTotal.bicomplex

7. def OAI.DerivedBar.RecursiveTotal.summand line 48

   Source documentation

   Literal nested terms, before any coproducts are taken.

   def summand : (r n : ℕ) → Index r n → ModuleCat.{u} D
     | 0, n, _ => Z.X n
     | r+1, _, ⟨p,t⟩ => (degreeFunctor B r p.val.1).obj (summand r p.val.2 t)
   
   /-- Insert a literal nested term into the actual recursive total. -/

   Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.degreeFunctor, OAI.DerivedBar.term

8. def OAI.DerivedBar.RecursiveTotal.inclusion line 53

   Source documentation

   Insert a literal nested term into the actual recursive total.

   def inclusion : (r n : ℕ) → (t : Index r n) → summand B Z r n t ⟶ (iter B Z r).X n
     | 0, _, _ => 𝟙 _
     | r+1, n, ⟨p,t⟩ =>
       (degreeFunctor B r p.val.1).map (inclusion r p.val.2 t) ≫
         (bicomplex B r (iter B Z r)).ιTotal c p.val.1 p.val.2 n p.property
   
   /-- A map out of an additive image of the recursive total is specified on all
   literal nested terms. Only finite diagonal coproducts are distributed. -/

   Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.summand, OAI.DerivedBar.RecursiveTotal.iter, OAI.DerivedBar.RecursiveTotal.degreeFunctor, OAI.DerivedBar.RecursiveTotal.bicomplex

9. def OAI.DerivedBar.RecursiveTotal.desc line 61

   Source documentation

   A map out of an additive image of the recursive total is specified on all literal nested terms. Only finite diagonal coproducts are distributed.

   def desc : (r : ℕ) → (G : ModuleCat.{u} D ⥤ ModuleCat.{u} D) → [G.Additive] →
       {n : ℕ} → {Y : ModuleCat.{u} D} →
       (∀ t : Index r n, G.obj (summand B Z r n t) ⟶ Y) →
       (G.obj ((iter B Z r).X n) ⟶ Y)
     | 0, _, _, _, _, f => f ()
     | r+1, G, _, _, _, f => totalMapDesc G (bicomplex B r (iter B Z r))
         (fun i q h => desc r (degreeFunctor B r i ⋙ G) (fun t => f ⟨⟨⟨i,q⟩,h⟩,t⟩))
   
   @[reassoc (attr := simp)]

   Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.summand, OAI.DerivedBar.RecursiveTotal.iter, OAI.DerivedBar.totalMapDesc, OAI.DerivedBar.RecursiveTotal.bicomplex, OAI.DerivedBar.RecursiveTotal.degreeFunctor

10. theorem OAI.DerivedBar.RecursiveTotal.inclusion_desc line 70
11. theorem OAI.DerivedBar.RecursiveTotal.hom_ext line 85
12. def OAI.DerivedBar.RecursiveTotal.flattenIso line 108

    Source documentation

    Actual degreewise flattening into an ordinary direct sum of nested tensors. The universal property is proved for the recursive totals, not assumed.

    def flattenIso (r n : ℕ) (G : ModuleCat.{u} D ⥤ ModuleCat.{u} D) [G.Additive] :
        G.obj ((iter B Z r).X n) ≅
          ModuleCat.of D (⨁ t : Index r n, G.obj (summand B Z r n t)) where
    …

    Mentions: OAI.DerivedBar.RecursiveTotal.iter, OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.summand