OAI/Algebra/Finitistic/Dimension/PDBaseBarConsumer.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.PDBarQuotient.restrictHomologyIso line 17

   Source documentation

   Restriction of scalars preserves the actual homology of a D-complex.

   def restrictHomologyIso (C : ChainComplex (ModuleCat.{u} D) ℕ) (n : ℕ) :
       (((ModuleCat.restrictScalars (algebraMap k D)).mapHomologicalComplex _).obj C).homology n ≅
         (ModuleCat.restrictScalars (algebraMap k D)).obj (C.homology n) :=
   …

2. theorem OAI.LittleFinitistic.PDBarQuotient.lower_bound_of_base_bar line 27

   Source documentation

   Actual nonzero D-module bar homology, with its exterior action intact, forces the same projective-dimension lower bound over A.

   theorem lower_bound_of_base_bar (r n : ℕ) (hrn : r ≤ n)
       (h : ¬ IsZero ((DerivedBar.twoSidedComplex k A D N f).homology n)) :
       r ≤ projectiveDimension (ModuleCat.of A N) := by
   …

   Mentions: OAI.DerivedBar.twoSidedComplex

3. abbrev OAI.LittleFinitistic.PDBarQuotient.baseDerived line 41
4. def OAI.LittleFinitistic.PDBarQuotient.baseDerivedHomologyIso line 44
5. theorem OAI.LittleFinitistic.PDBarQuotient.lower_bound_of_base_derived_retract line 52

   Source documentation

   Consumer of an actual D-linear derived bar splitting. No splitting or nonzero-iterate theorem is assumed implicitly; the iso, retract and class are inputs.

   theorem lower_bound_of_base_derived_retract
       (Z T : DerivedCategory (ModuleCat.{u} D)) (e : baseDerived f N ≅ Z)
       (i : T ⟶ Z) (p : Z ⟶ T) (hip : i ≫ p = 𝟙 T)
       (r n : ℕ) (hrn : r ≤ n)
       (h : ¬ IsZero ((DerivedCategory.homologyFunctor (ModuleCat D) (-(n : ℤ))).obj T)) :
       r ≤ projectiveDimension (ModuleCat.of A N) := by
   …

   Mentions: OAI.LittleFinitistic.PDBarQuotient.baseDerived