OAI/Algebra/Finitistic/Ordinary/OrdinaryFiniteTotal.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.FiniteColumnComplex.diagonal line 12

   Source documentation

   The vertical differential on the finite direct sum of the columns.

   def diagonal (n : ℤ) : term K n →ₗ[R] term K (n+1) :=
   …

   Mentions: OAI.LittleFinitistic.FiniteColumnComplex.term

2. theorem OAI.LittleFinitistic.FiniteColumnComplex.diagonal_apply line 15
3. theorem OAI.LittleFinitistic.FiniteColumnComplex.diagonal_square line 18
4. structure OAI.LittleFinitistic.FiniteColumnComplex.Horizontal line 25

   Source documentation

   A horizontal differential on signed columns, with its actual square and mixed relation.

   structure Horizontal where
   …

5. def OAI.LittleFinitistic.FiniteColumnComplex.totalDifferential line 35

   Source documentation

   The full differential is the sum of the signed vertical and horizontal differentials.

   def totalDifferential : Differential K where
   …

   Mentions: OAI.LittleFinitistic.FiniteColumnComplex.Differential

6. def OAI.LittleFinitistic.FiniteColumnComplex.total line 54
7. theorem OAI.LittleFinitistic.FiniteColumnComplex.total_acyclic line 56