OAI/Algebra/Finitistic/Ordinary/OrdinaryFullTensorComplex.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.OrdinarySimulation.FullTensorTerm.differential line 14
  2. theorem OAI.LittleFinitistic.OrdinarySimulation.FullTensorTerm.differential_square line 18
  3. def OAI.LittleFinitistic.OrdinarySimulation.FullTensorTerm.complex line 30

    Source documentation

    Actual tensor complex, with both B-actions and the actual extended arrow maps.

    def complex : CochainComplex (ModuleCat.{u} (Enveloping k B)) ℕ :=
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.Enveloping

  4. theorem OAI.LittleFinitistic.OrdinarySimulation.FullTensorTerm.supportedEquiv_mk line 36

    Source documentation

    Supported evaluation is the product action followed by the source coordinate projection.

    theorem supportedEquiv_mk (n : ℕ) (hn : n ≤ l) (m : TensorResolution.term k B l n) (v : BimoduleO P a l) :
    supportedEquiv P a l n hn
      (TwoSidedTensor.mk k (B ⊗[k] ChainAlgebra k l) B Bᵐᵒᵖ (TensorResolution.term k B l n) (BimoduleO P a l) m v) =
        (m.val • v : BimoduleO P a l) ⟨n,by omega⟩ := rfl

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.term, OAI.LittleFinitistic.OrdinarySimulation.BimoduleO, OAI.LittleFinitistic.OrdinarySimulation.FullTensorTerm.supportedEquiv, OAI.LittleFinitistic.TwoSidedTensor.mk, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra

  5. theorem OAI.LittleFinitistic.OrdinarySimulation.FullTensorTerm.supported_differential line 41
  6. theorem OAI.LittleFinitistic.OrdinarySimulation.FullTensorTerm.termEquiv_differential line 61
  7. def OAI.LittleFinitistic.OrdinarySimulation.FullTensorTerm.complexIso line 72

    Source documentation

    The entire actual tensor complex identifies with P on degrees a,a+1,... .

    def complexIso : complex P a l ≅ P.restriction (ComplexShape.embeddingUpIntGE a) :=
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.FullTensorTerm.complex