OAI/Algebra/Finitistic/Bar/BalancedTensorFunctor.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DerivedBar.Balanced.tensorFunctor line 17
  2. instance OAI.DerivedBar.Balanced.tensorFunctor_additive line 23
  3. def OAI.DerivedBar.Balanced.tensorFunctorObjIso line 34
  4. theorem OAI.DerivedBar.Balanced.tensorFunctorObjIso_natural line 41
  5. def OAI.DerivedBar.Balanced.resolvedTensorIso line 55
  6. def OAI.DerivedBar.Balanced.tensorBarComputesLeftDerived line 71

    Source documentation

    The left-derived balanced tensor functor is computed by exactly the original tensorBarComplex, via the proved free bar projective resolution.

    def tensorBarComputesLeftDerived :
    (tensorFunctor f).leftDerivedToHomotopyCategory.obj (ModuleCat.of A N) ≅
      (HomotopyCategory.quotient (ModuleCat.{u} D) (.down ℕ)).obj (tensorBarComplex k A D N f) :=
…

    Mentions: OAI.DerivedBar.Balanced.tensorFunctor, OAI.DerivedBar.tensorBarComplex

  7. def OAI.DerivedBar.Balanced.tensorBarHomologyIso line 77