OAI/Algebra/Finitistic/Ordinary/OrdinaryTensorResolution.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.term line 15
  2. def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.termEquiv line 18
  3. def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.regularEquiv line 21
  4. def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.leftMultiply line 30
  5. def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.retract line 36
  6. instance OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.term_projective line 41
  7. def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.differential line 49

    Source documentation

    The B-extended resolution differential is left multiplication by 1 tensor c.

    def differential (n : ℕ) : term k B l n →ₗ[(B ⊗[k] ChainAlgebra k l)ᵐᵒᵖ] term k B l (n+1) :=
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.term, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra

  8. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.differential_square line 57
  9. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.termEquiv_d line 62
  10. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.differential_exact line 74

    Source documentation

    Every interior exact sequence stays exact after the actual B-extension over k.

    theorem differential_exact (n : ℕ) (hn : n+1 < l) :
    Function.Exact (differential k B l n) (differential k B l (n+1)) := by
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.differential