OAI/Algebra/Finitistic/Bar/FiniteBarResolution.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.DerivedBar.term_finiteDimensional line 17

   Source documentation

   Every absolute bar word remains finite dimensional over the base field.

   instance term_finiteDimensional : (n : ℕ) → FiniteDimensional k (term k A N n)
     | 0 => inferInstanceAs (FiniteDimensional k N)
     | n+1 => by
       let := term_finiteDimensional n
   …

   Mentions: OAI.DerivedBar.term

2. instance OAI.DerivedBar.term_finite line 23
3. theorem OAI.DerivedBar.projectiveResolution_finite line 27

   Source documentation

   The actual bar projective resolution has finitely generated free terms.

   theorem projectiveResolution_finite (n : ℕ) :
       Module.Finite A ((projectiveResolution k A N).complex.X n) :=
   …

   Mentions: OAI.DerivedBar.projectiveResolution

4. theorem OAI.DerivedBar.projectiveResolution_free line 31