OAI/Algebra/Finitistic/Bar/RecursiveSuffixEmbedding.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DerivedBar.ParityBridge.barSuffix line 25

   Source documentation

   Prefix one original categorical X bar to a linear suffix map.

   def barSuffix (V : ModuleCat.{u} D) (s i : ℕ)
       (e : V →ₗ[k] term k A N s) :
       ((XB).obj V).X i →ₗ[k] term k A N ((s+i)+1) :=
   …

   Mentions: OAI.DerivedBar.term

2. theorem OAI.DerivedBar.ParityBridge.barSuffix_smul line 32

   Source documentation

   The prefix keeps the original left D action.

   theorem barSuffix_smul (V : ModuleCat.{u} D) (s i : ℕ)
       (e : V →ₗ[k] term k A N s) (d : D) (v : ((XB).obj V).X i) :
       letI : Module A N := inflatedModule D X N
   …

   Mentions: OAI.DerivedBar.term, OAI.DerivedBar.ParityBridge.inflatedModule

3. theorem OAI.DerivedBar.ParityBridge.barSuffix_ideal_zero line 47
4. theorem OAI.DerivedBar.ParityBridge.barSuffix_map line 62

   Source documentation

   Naturality uses the original bar functor, including its supplied scalar coherence.

   theorem barSuffix_map (V W : ModuleCat.{u} D) (s i : ℕ)
       (e : W →ₗ[k] term k A N s) (f : V ⟶ W) (v : ((XB).obj V).X i) :
       barSuffix k D X N W s i e ((((XB).map f).f i).hom v) =
         barSuffix k D X N V s i (e.comp (f.hom.restrictScalars k)) v := by
   …

   Mentions: OAI.DerivedBar.term, OAI.DerivedBar.ParityBridge.barSuffix

5. def OAI.DerivedBar.ParityBridge.innerEmbedding line 78

   Source documentation

   Literal recursive suffix embedding on every summand, including zero input degrees.

   def innerEmbedding : (r n : ℕ) →
       RecursiveTotal.flat B Z r n →ₗ[k] term k A N (r+n)
     | 0, 0 => DirectSum.toModule k _ _ (fun _ => LinearMap.id)
     | 0, n+1 => 0
     | r+1, n => DirectSum.toModule k _ _ (fun t =>
         (termCast k D X N (show ((r+t.1.val.2)+t.1.val.1)+1=(r+1)+n by
           have h := t.1.property; omega)).comp
   …

   Mentions: OAI.DerivedBar.RecursiveTotal.flat, OAI.DerivedBar.term, OAI.DerivedBar.ParityBridge.termCast

6. theorem OAI.DerivedBar.ParityBridge.toModule_of_scalar line 90
7. theorem OAI.DerivedBar.ParityBridge.innerEmbedding_lof_succ line 97
8. theorem OAI.DerivedBar.ParityBridge.termCast_smul line 109
9. theorem OAI.DerivedBar.ParityBridge.innerEmbedding_smul line 116

   Source documentation

   The complete finite-sum suffix map has its original D action.

   theorem innerEmbedding_smul (r n : ℕ) (d : D) (v : RecursiveTotal.flat B Z r n) :
       letI : Module A N := inflatedModule D X N
   …

   Mentions: OAI.DerivedBar.RecursiveTotal.flat, OAI.DerivedBar.ParityBridge.inflatedModule

10. theorem OAI.DerivedBar.ParityBridge.innerEmbedding_ideal_zero line 145

    Source documentation

    Every recursive X-leading sum is killed by the square-zero ideal; the r=0 degree-zero input is killed by the specified inflation.

    theorem innerEmbedding_ideal_zero (r n : ℕ) (x : X) (v : RecursiveTotal.flat B Z r n) :
        letI : Module A N := inflatedModule D X N
    …

    Mentions: OAI.DerivedBar.RecursiveTotal.flat, OAI.DerivedBar.ParityBridge.inflatedModule