OAI/Algebra/Finitistic/Encoding/RelationMatrixSequence.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.RelationMatrixSequence.relationIso line 13
  2. abbrev OAI.LittleFinitistic.RelationMatrixSequence.pathIso line 14
  3. def OAI.LittleFinitistic.RelationMatrixSequence.inclusion line 16
  4. def OAI.LittleFinitistic.RelationMatrixSequence.quotient line 18
  5. theorem OAI.LittleFinitistic.RelationMatrixSequence.transported_zero line 20
  6. theorem OAI.LittleFinitistic.RelationMatrixSequence.transported_comp_hom line 26
  7. def OAI.LittleFinitistic.RelationMatrixSequence.sequence line 31
  8. def OAI.LittleFinitistic.RelationMatrixSequence.sequenceIso line 36

    Source documentation

    The actual independent relation columns and first-arrow path columns are the canonical exact sequence.

    def sequenceIso : sequence P ≅ RelationSequence.sequence P :=
…

    Mentions: OAI.LittleFinitistic.RelationMatrixSequence.sequence, OAI.LittleFinitistic.RelationSequence.sequence

  9. theorem OAI.LittleFinitistic.RelationMatrixSequence.shortExact line 40
  10. def OAI.LittleFinitistic.RelationMatrixSequence.splitting line 44

    Source documentation

    The concrete matrix sequence splits over the base field.

    def splitting : (sequence P).Splitting := (shortExact P).splittingOfProjective

    Mentions: OAI.LittleFinitistic.RelationMatrixSequence.sequence, OAI.LittleFinitistic.RelationMatrixSequence.shortExact

  11. theorem OAI.LittleFinitistic.RelationMatrixSequence.realized_total_acyclic line 46
  12. theorem OAI.LittleFinitistic.RelationMatrixSequence.quotient_injection line 53

    Source documentation

    Each middle column maps by the original length-two path quotient.

    theorem quotient_injection (a : Fin (d+1)) (w : Arrows k d) :
    (biproduct.ι (PathBasisIso.family k d) a ≫ quotient P).hom w =
      (relationSpace P).mkQ (w ⊗ₜ[k] basis a) := by
…

    Mentions: OAI.LittleFinitistic.PathBasisIso.family, OAI.LittleFinitistic.RelationMatrixSequence.quotient

  13. theorem OAI.LittleFinitistic.RelationMatrixSequence.inclusion_coordinate line 61

    Source documentation

    An independent relation column has exactly the source coefficient matrix.

    theorem inclusion_coordinate (r : RelationIndex P) (a : Fin (d+1)) (c : k) :
    (biproduct.ι (FiniteBasisIso.family (k := k) : RelationIndex P → _) r ≫
…

    Mentions: OAI.LittleFinitistic.FiniteBasisIso.family