OAI/Algebra/Finitistic/Bar/SupportedOuterCoordinates.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DerivedBar.ParityBridge.outerEmbed_freeBarPatternIso line 32

   Source documentation

   The projected exterior coefficient remains D while the internal word uses exactly the old literal pattern embedding.

   theorem outerEmbed_freeBarPatternIso (i : ℕ) (p : List Bool)
       (v : ((barFunctor k D).obj (ModuleCat.of D (patternTerm k D X N p))).X i) :
       AlgebraTensorModule.lTensor D D (embed k D X N (List.replicate i false ++ p))
         ((freeBarPatternIso k D X N i p).hom.hom v) =
       outerCast k D X N
         (show p.length+i=(List.replicate i false ++ p).length by simp; omega)
         (outerSuffixEmbed k D X N (patternTerm k D X N p) p.length i (embed k D X N p)
           ((freeBarObjIso k D (patternTerm k D X N p) i).hom.hom v)) := by
   …

   Mentions: OAI.DerivedBar.barFunctor, OAI.DerivedBar.ParityBridge.outerCast, OAI.DerivedBar.ParityBridge.outerSuffixEmbed

2. theorem OAI.DerivedBar.ParityBridge.outerBarSuffix_canonicalLinear line 57
3. theorem OAI.DerivedBar.ParityBridge.outerBarSuffix_termCast line 66
4. theorem OAI.DerivedBar.ParityBridge.freeBarPatternIso_eqToIso line 77