OAI/Algebra/Finitistic/Localization/VectorComplexFormality.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.VectorComplexFormality.zeroComplex line 17

    Source documentation

    A graded vector space regarded as a complex with zero differential.

    def zeroComplex (V : ℤ → ModuleCat.{v} k) : CochainComplex (ModuleCat.{v} k) ℤ where
…
  2. def OAI.LittleFinitistic.VectorComplexFormality.homologySection line 23
  3. lemma OAI.LittleFinitistic.VectorComplexFormality.homologySection_comp line 28
  4. def OAI.LittleFinitistic.VectorComplexFormality.formalityMap line 34

    Source documentation

    Choose cycle representatives for each homology vector space.

    def formalityMap (C : CochainComplex (ModuleCat.{v} k) ℤ) :
    zeroComplex (fun i => C.homology i) ⟶ C where
…

    Mentions: OAI.LittleFinitistic.VectorComplexFormality.zeroComplex

  5. lemma OAI.LittleFinitistic.VectorComplexFormality.formality_cycles line 41
  6. lemma OAI.LittleFinitistic.VectorComplexFormality.formality_homology line 47
  7. instance OAI.LittleFinitistic.VectorComplexFormality.formalityMapQuasiIso line 53
  8. lemma OAI.LittleFinitistic.VectorComplexFormality.homology_finite line 64
  9. lemma OAI.LittleFinitistic.VectorComplexFormality.zeroHomology_property line 71
  10. def OAI.LittleFinitistic.VectorComplexFormality.zeroHomologyK line 81

    Source documentation

    The bounded homology representative has the same finite support and finite terms.

    def zeroHomologyK (T : K.{u,v} k) : K.{u,v} k :=
…
  11. def OAI.LittleFinitistic.VectorComplexFormality.formalityIso line 86

    Source documentation

    Every bounded complex of vector spaces is isomorphic to its homology with zero differential.

    def formalityIso (T : K.{u,v} k) : zeroHomologyK T ≅ T := by
…

    Mentions: OAI.LittleFinitistic.VectorComplexFormality.zeroHomologyK