OAI/Algebra/Finitistic/Rectification/TensorArrowSum.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.TensorArrowSum.insertion line 10
2. theorem OAI.LittleFinitistic.TensorArrowSum.insertion_apply line 13
3. theorem OAI.LittleFinitistic.TensorArrowSum.desc_isIso line 18

   Source documentation

   An additive realization of the actual arrow-basis sum is an isomorphism.

   theorem desc_isIso {C : Type*} [Category C] [Preadditive C] [HasFiniteBiproducts C]
       (F : ModuleCat.{u} k ⥤ C) [F.Additive] :
       IsIso (biproduct.desc (fun a : Fin (d+1) => F.map (insertion k d a))) := by
   …

   Mentions: OAI.LittleFinitistic.TensorArrowSum.insertion

4. theorem OAI.LittleFinitistic.TensorArrowSum.desc_isIso_of_coordinates line 31

   Source documentation

   Coordinate isomorphisms identify an actual arrow family with the realized basis.

   theorem desc_isIso_of_coordinates {C : Type*} [Category C] [Preadditive C]
       [HasFiniteBiproducts C] (F : ModuleCat.{u} k ⥤ C) [F.Additive]
       (X : Fin (d+1) → C) (Y : C) (α : ∀ a, X a ≅ F.obj (ModuleCat.of k k))
       (β : Y ≅ F.obj (ModuleCat.of k (QuadraticEncoding.Arrows k d)))
       (f : ∀ a, X a ⟶ Y)
       (hf : ∀ a, (α a).hom ≫ F.map (insertion k d a) = f a ≫ β.hom) :
       IsIso (biproduct.desc f) := by
   …

   Mentions: OAI.LittleFinitistic.QuadraticEncoding.Arrows, OAI.LittleFinitistic.TensorArrowSum.insertion