OAI/Algebra/Finitistic/Bar/BarPatternEmbedding.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DerivedBar.ParityBridge.embed_twoSidedBarPatternIso line 20

   Source documentation

   The categorical X-bar pattern coordinates and the suffix formula have exactly the same embedding into the original A bar, including the degree cast.

   theorem embed_twoSidedBarPatternIso (i : ℕ) (p : List Bool)
       (v : ((BimoduleTensor.twoSidedBarFunctor k D X).obj
         (ModuleCat.of D (patternTerm k D X N p))).X i) :
       embed k D X N (true :: (List.replicate i false ++ p))
         ((twoSidedBarPatternIso k D X N i p).hom.hom v) =
       termCast k D X N
         (show (p.length+i)+1=(true :: (List.replicate i false ++ p)).length by simp; omega)
         (idealSuffixEmbed k D X N (patternTerm k D X N p) p.length i (embed k D X N p)
           ((twoSidedBarObjIso k D X (patternTerm k D X N p) i).hom.hom v)) := by
   …

   Mentions: OAI.DerivedBar.BimoduleTensor.twoSidedBarFunctor, OAI.DerivedBar.ParityBridge.termCast, OAI.DerivedBar.ParityBridge.idealSuffixEmbed

2. theorem OAI.DerivedBar.ParityBridge.embed_freeBarPatternIso line 50

   Source documentation

   The same compatibility for the final free D bar, before projecting its exterior slot.

   theorem embed_freeBarPatternIso (i : ℕ) (p : List Bool)
       (v : ((barFunctor k D).obj (ModuleCat.of D (patternTerm k D X N p))).X i) :
       embed k D X N (List.replicate (i+1) false ++ p)
         ((freeBarPatternIso k D X N i p).hom.hom v) =
       termCast k D X N
         (show p.length+(i+1)=(List.replicate (i+1) false ++ p).length by simp; omega)
         (suffixEmbed k D X N (patternTerm k D X N p) p.length (embed k D X N p) (i+1)
           ((freeBarObjIso k D (patternTerm k D X N p) i).hom.hom v)) :=
   …

   Mentions: OAI.DerivedBar.barFunctor, OAI.DerivedBar.ParityBridge.termCast, OAI.DerivedBar.ParityBridge.suffixEmbed