OAI/Algebra/Finitistic/Ordinary/OrdinaryBimoduleAugmentation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.bimoduleTerminal line 12
  2. abbrev OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.bimoduleTerminalObject line 13
  3. def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.bimoduleAugmentationHom line 16
  4. def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.bimoduleAugmentationMap line 21

    Source documentation

    The actual augmentation of the genuine finite bimodule resolution.

    def bimoduleAugmentationMap : bimoduleComplex k B l ⟶
    (HomologicalComplex.single _ (.up ℕ) l).obj (bimoduleTerminalObject k B l) :=
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.bimoduleComplex, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.bimoduleTerminalObject

  5. def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.forgetBimoduleTerminal line 34
  6. def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.forgetAugmentationTargetIso line 49