OAI/Algebra/Finitistic/Bar/RecursiveSuffixSums.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DerivedBar.ParityBridge.sum_hom_ext_scalar line 26

   Source documentation

   Finite coproduct extensionality also holds for k-linear maps out of a D bar.

   theorem sum_hom_ext_scalar {I : Type} [Finite I] [DecidableEq I]
       (V : I → ModuleCat.{u} D) (G : ModuleCat.{u} D ⥤ ModuleCat.{u} D) [G.Additive]
       (W : ModuleCat.{u} k)
       {f g : G.obj (ModuleCat.of D (⨁ t, V t)) →ₗ[k] W}
       (h : ∀ t, f.comp ((G.map (ModuleCat.ofHom (DirectSum.lof D I (fun t => V t) t))).hom.restrictScalars k) =
         g.comp ((G.map (ModuleCat.ofHom (DirectSum.lof D I (fun t => V t) t))).hom.restrictScalars k)) :
       f=g := by
   …

2. theorem OAI.DerivedBar.ParityBridge.innerEmbedding_sumDesc line 44

   Source documentation

   Suffix insertion commutes with the actual finite-sum distribution map appearing in the independently defined vertical differential.

   theorem innerEmbedding_sumDesc (r n i q : ℕ) (h : i+q=n)
       (v : (RecursiveTotal.degreeFunctor B r i).obj (RecursiveTotal.flat B Z r q)) :
       innerEmbedding k D X N (r+1) n
         ((RecursiveTotal.sumDesc (RecursiveTotal.summand B Z r q)
           (RecursiveTotal.degreeFunctor B r i)
           (fun t => RecursiveTotal.lof B Z (r+1) n ⟨⟨⟨i,q⟩,h⟩,t⟩)).hom v) =
       termCast k D X N (show ((r+q)+i)+1=(r+1)+n by omega)
         (barSuffix k D X N (RecursiveTotal.flat B Z r q) (r+q) i
           (innerEmbedding k D X N r q) v) := by
   …

   Mentions: OAI.DerivedBar.RecursiveTotal.degreeFunctor, OAI.DerivedBar.RecursiveTotal.flat, OAI.DerivedBar.ParityBridge.innerEmbedding, OAI.DerivedBar.RecursiveTotal.sumDesc, OAI.DerivedBar.RecursiveTotal.summand, OAI.DerivedBar.RecursiveTotal.lof, OAI.DerivedBar.ParityBridge.termCast, OAI.DerivedBar.ParityBridge.barSuffix