OAI/Algebra/Finitistic/Ordinary/OrdinaryXResolution.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.OrdinarySimulation.XResolution.ordinaryOObject line 17
2. abbrev OAI.LittleFinitistic.OrdinarySimulation.XResolution.ordinaryOComplex line 20
3. def OAI.LittleFinitistic.OrdinarySimulation.XResolution.complex line 24

   Source documentation

   The manuscript's actual Q_X = O[0] ⊕ Q_T, with both D-actions retained.

   def complex := OffDiagonal.complex k B (B ⊗[k] ChainAlgebra k l)
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.complex, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra

4. abbrev OAI.LittleFinitistic.OrdinarySimulation.XResolution.target line 27
5. def OAI.LittleFinitistic.OrdinarySimulation.XResolution.augmentation line 32

   Source documentation

   The identity on O and the genuine terminal augmentation give a D-bimodule chain map.

   def augmentation : complex P a l ⟶ target P a l :=
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.XResolution.complex, OAI.LittleFinitistic.OrdinarySimulation.XResolution.target

6. theorem OAI.LittleFinitistic.OrdinarySimulation.XResolution.ordinaryOComplex_right_projective line 36
7. theorem OAI.LittleFinitistic.OrdinarySimulation.XResolution.right_projective line 56

   Source documentation

   Every actual term of Q_X is right-D-projective; no left projectivity is assumed.

   theorem right_projective
       [∀ n, Module.Projective Bᵐᵒᵖ ((underlyingRightComplex P).X n)] (n : ℤ) :
       Module.Projective (AlgebraD k l B)ᵐᵒᵖ
         (BimoduleCoefficients k (AlgebraD k l B) (AlgebraD k l B) ((complex P a l).X n)) := by
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.underlyingRightComplex, OAI.LittleFinitistic.OrdinarySimulation.AlgebraD, OAI.LittleFinitistic.BimoduleCoefficients, OAI.LittleFinitistic.OrdinarySimulation.XResolution.complex

8. theorem OAI.LittleFinitistic.OrdinarySimulation.XResolution.vanishes line 71

   Source documentation

   The support of the genuine resolution is exactly bounded by [-l,0].

   theorem vanishes (n : ℤ) (hn : n < -(l:ℤ) ∨ 0 < n) : IsZero ((complex P a l).X n) := by
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.XResolution.complex