OAI/Algebra/Finitistic/Selected/SelectedTensor.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.SelectedTensor.complex line 13

    Source documentation

    Evaluate the one fixed selecting bimodule, retaining its full left action.

    abbrev complex := FullTensorRectification.tensor P D0 D1 D2 f g relations N

    Mentions: OAI.LittleFinitistic.FullTensorRectification.tensor

  2. abbrev OAI.LittleFinitistic.SelectedTensor.source line 14
  3. abbrev OAI.LittleFinitistic.SelectedTensor.comparison line 15
  4. instance OAI.LittleFinitistic.SelectedTensor.comparison_isIso line 19

    Source documentation

    Every cohomology comparison is invertible for the fixed selected representatives.

    instance comparison_isIso (v : Fin 3) (n : ℤ) : IsIso (comparison N v n) := by
…

    Mentions: OAI.LittleFinitistic.SelectedTensor.comparison

  5. def OAI.LittleFinitistic.SelectedTensor.comparisonIso line 32
  6. theorem OAI.LittleFinitistic.SelectedTensor.bounded line 35

    Source documentation

    The actual tensor complex has bounded support.

    theorem bounded : ∃ lo hi : ℤ, ∀ n, n < lo ∨ hi < n → IsZero ((complex N).X n) := by
…

    Mentions: OAI.LittleFinitistic.SelectedTensor.complex

  7. theorem OAI.LittleFinitistic.SelectedTensor.finite line 40

    Source documentation

    Every actual evaluated term is finite-dimensional.

    theorem finite [FiniteDimensional ℂ N] (n : ℤ) :
    FiniteDimensional ℂ ((ModuleCat.restrictScalars (algebraMap ℂ (B P))).obj ((complex N).X n)) := by
…

    Mentions: OAI.LittleFinitistic.SelectedTensor.complex