OAI/Algebra/Finitistic/Bar/PatternPrefixCoordinates.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DerivedBar.ParityBridge.termPatternIso_hom_tmul line 22

   Source documentation

   Prefix coordinates act literally on each tensor generator.

   theorem termPatternIso_hom_tmul (i : ℕ) (p : List Bool) (d : D)
       (v : term k D (patternTerm k D X N p) i) :
       (termPatternIso k D X N (i+1) p).hom.hom (d ⊗ₜ[k] v) =
         d ⊗ₜ[k] (termPatternIso k D X N i p).hom.hom v := rfl
   …

   Mentions: OAI.DerivedBar.term

2. theorem OAI.DerivedBar.ParityBridge.embed_termPatternIso line 30

   Source documentation

   The recursive suffix embedding is exactly the existing literal block embedding, with every degree cast exposed.

   theorem embed_termPatternIso (i : ℕ) (p : List Bool)
       (v : term k D (patternTerm k D X N p) i) :
       embed k D X N (List.replicate i false ++ p)
         ((termPatternIso k D X N i p).hom.hom v) =
       termCast k D X N (show p.length+i=(List.replicate i 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 v) := by
   …

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