OAI/Algebra/Finitistic/Ordinary/OrdinaryPairQuasiIso.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.PairComplex.map line 13
2. theorem OAI.LittleFinitistic.PairComplex.biprodIso_natural line 25
3. theorem OAI.LittleFinitistic.PairComplex.biprodMap_quasiIso line 36

   Source documentation

   Native binary biproducts preserve actual quasi-isomorphisms.

   theorem biprodMap_quasiIso (f : O ⟶ O') (g : T ⟶ T') [QuasiIso f] [QuasiIso g] :
       QuasiIso (biprod.map f g) := by
   …

4. theorem OAI.LittleFinitistic.PairComplex.map_quasiIso line 63

   Source documentation

   Coordinatewise quasi-isomorphisms give a quasi-isomorphism of the actual direct sum.

   theorem map_quasiIso (f : O ⟶ O') (g : T ⟶ T') [QuasiIso f] [QuasiIso g] :
       QuasiIso (map f g) := by
   …

   Mentions: OAI.LittleFinitistic.PairComplex.map