OAI/Algebra/Finitistic/Ordinary/OrdinaryIntegerResolution.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.degreeEmbedding line 12
  2. instance OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.degreeEmbedding_rel line 15
  3. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.degreeEmbedding_apply line 18
  4. def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerComplex line 21

    Source documentation

    Q_T in the manuscript's cohomological degrees -l,...,0.

    def integerComplex : CochainComplex (ModuleCat.{u} (B ⊗[k] ChainAlgebra k l)ᵐᵒᵖ) ℤ :=
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra

  5. def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerTermIso line 24
  6. def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerAugmentation line 28

    Source documentation

    The terminal simple is in degree zero after the actual reindexing.

    def integerAugmentation : integerComplex k B l ⟶
    (HomologicalComplex.single _ (.up ℤ) 0).obj
      (ModuleCat.of (B ⊗[k] ChainAlgebra k l)ᵐᵒᵖ (TerminalTensor B)) :=
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerComplex, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.TerminalTensor

  7. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerAugmentation_quasiIso line 35
  8. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerTerm_lower line 42
  9. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerTerm_upper line 48
  10. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerTerm_projective line 60