OAI/Algebra/Finitistic/Ordinary/OrdinaryFiniteTotalMaps.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.FiniteColumnComplex.componentMap line 14

   Source documentation

   The degreewise map between the actual finite sums of columns.

   def componentMap (n : ℤ) : term K n →ₗ[R] term L n :=
   …

   Mentions: OAI.LittleFinitistic.FiniteColumnComplex.term

2. theorem OAI.LittleFinitistic.FiniteColumnComplex.componentMap_apply line 17
3. def OAI.LittleFinitistic.FiniteColumnComplex.complexMap line 21

   Source documentation

   A compatible family of column maps gives an actual map of total complexes.

   def complexMap (hc : ∀ n,
       (ε.d n).comp (componentMap K L f n) = (componentMap K L f (n+1)).comp (δ.d n)) :
       complex K δ ⟶ complex L ε where
   …

   Mentions: OAI.LittleFinitistic.FiniteColumnComplex.componentMap, OAI.LittleFinitistic.FiniteColumnComplex.complex