OAI/Algebra/Finitistic/Ordinary/OrdinaryBimoduleCoefficientEquiv.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.BimoduleCoefficients.equiv line 14
  2. theorem OAI.LittleFinitistic.BimoduleCoefficients.equiv_left line 20
  3. def OAI.LittleFinitistic.BimoduleComplexTensor.rightTermEquiv line 29
  4. theorem OAI.LittleFinitistic.BimoduleComplexTensor.rightTermEquiv_map line 35

    Source documentation

    Both actual tensor maps respect an isomorphism of genuine bimodule complexes.

    theorem rightTermEquiv_map (p p' q q' : ℤ) (g : Z.X q ⟶ Z.X q') :
    (rightTermEquiv k S A e Z p' q').toLinearMap.comp (map k S A Q Z (Q.d p p') g) =
    (map k S A Q' Z (Q'.d p p') g).comp (rightTermEquiv k S A e Z p q).toLinearMap := by
…

    Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.rightTermEquiv, OAI.LittleFinitistic.BimoduleComplexTensor.map

  5. theorem OAI.LittleFinitistic.BimoduleComplexTensor.rightTermEquiv_map_id line 45