RelationSequence.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.RelationSequence.sequence line 14
Source documentation
The actual length-two relation subspace, all paths, and their quotient.
```
noncomputable def sequence : ShortComplex (ModuleCat k) where
…
```
theorem OAI.LittleFinitistic.RelationSequence.sequence_shortExact line 29
Source documentation
No additional relation appears: the path quotient sequence is genuinely exact.
```
theorem sequence_shortExact : (sequence P).ShortExact := by
…
```
Mentions: OAI.LittleFinitistic.RelationSequence.sequence
def OAI.LittleFinitistic.RelationSequence.sequenceSplitting line 42
Source documentation
Over the base field this exact sequence has an actual splitting.
```
noncomputable def sequenceSplitting : (sequence P).Splitting :=
…
```
Mentions: OAI.LittleFinitistic.RelationSequence.sequence
def OAI.LittleFinitistic.RelationSequence.relationBasis line 46
Source documentation
The finite relation basis used by the manuscript exists for this exact subspace.
```
noncomputable def relationBasis : Module.Basis (Fin (Module.finrank k (relationSpace P))) k
    (relationSpace P) := by
…
```
theorem OAI.LittleFinitistic.RelationSequence.realized_sequence_shortExact line 53
Source documentation
Tensoring the split path sequence with a complex, or applying any additive realization functor, gives a short exact sequence of actual complexes.
```
theorem realized_sequence_shortExact {C : Type*} [Category C] [Abelian C]
    (F : ModuleCat k ⥤ CochainComplex C ℤ) [F.Additive] :
    ((sequence P).map F).ShortExact :=
…
```
Mentions: OAI.LittleFinitistic.RelationSequence.sequence

theorem OAI.LittleFinitistic.RelationSequence.realized_sequence_total_acyclic line 59

Source documentation

The (0,2) associated graded total is acyclic after such a realization.

theorem realized_sequence_total_acyclic {C : Type*} [Category C] [Abelian C]
    (F : ModuleCat k ⥤ CochainComplex C ℤ) [F.Additive] :
    (RectificationTotal.total ((sequence P).map F).g ((sequence P).map F).f
      (Homotopy.ofEq ((sequence P).map F).zero)).Acyclic :=
…

Mentions: OAI.LittleFinitistic.RectificationTotal.total, OAI.LittleFinitistic.RelationSequence.sequence