OAI/Algebra/Finitistic/Encoding/ArrowBasisIso.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.ArrowBasisIso.family line 12
2. def OAI.LittleFinitistic.ArrowBasisIso.iso line 15

   Source documentation

   The adjacent arrow space is precisely the direct sum of its scalar arrow columns.

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

   Mentions: OAI.LittleFinitistic.ArrowBasisIso.family, OAI.LittleFinitistic.QuadraticEncoding.Arrows

3. theorem OAI.LittleFinitistic.ArrowBasisIso.hom_proj line 18
4. theorem OAI.LittleFinitistic.ArrowBasisIso.injection_apply line 24

   Source documentation

   The coproduct injection sends a scalar to that scalar times its original arrow basis.

   theorem injection_apply (i : Fin (d+1)) (c : k) :
       ((biproduct.ι (family k d) i ≫ (iso k d).hom).hom) c =
         c • QuadraticEncoding.basis i := by
   …

   Mentions: OAI.LittleFinitistic.ArrowBasisIso.family, OAI.LittleFinitistic.ArrowBasisIso.iso, OAI.LittleFinitistic.QuadraticEncoding.basis