OAI/Algebra/Finitistic/Ordinary/OrdinaryOffDiagonalForget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.forgetTermIso line 16
  2. def OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.forgetIso line 22

    Source documentation

    Forgetting the two outside actions gives the actual coordinate direct-sum complex.

    def forgetIso : underlyingComplex (k := k) (complex k L R O T) ≅
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.underlyingComplex, OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.complex

  3. theorem OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.forgetIso_natural line 37
  4. theorem OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.complexMap_quasiIso line 47

    Source documentation

    The actual off-diagonal map is a quasi-isomorphism when its two components are.

    theorem complexMap_quasiIso (f : O ⟶ O') (g : T ⟶ T') [QuasiIso f] [QuasiIso g] :
    QuasiIso (complexMap k L R f g) := by
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.complexMap