OAI/NumberTheory/PiExponent/Geometry/LineBundleGluing.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PiExponentSeshadri.LineBundleGluing.Cocycle line 15
  2. def OAI.PiExponentSeshadri.LineBundleGluing.LocalIndex line 25
  3. abbrev OAI.PiExponentSeshadri.LineBundleGluing.Family line 27
  4. def OAI.PiExponentSeshadri.LineBundleGluing.localModule line 30
  5. instance OAI.PiExponentSeshadri.LineBundleGluing.familyModule line 34
  6. def OAI.PiExponentSeshadri.LineBundleGluing.sections line 40
  7. def OAI.PiExponentSeshadri.LineBundleGluing.restrict line 84
  8. lemma OAI.PiExponentSeshadri.LineBundleGluing.restrict_smul line 91
  9. def OAI.PiExponentSeshadri.LineBundleGluing.presheaf line 103
  10. def OAI.PiExponentSeshadri.LineBundleGluing.fromChart line 114
  11. def OAI.PiExponentSeshadri.LineBundleGluing.chartEquiv line 136
  12. lemma OAI.PiExponentSeshadri.LineBundleGluing.chartEquiv_restrict line 159
  13. lemma OAI.PiExponentSeshadri.LineBundleGluing.chartEquiv_change line 165
  14. def OAI.PiExponentSeshadri.LineBundleGluing.openPresheafFrame line 170
  15. def OAI.PiExponentSeshadri.LineBundleGluing.chartPresheafFrame line 182
  16. def OAI.PiExponentSeshadri.LineBundleGluing.sheaf line 187
  17. def OAI.PiExponentSeshadri.LineBundleGluing.openFrame line 190
  18. def OAI.PiExponentSeshadri.LineBundleGluing.lineBundle line 199
  19. def OAI.PiExponentSeshadri.LineBundleGluing.restrictUnit line 212
  20. lemma OAI.PiExponentSeshadri.LineBundleGluing.restrictUnit_val line 215
  21. lemma OAI.PiExponentSeshadri.LineBundleGluing.restrictUnit_trans line 218
  22. lemma OAI.PiExponentSeshadri.LineBundleGluing.restrictUnit_refl line 226
  23. structure OAI.PiExponentSeshadri.LineBundleGluing.PairCocycle line 233
  24. def OAI.PiExponentSeshadri.LineBundleGluing.PairCocycle.toCocycle line 246
  25. lemma OAI.PiExponentSeshadri.LineBundleGluing.PairCocycle.toCocycle_transition line 257
  26. def OAI.PiExponentSeshadri.LineBundleGluing.PairCocycle.lineBundle line 261