OAI/Algebra/Finitistic/Selected/SelectedRealization.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.SelectedRealization.input line 19
  2. abbrev OAI.LittleFinitistic.SelectedRealization.selectedRepresentation line 20
  3. abbrev OAI.LittleFinitistic.SelectedRealization.reference line 21
  4. lemma OAI.LittleFinitistic.SelectedRealization.selected_action line 24
  5. def OAI.LittleFinitistic.SelectedRealization.coordinates line 36
  6. lemma OAI.LittleFinitistic.SelectedRealization.coordinates01 line 42
  7. lemma OAI.LittleFinitistic.SelectedRealization.coordinates12 line 49
  8. def OAI.LittleFinitistic.SelectedRealization.cohomology line 57

    Source documentation

    The entire cohomology B-module is the manuscript's M(H(Y)), in both degrees.

    def cohomology (n : ℤ) (hn : n = 0 ∨ n = -3) :
    (SelectedTensor.complex (input (Y := Y))).homology n ≅ reference (Y := Y) :=
…

    Mentions: OAI.LittleFinitistic.SelectedTensor.complex, OAI.LittleFinitistic.SelectedRealization.input, OAI.LittleFinitistic.SelectedRealization.reference

  9. lemma OAI.LittleFinitistic.SelectedRealization.source_zero line 62
  10. def OAI.LittleFinitistic.SelectedRealization.realization line 71

    Source documentation

    The one fixed selecting bimodule realizes H on every finite-dimensional Y. This is an isomorphism in the full B-module derived category.

    def realization :
    SelectedTensorSplitting.object (input (Y := Y)) ≅
…

    Mentions: OAI.LittleFinitistic.SelectedTensorSplitting.object, OAI.LittleFinitistic.SelectedRealization.input