OAI/Algebra/Finitistic/Ordinary/OrdinaryTensorColumnAcyclic.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.ComplexTensor.map_id_left line 14
2. theorem OAI.LittleFinitistic.ComplexTensor.column_acyclic line 24

   Source documentation

   A signed tensor column for an actual projective right term preserves acyclicity.

   theorem column_acyclic (p : ℤ) [Module.Projective Aᵐᵒᵖ (rightTerm k A Q p)]
       (hZ : Z.Acyclic) : (column k A Q Z p).Acyclic := by
   …

   Mentions: OAI.LittleFinitistic.ComplexTensor.rightTerm, OAI.LittleFinitistic.ComplexTensor.column