OAI/Algebra/Finitistic/Ordinary/OrdinaryProjectiveTensor.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.BalancedTensor.mapLeft_mapRightTo line 19
2. theorem OAI.LittleFinitistic.BalancedTensor.mapLeft_split line 27
3. theorem OAI.LittleFinitistic.BalancedTensor.tensor_exact_of_split line 35

   Source documentation

   Exactness descends through an actual split right-module retract.

   theorem tensor_exact_of_split (i : M →ₗ[Aᵐᵒᵖ] M') (p : M' →ₗ[Aᵐᵒᵖ] M)
       (hp : p.comp i = LinearMap.id) (f : N →ₗ[A] N') (g : N' →ₗ[A] N'')
       (h : Function.Exact f g)
       (h' : Function.Exact (mapRightTo (k := k) (M := M') f) (mapRightTo (k := k) (M := M') g)) :
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.mapRightTo

4. theorem OAI.LittleFinitistic.BalancedTensor.projectiveTensor_exact line 55

   Source documentation

   Projectivity of the actual right module suffices, with no hypothesis on the left modules.

   theorem projectiveTensor_exact [Module.Projective Aᵐᵒᵖ M]
       (f : N →ₗ[A] N') (g : N' →ₗ[A] N'') (h : Function.Exact f g) :
       Function.Exact (mapRightTo (k := k) (M := M) f) (mapRightTo (k := k) (M := M) g) := by
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.mapRightTo

5. theorem OAI.LittleFinitistic.BalancedTensor.projectiveTensor_mapsExact line 64
6. theorem OAI.LittleFinitistic.BalancedTensor.projectiveTensor_preservesHomology line 84
7. theorem OAI.LittleFinitistic.BalancedTensor.projectiveTensor_quasiIso line 89

   Source documentation

   Degree-zero projective tensor preserves quasi-isomorphisms of arbitrary complexes.

   theorem projectiveTensor_quasiIso [Module.Projective Aᵐᵒᵖ M]
       {Z Z' : CochainComplex (ModuleCat.{u} A) ℤ} (f : Z ⟶ Z') [QuasiIso f] :
       QuasiIso (((fixedTensorFunctor k A M).mapHomologicalComplex (.up ℤ)).map f) := by
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.fixedTensorFunctor