OAI/Algebra/Finitistic/Ordinary/OrdinarySourceDerivedComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.OrdinarySimulation.resolvedBimoduleComparison line 20

   Source documentation

   The source's resolved T tensor O comparison in the native derived category of genuine B-bimodules. Its left operand includes the actual bounded right-BC-projective resolution and augmentation to T.

   def resolvedBimoduleComparison :
       (TensorResolution.resolutionModel k B l).tensorOrdinary B (BimoduleO P a l) ≅
         DerivedCategory.Q.obj (P⟦b⟧) :=
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.resolutionModel, OAI.LittleFinitistic.OrdinarySimulation.BimoduleO

2. def OAI.LittleFinitistic.OrdinarySimulation.resolvedSquareComparison line 31

   Source documentation

   The source's native derived square with both tensor functors tied to their certified full-support models.

   def resolvedSquareComparison (Z : CochainComplex (ModuleCat.{u} B) ℤ) :
       (XResolution.resolutionModel P a l).toFiniteProjectiveBimoduleComplex.derivedTensor.obj
         ((XResolution.resolutionModel P a l).toFiniteProjectiveBimoduleComplex.derivedTensor.obj
           ((BlockModule.derivedFirst B (B ⊗[k] ChainAlgebra k l)).obj (DerivedCategory.Q.obj Z))) ≅
       (BlockModule.derivedFirst B (B ⊗[k] ChainAlgebra k l)).obj
         ((shiftedResolutionModel P a l b hb hP).derivedTensor.obj (DerivedCategory.Q.obj Z)) :=
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.XResolution.resolutionModel, OAI.LittleFinitistic.BlockModule.derivedFirst, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.shiftedResolutionModel