OAI/Algebra/Finitistic/Ordinary/OrdinaryBimoduleAssociativeTerms.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.BimoduleComplexTensor.middleBimoduleComplex line 20
2. def OAI.LittleFinitistic.BimoduleComplexTensor.associativeTermEquiv line 23

   Source documentation

   Associativity on actual cochain terms, retaining the outside S-action.

   def associativeTermEquiv (p q : ℤ) :
       term k S B (middleBimoduleComplex k S A B N Q) Z p q ≃ₗ[S]
         term k S A Q (middleLeftComplex k A B N Z) p q := by
   …

   Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.term, OAI.LittleFinitistic.BimoduleComplexTensor.middleBimoduleComplex, OAI.LittleFinitistic.middleLeftComplex

3. theorem OAI.LittleFinitistic.BimoduleComplexTensor.associativeTermEquiv_map line 33

   Source documentation

   Associativity commutes with both actual cochain-term maps.

   theorem associativeTermEquiv_map {p p' q q' : ℤ} (f : Q.X p ⟶ Q.X p') (g : Z.X q ⟶ Z.X q') :
       (associativeTermEquiv k S A B N Q Z p' q').toLinearMap.comp
         (map k S B (middleBimoduleComplex k S A B N Q) Z ((bimoduleTensorFunctor k S A Bᵐᵒᵖ N).map f) g) =
       (map k S A Q (middleLeftComplex k A B N Z) f ((middleLeftFunctor k A B N).map g)).comp
         (associativeTermEquiv k S A B N Q Z p q).toLinearMap := by
   …

   Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.associativeTermEquiv, OAI.LittleFinitistic.BimoduleComplexTensor.map, OAI.LittleFinitistic.BimoduleComplexTensor.middleBimoduleComplex, OAI.LittleFinitistic.bimoduleTensorFunctor, OAI.LittleFinitistic.middleLeftComplex, OAI.LittleFinitistic.middleLeftFunctor