OAI/Algebra/Finitistic/Encoding/PathBasisIso.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.PathBasisIso.family line 11
2. def OAI.LittleFinitistic.PathBasisIso.iso line 14

   Source documentation

   Group paths by their first traversed arrow; the later arrow is the first tensor factor.

   def iso : (⨁ family k d) ≅ ModuleCat.of k (QuadraticEncoding.Paths k d) :=
   …

   Mentions: OAI.LittleFinitistic.PathBasisIso.family, OAI.LittleFinitistic.QuadraticEncoding.Paths

3. theorem OAI.LittleFinitistic.PathBasisIso.pi_hom_proj line 18
4. theorem OAI.LittleFinitistic.PathBasisIso.pi_injection_apply line 24
5. theorem OAI.LittleFinitistic.PathBasisIso.injection_apply line 38

   Source documentation

   A summand w at a maps to the actual tensor path w tensor a.

   theorem injection_apply (a : Fin (d+1)) (w : QuadraticEncoding.Arrows k d) :
       (biproduct.ι (family k d) a ≫ (iso k d).hom).hom w = w ⊗ₜ[k] QuadraticEncoding.basis a := by
   …

   Mentions: OAI.LittleFinitistic.QuadraticEncoding.Arrows, OAI.LittleFinitistic.PathBasisIso.family, OAI.LittleFinitistic.PathBasisIso.iso, OAI.LittleFinitistic.QuadraticEncoding.basis