OAI/Algebra/Finitistic/Localization/VectorIdempotentCompleteness.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LittleFinitistic.VectorComplexFormality.zeroDifferential_homotopy_eq line 12
2. lemma OAI.LittleFinitistic.VectorComplexFormality.zeroDifferential_idempotents_split line 19
3. instance OAI.LittleFinitistic.VectorComplexFormality.finiteVectorHomotopyIdempotentComplete line 70

   Source documentation

   Bounded finite-dimensional homotopy complexes split every idempotent.

   instance finiteVectorHomotopyIdempotentComplete : IsIdempotentComplete (K.{u,v} k) where
   …

4. instance OAI.LittleFinitistic.VectorComplexFormality.finiteVectorDerivedIdempotentComplete line 83

   Source documentation

   The actual bounded finite-dimensional derived target is idempotent complete.

   instance finiteVectorDerivedIdempotentComplete :
       IsIdempotentComplete (FiniteVectorDerived.{u,v} (k := k)) :=
   …