OAI/Topology/ArtinGroups/Complexes/InitialProjective.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.initialProjective line 11
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homDimension_le_homSpace line 19
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.initial_homSpace_nonzero_cochain line 26
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.initial_homSpace_orthogonal line 38
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.initial_self_entry_decomposition line 52
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.initial_self_entry_homogeneous line 61
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.initial_homSpace_other_internal line 67
8. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.initialCoordinate line 80
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.initialCoordinate_injective line 87
10. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.initial_homDimension_le_one line 115