OAI/RingTheory/Multiplicity/CechReduction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Lech.FiniteModuleCech.coefficients line 14
2. def OAI.Lech.FiniteModuleCech.Map.coefficients line 20
3. abbrev OAI.Lech.FiniteModuleCech.reduction line 28
4. lemma OAI.Lech.FiniteModuleCech.quotientPiEquiv_d line 30
5. def OAI.Lech.FiniteModuleCech.reductionComplexIso line 50
6. def OAI.Lech.FiniteModuleCech.reductionPositiveIso line 68
7. lemma OAI.Lech.FiniteModuleCech.reduction_cochains_torsion line 87
8. lemma OAI.Lech.FiniteModuleCech.reduction_homology_torsion line 93
9. lemma OAI.Lech.FiniteModuleCech.reduction_positiveHomology_torsion line 99
10. lemma OAI.Lech.FiniteModuleCech.Map.cochains_isoModSerre line 110
11. lemma OAI.Lech.FiniteModuleCech.Map.homology_isoModSerre line 115
12. lemma OAI.Lech.FiniteModuleCech.Map.positiveHomology_isoModSerre line 119